:: CHAIN_1 semantic presentation

theorem Th1: :: CHAIN_1:1

for x, y being real number st x < y holds
ex z being Real st
( x < z & z < y )

proof end;

theorem Th2: :: CHAIN_1:2

for x, y being real number ex z being Real st
( x < z & y < z )

proof end;

scheme :: CHAIN_1:sch 1
FrSet12{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ], F₃( set , set ) -> Element of F₁() } :

{ F₃(x,y) where x, y is Element of F₂() : P₁[x,y] } c= F₁()

proof end;

definition

let B be set ;
let A be Subset of B;
:: original: bool
redefine func bool A -> Subset-Family of B;
coherence by ZFMISC_1:79;

end;

definition

let d be real Nat;
redefine attr d is empty means :: CHAIN_1:def 1
not d > 0;
compatibility ;

end;

:: deftheorem defines zero CHAIN_1:def 1 :

definition

let d be Nat;
redefine attr d is empty means :Def2: :: CHAIN_1:def 2
not d >= 1;
compatibility

proof end;

end;

:: deftheorem Def2 defines zero CHAIN_1:def 2 :

registration

cluster non zero Element of NAT ;
existence

proof end;

end;

registration

let d be non zero Nat;
cluster Seg d -> non empty ;
coherence by FINSEQ_1:5;

end;

definition

let X be set ;
redefine attr X is trivial means :Def3: :: CHAIN_1:def 3
for x, y being set st x in X & y in X holds
x = y;
compatibility

proof end;

end;

:: deftheorem Def3 defines trivial CHAIN_1:def 3 :

theorem :: CHAIN_1:3

canceled;

theorem Th4: :: CHAIN_1:4

for x, y being set holds
( {x,y} is trivial iff x = y )

proof end;

registration

cluster finite non trivial set ;
existence

proof end;

end;

registration

let X be non trivial set ;
let Y be set ;
cluster X \/ Y -> non trivial ;
coherence

proof end;

cluster Y \/ X -> non trivial ;
coherence ;

end;

registration

cluster REAL -> non trivial ;
coherence

proof end;

end;

registration

let X be non trivial set ;
cluster finite non trivial Element of bool X;
existence

proof end;

end;

theorem Th5: :: CHAIN_1:5

for X, y being set st X is trivial & not X \/ {y} is trivial holds
ex x being set st X = {x}

proof end;

scheme :: CHAIN_1:sch 2
NonEmptyFinite{ F₁() -> non empty set , F₂() -> non empty finite Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x being Element of F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of F₁()
for B being non empty finite Subset of F₁() st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]

proof end;

scheme :: CHAIN_1:sch 3
NonTrivialFinite{ F₁() -> non trivial set , F₂() -> finite non trivial Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x, y being Element of F₁() st x in F₂() & y in F₂() & x <> y holds
P₁[{x,y}] and
A2: for x being Element of F₁()
for B being finite non trivial Subset of F₁() st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]

proof end;

theorem Th6: :: CHAIN_1:6

for X being set holds
( Card X = 2 iff ex x, y being set st
( x in X & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) ) )

proof end;

theorem Th7: :: CHAIN_1:7

for m, n being Nat holds
( ( m is even iff n is even ) iff m + n is even )

proof end;

theorem Th8: :: CHAIN_1:8

for X, Y being finite set st X misses Y holds
( ( card X is even iff card Y is even ) iff card (X \/ Y) is even )

proof end;

theorem Th9: :: CHAIN_1:9

for X, Y being finite set holds
( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )

proof end;

definition

let n be Nat;
redefine func REAL n means :Def4: :: CHAIN_1:def 4
for x being set holds
( x in it iff x is Function of Seg n, REAL );
compatibility

proof end;

end;

:: deftheorem Def4 defines REAL CHAIN_1:def 4 :

definition

let d be non zero Nat;
let x be Element of REAL d;
let i be Element of Seg d;
:: original: .
redefine func x . i -> Real;
coherence

proof end;

end;

definition

let d be non zero Nat;
mode Grating of d -> Function of Seg d, bool REAL means :Def5: :: CHAIN_1:def 5
for i being Element of Seg d holds
( not it . i is trivial & it . i is finite );
existence

proof end;

end;

:: deftheorem Def5 defines Grating CHAIN_1:def 5 :

definition

