let A be non empty set ; :: thesis: for L being lower-bounded LATTICE

for O being Ordinal

for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let L be lower-bounded LATTICE; :: thesis: for O being Ordinal

for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let O be Ordinal; :: thesis: for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric )

assume A1: d is symmetric ; :: thesis: for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let q be QuadrSeq of d; :: thesis: ConsecutiveDelta (q,O) is symmetric

defpred S_{1}[ Ordinal] means ConsecutiveDelta (q,$1) is symmetric ;

A2: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

S_{1}[O1] ) holds

S_{1}[O2]
_{1}[ 0 ]
_{1}[O]
from ORDINAL2:sch 1(A35, A2, A5);

hence ConsecutiveDelta (q,O) is symmetric ; :: thesis: verum

for O being Ordinal

for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let L be lower-bounded LATTICE; :: thesis: for O being Ordinal

for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let O be Ordinal; :: thesis: for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric )

assume A1: d is symmetric ; :: thesis: for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric

let q be QuadrSeq of d; :: thesis: ConsecutiveDelta (q,O) is symmetric

defpred S

A2: for O1 being Ordinal st S

S

proof

A5:
for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
let O1 be Ordinal; :: thesis: ( S_{1}[O1] implies S_{1}[ succ O1] )

assume ConsecutiveDelta (q,O1) is symmetric ; :: thesis: S_{1}[ succ O1]

then A3: new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) is symmetric by Th17;

let x, y be Element of ConsecutiveSet (A,(succ O1)); :: according to LATTICE5:def 5 :: thesis: (ConsecutiveDelta (q,(succ O1))) . (x,y) = (ConsecutiveDelta (q,(succ O1))) . (y,x)

reconsider x9 = x, y9 = y as Element of new_set (ConsecutiveSet (A,O1)) by Th22;

A4: ConsecutiveDelta (q,(succ O1)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),(Quadr (q,O1))) by Th27

.= new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) by Def15 ;

hence (ConsecutiveDelta (q,(succ O1))) . (x,y) = (new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (y9,x9) by A3

.= (ConsecutiveDelta (q,(succ O1))) . (y,x) by A4 ;

:: thesis: verum

end;assume ConsecutiveDelta (q,O1) is symmetric ; :: thesis: S

then A3: new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) is symmetric by Th17;

let x, y be Element of ConsecutiveSet (A,(succ O1)); :: according to LATTICE5:def 5 :: thesis: (ConsecutiveDelta (q,(succ O1))) . (x,y) = (ConsecutiveDelta (q,(succ O1))) . (y,x)

reconsider x9 = x, y9 = y as Element of new_set (ConsecutiveSet (A,O1)) by Th22;

A4: ConsecutiveDelta (q,(succ O1)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),(Quadr (q,O1))) by Th27

.= new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) by Def15 ;

hence (ConsecutiveDelta (q,(succ O1))) . (x,y) = (new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (y9,x9) by A3

.= (ConsecutiveDelta (q,(succ O1))) . (y,x) by A4 ;

:: thesis: verum

S

S

proof

A35:
S
deffunc H_{1}( Ordinal) -> BiFunction of (ConsecutiveSet (A,$1)),L = ConsecutiveDelta (q,$1);

let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds

S_{1}[O1] ) implies S_{1}[O2] )

assume that

A6: ( O2 <> 0 & O2 is limit_ordinal ) and

A7: for O1 being Ordinal st O1 in O2 holds

ConsecutiveDelta (q,O1) is symmetric ; :: thesis: S_{1}[O2]

set CS = ConsecutiveSet (A,O2);

consider Ls being Sequence such that

A8: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds

Ls . O1 = H_{1}(O1) ) )
from ORDINAL2:sch 2();

ConsecutiveDelta (q,O2) = union (rng Ls) by A6, A8, Th28;

then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet (A,O2)),L ;

deffunc H_{2}( Ordinal) -> set = ConsecutiveSet (A,$1);

consider Ts being Sequence such that

A9: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds

Ts . O1 = H_{2}(O1) ) )
from ORDINAL2:sch 2();

A10: ConsecutiveSet (A,O2) = union (rng Ts) by A6, A9, Th23;

f is symmetric_{1}[O2]
by A6, A8, Th28; :: thesis: verum

end;let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds

S

assume that

A6: ( O2 <> 0 & O2 is limit_ordinal ) and

A7: for O1 being Ordinal st O1 in O2 holds

ConsecutiveDelta (q,O1) is symmetric ; :: thesis: S

set CS = ConsecutiveSet (A,O2);

consider Ls being Sequence such that

A8: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds

Ls . O1 = H

ConsecutiveDelta (q,O2) = union (rng Ls) by A6, A8, Th28;

then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet (A,O2)),L ;

deffunc H

consider Ts being Sequence such that

A9: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds

Ts . O1 = H

A10: ConsecutiveSet (A,O2) = union (rng Ts) by A6, A9, Th23;

f is symmetric

proof

hence
S
let x, y be Element of ConsecutiveSet (A,O2); :: according to LATTICE5:def 5 :: thesis: f . (x,y) = f . (y,x)

consider x1 being set such that

A11: x in x1 and

A12: x1 in rng Ts by A10, TARSKI:def 4;

consider o1 being object such that

A13: o1 in dom Ts and

A14: x1 = Ts . o1 by A12, FUNCT_1:def 3;

consider y1 being set such that

A15: y in y1 and

A16: y1 in rng Ts by A10, TARSKI:def 4;

consider o2 being object such that

A17: o2 in dom Ts and

A18: y1 = Ts . o2 by A16, FUNCT_1:def 3;

reconsider o1 = o1, o2 = o2 as Ordinal by A13, A17;

A19: x in ConsecutiveSet (A,o1) by A9, A11, A13, A14;

A20: Ls . o1 = ConsecutiveDelta (q,o1) by A8, A9, A13;

then reconsider h1 = Ls . o1 as BiFunction of (ConsecutiveSet (A,o1)),L ;

A21: h1 is symmetric

A24: y in ConsecutiveSet (A,o2) by A9, A15, A17, A18;

A25: Ls . o2 = ConsecutiveDelta (q,o2) by A8, A9, A17;

then reconsider h2 = Ls . o2 as BiFunction of (ConsecutiveSet (A,o2)),L ;

A26: h2 is symmetric

end;consider x1 being set such that

A11: x in x1 and

A12: x1 in rng Ts by A10, TARSKI:def 4;

consider o1 being object such that

A13: o1 in dom Ts and

A14: x1 = Ts . o1 by A12, FUNCT_1:def 3;

consider y1 being set such that

A15: y in y1 and

A16: y1 in rng Ts by A10, TARSKI:def 4;

consider o2 being object such that

A17: o2 in dom Ts and

A18: y1 = Ts . o2 by A16, FUNCT_1:def 3;

reconsider o1 = o1, o2 = o2 as Ordinal by A13, A17;

A19: x in ConsecutiveSet (A,o1) by A9, A11, A13, A14;

A20: Ls . o1 = ConsecutiveDelta (q,o1) by A8, A9, A13;

then reconsider h1 = Ls . o1 as BiFunction of (ConsecutiveSet (A,o1)),L ;

A21: h1 is symmetric

proof

A23:
dom h1 = [:(ConsecutiveSet (A,o1)),(ConsecutiveSet (A,o1)):]
by FUNCT_2:def 1;
let x, y be Element of ConsecutiveSet (A,o1); :: according to LATTICE5:def 5 :: thesis: h1 . (x,y) = h1 . (y,x)

A22: ConsecutiveDelta (q,o1) is symmetric by A7, A9, A13;

thus h1 . (x,y) = (ConsecutiveDelta (q,o1)) . (x,y) by A8, A9, A13

.= (ConsecutiveDelta (q,o1)) . (y,x) by A22

.= h1 . (y,x) by A8, A9, A13 ; :: thesis: verum

end;A22: ConsecutiveDelta (q,o1) is symmetric by A7, A9, A13;

thus h1 . (x,y) = (ConsecutiveDelta (q,o1)) . (x,y) by A8, A9, A13

.= (ConsecutiveDelta (q,o1)) . (y,x) by A22

.= h1 . (y,x) by A8, A9, A13 ; :: thesis: verum

A24: y in ConsecutiveSet (A,o2) by A9, A15, A17, A18;

A25: Ls . o2 = ConsecutiveDelta (q,o2) by A8, A9, A17;

then reconsider h2 = Ls . o2 as BiFunction of (ConsecutiveSet (A,o2)),L ;

A26: h2 is symmetric

proof

A28:
dom h2 = [:(ConsecutiveSet (A,o2)),(ConsecutiveSet (A,o2)):]
by FUNCT_2:def 1;
let x, y be Element of ConsecutiveSet (A,o2); :: according to LATTICE5:def 5 :: thesis: h2 . (x,y) = h2 . (y,x)

A27: ConsecutiveDelta (q,o2) is symmetric by A7, A9, A17;

thus h2 . (x,y) = (ConsecutiveDelta (q,o2)) . (x,y) by A8, A9, A17