let d be non zero Nat;
let G be Grating of d;
let i be Element of Seg d;
:: original: .
redefine func G . i -> finite non trivial Subset of REAL ;
coherence by Def5;

end;

theorem Th10: :: CHAIN_1:10

for d being non zero Nat
for x being Element of REAL d
for G being Grating of d holds
( x in product G iff for i being Element of Seg d holds x . i in G . i )

proof end;

theorem Th11: :: CHAIN_1:11

for d being non zero Nat
for G being Grating of d holds product G is finite

proof end;

theorem Th12: :: CHAIN_1:12

for X being non empty finite Subset of REAL ex ri being Real st
( ri in X & ( for xi being Real st xi in X holds
ri >= xi ) )

proof end;

theorem Th13: :: CHAIN_1:13

for X being non empty finite Subset of REAL ex li being Real st
( li in X & ( for xi being Real st xi in X holds
li <= xi ) )

proof end;

theorem Th14: :: CHAIN_1:14

for Gi being finite non trivial Subset of REAL ex li, ri being Real st
( li in Gi & ri in Gi & li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) )

proof end;

theorem Th15: :: CHAIN_1:15

for X being non empty finite Subset of REAL ex ri being Real st
( ri in X & ( for xi being Real st xi in X holds
ri >= xi ) ) by Th12;

theorem :: CHAIN_1:16

for Gi being finite non trivial Subset of REAL ex li, ri being Real st
( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) )

proof end;

definition

let Gi be finite non trivial Subset of REAL ;
mode Gap of Gi -> Element of [:REAL ,REAL :] means :Def6: :: CHAIN_1:def 6
ex li, ri being Real st
( it = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) );
existence

proof end;

end;

:: deftheorem Def6 defines Gap CHAIN_1:def 6 :

theorem Th17: :: CHAIN_1:17

for Gi being finite non trivial Subset of REAL
for li, ri being Real holds
( [li,ri] is Gap of Gi iff ( li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) ) )

proof end;

theorem :: CHAIN_1:18

for Gi being finite non trivial Subset of REAL
for li, ri, li', ri' being Real st Gi = {li,ri} holds
( [li',ri'] is Gap of Gi iff ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) )

proof end;

deffunc H₁( set ) -> set = $1;

theorem Th19: :: CHAIN_1:19

for Gi being finite non trivial Subset of REAL
for xi being Real st xi in Gi holds
ex ri being Real st [xi,ri] is Gap of Gi

proof end;

theorem Th20: :: CHAIN_1:20

for Gi being finite non trivial Subset of REAL
for xi being Real st xi in Gi holds
ex li being Real st [li,xi] is Gap of Gi

proof end;

theorem Th21: :: CHAIN_1:21

for Gi being finite non trivial Subset of REAL
for li, ri, ri' being Real st [li,ri] is Gap of Gi & [li,ri'] is Gap of Gi holds
ri = ri'

proof end;

theorem Th22: :: CHAIN_1:22

for Gi being finite non trivial Subset of REAL
for li, ri, li' being Real st [li,ri] is Gap of Gi & [li',ri] is Gap of Gi holds
li = li'

proof end;

theorem Th23: :: CHAIN_1:23

for Gi being finite non trivial Subset of REAL
for ri, li, ri', li' being Real st ri < li & [li,ri] is Gap of Gi & ri' < li' & [li',ri'] is Gap of Gi holds
( li = li' & ri = ri' )

proof end;

definition

let d be non zero Nat;
let l, r be Element of REAL d;
func cell l,r -> non empty Subset of (REAL d) equals :: CHAIN_1:def 7
{ x where x is Element of REAL d : ( for i being Element of Seg d holds
( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) } ;
coherence

proof end;

end;

:: deftheorem defines cell CHAIN_1:def 7 :

theorem Th24: :: CHAIN_1:24

for d being non zero Nat
for x, l, r being Element of REAL d holds
( x in cell l,r iff ( for i being Element of Seg d holds
( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) )

proof end;

theorem Th25: :: CHAIN_1:25

for d being non zero Nat
for l, r, x being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) holds
( x in cell l,r iff for i being Element of Seg d holds
( l . i <= x . i & x . i <= r . i ) )

proof end;

theorem Th26: :: CHAIN_1:26

for d being non zero Nat
for r, l, x being Element of REAL d st ex i being Element of Seg d st r . i < l . i holds
( x in cell l,r iff ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) )

proof end;