.= (ConsecutiveDelta (q,o2)) . (y,x) by A27

.= h2 . (y,x) by A8, A9, A17 ; :: thesis: verum

end;A27: ConsecutiveDelta (q,o2) is symmetric by A7, A9, A17;

thus h2 . (x,y) = (ConsecutiveDelta (q,o2)) . (x,y) by A8, A9, A17

.= (ConsecutiveDelta (q,o2)) . (y,x) by A27

.= h2 . (y,x) by A8, A9, A17 ; :: thesis: verum

per cases
( o1 c= o2 or o2 c= o1 )
;

end;

suppose
o1 c= o2
; :: thesis: f . (x,y) = f . (y,x)

then A29:
ConsecutiveSet (A,o1) c= ConsecutiveSet (A,o2)
by Th29;

then A30: [y,x] in dom h2 by A19, A24, A28, ZFMISC_1:87;

ConsecutiveDelta (q,o2) in rng Ls by A8, A9, A17, A25, FUNCT_1:def 3;

then A31: h2 c= f by A25, ZFMISC_1:74;

reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o2) by A9, A15, A17, A18, A19, A29;

[x,y] in dom h2 by A19, A24, A28, A29, ZFMISC_1:87;

hence f . (x,y) = h2 . (x9,y9) by A31, GRFUNC_1:2

.= h2 . (y9,x9) by A26

.= f . (y,x) by A31, A30, GRFUNC_1:2 ;

:: thesis: verum

end;then A30: [y,x] in dom h2 by A19, A24, A28, ZFMISC_1:87;

ConsecutiveDelta (q,o2) in rng Ls by A8, A9, A17, A25, FUNCT_1:def 3;

then A31: h2 c= f by A25, ZFMISC_1:74;

reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o2) by A9, A15, A17, A18, A19, A29;

[x,y] in dom h2 by A19, A24, A28, A29, ZFMISC_1:87;

hence f . (x,y) = h2 . (x9,y9) by A31, GRFUNC_1:2

.= h2 . (y9,x9) by A26

.= f . (y,x) by A31, A30, GRFUNC_1:2 ;

:: thesis: verum

suppose
o2 c= o1
; :: thesis: f . (x,y) = f . (y,x)

then A32:
ConsecutiveSet (A,o2) c= ConsecutiveSet (A,o1)
by Th29;

then A33: [y,x] in dom h1 by A19, A24, A23, ZFMISC_1:87;

ConsecutiveDelta (q,o1) in rng Ls by A8, A9, A13, A20, FUNCT_1:def 3;

then A34: h1 c= f by A20, ZFMISC_1:74;

reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o1) by A9, A11, A13, A14, A24, A32;

[x,y] in dom h1 by A19, A24, A23, A32, ZFMISC_1:87;

hence f . (x,y) = h1 . (x9,y9) by A34, GRFUNC_1:2

.= h1 . (y9,x9) by A21

.= f . (y,x) by A34, A33, GRFUNC_1:2 ;

:: thesis: verum

end;then A33: [y,x] in dom h1 by A19, A24, A23, ZFMISC_1:87;

ConsecutiveDelta (q,o1) in rng Ls by A8, A9, A13, A20, FUNCT_1:def 3;

then A34: h1 c= f by A20, ZFMISC_1:74;

reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o1) by A9, A11, A13, A14, A24, A32;

[x,y] in dom h1 by A19, A24, A23, A32, ZFMISC_1:87;

hence f . (x,y) = h1 . (x9,y9) by A34, GRFUNC_1:2

.= h1 . (y9,x9) by A21

.= f . (y,x) by A34, A33, GRFUNC_1:2 ;

:: thesis: verum

proof

for O being Ordinal holds S
let x, y be Element of ConsecutiveSet (A,0); :: according to LATTICE5:def 5 :: thesis: (ConsecutiveDelta (q,0)) . (x,y) = (ConsecutiveDelta (q,0)) . (y,x)

reconsider x9 = x, y9 = y as Element of A by Th21;

thus (ConsecutiveDelta (q,0)) . (x,y) = d . (x9,y9) by Th26

.= d . (y9,x9) by A1

.= (ConsecutiveDelta (q,0)) . (y,x) by Th26 ; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of A by Th21;

thus (ConsecutiveDelta (q,0)) . (x,y) = d . (x9,y9) by Th26

.= d . (y9,x9) by A1

.= (ConsecutiveDelta (q,0)) . (y,x) by Th26 ; :: thesis: verum

hence ConsecutiveDelta (q,O) is symmetric ; :: thesis: verum