theorem Th27: :: CHAIN_1:27

for d being non zero Nat
for l, r being Element of REAL d holds
( l in cell l,r & r in cell l,r )

proof end;

theorem Th28: :: CHAIN_1:28

for d being non zero Nat
for x being Element of REAL d holds cell x,x = {x}

proof end;

theorem Th29: :: CHAIN_1:29

for d being non zero Nat
for l', r', l, r being Element of REAL d st ( for i being Element of Seg d holds l' . i <= r' . i ) holds
( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i ) )

proof end;

theorem Th30: :: CHAIN_1:30

for d being non zero Nat
for r, l, l', r' being Element of REAL d st ( for i being Element of Seg d holds r . i < l . i ) holds
( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) )

proof end;

theorem Th31: :: CHAIN_1:31

for d being non zero Nat
for l, r, r', l' being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) & ( for i being Element of Seg d holds r' . i < l' . i ) holds
( cell l,r c= cell l',r' iff ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) )

proof end;

theorem Th32: :: CHAIN_1:32

for d being non zero Nat
for l, r, l', r' being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) holds
( cell l,r = cell l',r' iff ( l = l' & r = r' ) )

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
assume A1: k <= d ;
func cells k,G -> non empty finite Subset-Family of (REAL d) equals :Def8: :: CHAIN_1:def 8
{ (cell l,r) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def8 defines cells CHAIN_1:def 8 :

theorem Th33: :: CHAIN_1:33

for k being Nat
for d being non zero Nat
for G being Grating of d st k <= d holds
for A being Subset of (REAL d) holds
( A in cells k,G iff ex l, r being Element of REAL d st
( A = cell l,r & ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )

proof end;

theorem Th34: :: CHAIN_1:34

for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d holds
( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

proof end;

theorem Th35: :: CHAIN_1:35

for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell l,r in cells k,G & ex i being Element of Seg d st
( not ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) & not ( l . i = r . i & l . i in G . i ) ) holds
for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )

proof end;

theorem Th36: :: CHAIN_1:36

for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell l,r in cells k,G holds
for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )

proof end;

theorem :: CHAIN_1:37

for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell l,r in cells k,G & not for i being Element of Seg d holds l . i <= r . i holds
for i being Element of Seg d holds r . i < l . i by Th35;

theorem Th38: :: CHAIN_1:38

for d being non zero Nat
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells 0,G iff ex x being Element of REAL d st
( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) )

proof end;

theorem Th39: :: CHAIN_1:39

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d holds
( cell l,r in cells 0,G iff ( l = r & ( for i being Element of Seg d holds l . i in G . i ) ) )

proof end;

theorem Th40: :: CHAIN_1:40

for d being non zero Nat
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells d,G iff ex l, r being Element of REAL d st
( A = cell l,r & ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

proof end;

theorem Th41: :: CHAIN_1:41

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d holds
( cell l,r in cells d,G iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )

proof end;

theorem Th42: :: CHAIN_1:42

for d' being Nat
for d being non zero Nat
for G being Grating of d st d = d' + 1 holds
for A being Subset of (REAL d) holds
( A in cells d',G iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell l,r & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

proof end;

theorem :: CHAIN_1:43

for d' being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st d = d' + 1 holds
( cell l,r in cells d',G iff ex i0 being Element of Seg d st
( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

proof end;

theorem Th44: :: CHAIN_1:44

for d being non zero Nat
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells 1,G iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell l,r & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )

proof end;

theorem :: CHAIN_1:45

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d holds
( cell l,r in cells 1,G iff ex i0 being Element of Seg d st
( ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )

proof end;

theorem Th46: :: CHAIN_1:46

for k, k' being Nat
for d being non zero Nat
for l, r, l', r' being Element of REAL d
for G being Grating of d st k <= d & k' <= d & cell l,r in cells k,G & cell l',r' in cells k',G & cell l,r c= cell l',r' holds
for i being Element of Seg d holds
( ( l . i = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) or ( l . i <= r . i & r' . i < l' . i & r' . i <= l . i & r . i <= l' . i ) )

proof end;

theorem Th47: :: CHAIN_1:47

for k, k' being Nat
for d being non zero Nat
for l, r, l', r' being Element of REAL d
for G being Grating of d st k < k' & k' <= d & cell l,r in cells k,G & cell l',r' in cells k',G & cell l,r c= cell l',r' holds
ex i being Element of Seg d st
( ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) )

proof end;

theorem Th48: :: CHAIN_1:48

for d being non zero Nat
for l, r, l', r' being Element of REAL d
for G being Grating of d
for X, X' being Subset of (Seg d) st cell l,r c= cell l',r' & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) & ( for i being Element of Seg d holds
( ( i in X' & l' . i < r' . i & [(l' . i),(r' . i)] is Gap of G . i ) or ( not i in X' & l' . i = r' . i & l' . i in G . i ) ) ) holds
( X c= X' & ( for i being Element of Seg d st ( i in X or not i in X' ) holds
( l . i = l' . i & r . i = r' . i ) ) & ( for i being Element of Seg d st not i in X & i in X' & not ( l . i = l' . i & r . i = l' . i ) holds
( l . i = r' . i & r . i = r' . i ) ) )

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
mode Cell of k,G is Element of cells k,G;

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
mode Chain of k,G is Subset of (cells k,G);

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
func 0_ k,G -> Chain of k,G equals :: CHAIN_1:def 9
{} ;
coherence by SUBSET_1:4;

end;

:: deftheorem defines 0_ CHAIN_1:def 9 :

definition

let d be non zero Nat;
let G be Grating of d;
func Omega G -> Chain of d,G equals :: CHAIN_1:def 10
cells d,G;
coherence

proof end;

end;

:: deftheorem defines Omega CHAIN_1:def 10 :

notation

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C1, C2 be Chain of k,G;
synonym C1 + C2 for d \+\ G;

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C1, C2 be Chain of k,G;
:: original: +
redefine func C1 + C2 -> Chain of k,G;
coherence

proof end;

end;

definition

let d be non zero Nat;
let G be Grating of d;
func infinite-cell G -> Cell of d,G means :Def11: :: CHAIN_1:def 11
ex l, r being Element of REAL d st
( it = cell l,r & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines infinite-cell CHAIN_1:def 11 :

theorem Th49: :: CHAIN_1:49

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st cell l,r is Cell of d,G holds
( cell l,r = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )

proof end;

theorem Th50: :: CHAIN_1:50

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d holds
( cell l,r = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) )

proof end;

scheme :: CHAIN_1:sch 4
ChainInd{ F₁() -> non zero Nat, F₂() -> Grating of F₁(), F₃() -> Nat, F₄() -> Chain of F₃(),F₂(), P₁[ set ] } :

P₁[F₄()]

provided

A1: P₁[ 0_ F₃(),F₂()] and
A2: for A being Cell of F₃(),F₂() st A in F₄() holds
P₁[{A}] and
A3: for C1, C2 being Chain of F₃(),F₂() st C1 c= F₄() & C2 c= F₄() & P₁[C1] & P₁[C2] holds
P₁[C1 + C2]

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let A be Cell of k,G;
func star A -> Chain of (k + 1),G equals :: CHAIN_1:def 12
{ B where B is Cell of (k + 1),G : A c= B } ;
coherence

proof end;

end;

:: deftheorem defines star CHAIN_1:def 12 :

theorem Th51: :: CHAIN_1:51

for k being Nat
for d being non zero Nat
for G being Grating of d
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( B in star A iff A c= B )

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C be Chain of (k + 1),G;
func del C -> Chain of k,G equals :: CHAIN_1:def 13
{ A where A is Cell of k,G : ( k + 1 <= d & not card ((star A) /\ C) is even ) } ;
coherence

proof end;

end;

:: deftheorem defines del CHAIN_1:def 13 :

notation

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C be Chain of (k + 1),G;
synonym . C for del C;

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C be Chain of (k + 1),G;
let C' be Chain of k,G;
pred C' bounds C means :: CHAIN_1:def 14
C' = del C;

end;

:: deftheorem defines bounds CHAIN_1:def 14 :

theorem Th52: :: CHAIN_1:52

for k being Nat
for d being non zero Nat
for G being Grating of d
for A being Cell of k,G
for C being Chain of (k + 1),G holds
( A in del C iff ( k + 1 <= d & not card ((star A) /\ C) is even ) )

proof end;

theorem Th53: :: CHAIN_1:53

for k being Nat
for d being non zero Nat
for G being Grating of d st k + 1 > d holds
for C being Chain of (k + 1),G holds del C = 0_ k,G

proof end;

theorem Th54: :: CHAIN_1:54

for k being Nat
for d being non zero Nat
for G being Grating of d st k + 1 <= d holds
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )

proof end;

theorem Th55: :: CHAIN_1:55

for d' being Nat
for d being non zero Nat
for G being Grating of d st d = d' + 1 holds
for A being Cell of d',G holds card (star A) = 2

proof end;

theorem Th56: :: CHAIN_1:56

for d being non zero Nat
for G being Grating of d
for B being Cell of (0 + 1),G holds card (del {B}) = 2

proof end;

theorem :: CHAIN_1:57

for d being non zero Nat
for G being Grating of d holds
( Omega G = (0_ d,G) ` & 0_ d,G = (Omega G) ` )

proof end;

theorem :: CHAIN_1:58

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of k,G holds C + (0_ k,G) = C ;

theorem Th59: :: CHAIN_1:59

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of k,G holds C + C = 0_ k,G by XBOOLE_1:92;

theorem Th60: :: CHAIN_1:60

for d being non zero Nat
for G being Grating of d
for C being Chain of d,G holds C ` = C + (Omega G)

proof end;

theorem Th61: :: CHAIN_1:61

for k being Nat
for d being non zero Nat
for G being Grating of d holds del (0_ (k + 1),G) = 0_ k,G

proof end;

theorem Th62: :: CHAIN_1:62

for d' being Nat
for G being Grating of d' + 1 holds del (Omega G) = 0_ d',G

proof end;

theorem Th63: :: CHAIN_1:63

for k being Nat
for d being non zero Nat
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)

proof end;

theorem Th64: :: CHAIN_1:64

for d' being Nat
for G being Grating of d' + 1
for C being Chain of (d' + 1),G holds del (C ` ) = del C

proof end;

theorem Th65: :: CHAIN_1:65

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ k,G

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
mode Cycle of k,G -> Chain of k,G means :Def15: :: CHAIN_1:def 15
( ( k = 0 & card it is even ) or ex k' being Nat st
( k = k' + 1 & ex C being Chain of (k' + 1),G st
( C = it & del C = 0_ k',G ) ) );
existence

proof end;

end;

:: deftheorem Def15 defines Cycle CHAIN_1:def 15 :

theorem Th66: :: CHAIN_1:66

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of (k + 1),G holds
( C is Cycle of k + 1,G iff del C = 0_ k,G )

proof end;

theorem :: CHAIN_1:67

for k being Nat
for d being non zero Nat
for G being Grating of d st k > d holds
for C being Chain of k,G holds C is Cycle of k,G

proof end;

theorem Th68: :: CHAIN_1:68

for d being non zero Nat
for G being Grating of d
for C being Chain of 0,G holds
( C is Cycle of 0,G iff card C is even )

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C be Cycle of k + 1,G;
redefine func del C equals :: CHAIN_1:def 16
0_ k,G;
compatibility by Th66;

end;

:: deftheorem defines del CHAIN_1:def 16 :

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
:: original: 0_
redefine func 0_ k,G -> Cycle of k,G;
coherence

proof end;

end;

definition

let d be non zero Nat;
let G be Grating of d;
:: original: Omega
redefine func Omega G -> Cycle of d,G;
coherence

proof end;

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C1, C2 be Cycle of k,G;
:: original: +
redefine func C1 + C2 -> Cycle of k,G;
coherence

proof end;

end;

theorem :: CHAIN_1:69

for d being non zero Nat
for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G

proof end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C be Chain of (k + 1),G;
:: original: del
redefine func del C -> Cycle of k,G;
coherence

proof end;

end;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
func Chains k,G -> strict AbGroup means :Def17: :: CHAIN_1:def 17
( the carrier of it = bool (cells k,G) & 0. it = 0_ k,G & ( for A, B being Element of it
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines Chains CHAIN_1:def 17 :

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
mode GrChain of k,G is Element of (Chains k,G);

end;

theorem :: CHAIN_1:70

for k being Nat
for d being non zero Nat
for G being Grating of d
for x being set holds
( x is Chain of k,G iff x is GrChain of k,G ) by Def17;

definition

let d be non zero Nat;
let G be Grating of d;
let k be Nat;
func del k,G -> Homomorphism of Chains (k + 1),G, Chains k,G means :: CHAIN_1:def 18
for A being Element of (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
it . A = del A';
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines del CHAIN_1:def 18 :