let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric
let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric )
assume A1: d is symmetric ; :: thesis: for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric
let q be QuadrSeq of d; :: thesis: for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric
let O be Ordinal; :: thesis: ConsecutiveDelta2 (q,O) is symmetric
defpred S₁[ Ordinal] means ConsecutiveDelta2 (q,$1) is symmetric ;
A2: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume ConsecutiveDelta2 (q,O1) is symmetric ; :: thesis: S₁[ succ O1]
then A3: new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1))) is symmetric by Th11;
let x, y be Element of ConsecutiveSet2 (A,(succ O1)); :: according to LATTICE5:def 5 :: thesis: (ConsecutiveDelta2 (q,(succ O1))) . (x,y) = (ConsecutiveDelta2 (q,(succ O1))) . (y,x)
reconsider x9 = x, y9 = y as Element of new_set2 (ConsecutiveSet2 (A,O1)) by Th15;
A4: ConsecutiveDelta2 (q,(succ O1)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O1)),(ConsecutiveSet2 (A,O1)),L)),(Quadr2 (q,O1))) by Th19
.= new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1))) by LATTICE5:def 15 ;
hence (ConsecutiveDelta2 (q,(succ O1))) . (x,y) = (new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (y9,x9) by A3
.= (ConsecutiveDelta2 (q,(succ O1))) . (y,x) by A4 ;
:: thesis: verum

end;

A5: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

proof

deffunc H₁( Ordinal) -> BiFunction of (ConsecutiveSet2 (A,$1)),L = ConsecutiveDelta2 (q,$1);
let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S₁[O2] ) implies S₁[O2] )
assume that
A6: ( O2 <> 0 & O2 is limit_ordinal ) and
A7: for O1 being Ordinal st O1 in O2 holds
ConsecutiveDelta2 (q,O1) is symmetric ; :: thesis: S₁[O2]
set CS = ConsecutiveSet2 (A,O2);
consider Ls being Sequence such that
A8: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
ConsecutiveDelta2 (q,O2) = union (rng Ls) by A6, A8, Th20;
then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet2 (A,O2)),L ;
deffunc H₂( Ordinal) -> set = ConsecutiveSet2 (A,$1);
consider Ts being Sequence such that
A9: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ts . O1 = H₂(O1) ) ) from ORDINAL2:sch 2();
A10: ConsecutiveSet2 (A,O2) = union (rng Ts) by A6, A9, Th16;
f is symmetric

proof

let x, y be Element of ConsecutiveSet2 (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 ConsecutiveSet2 (A,o1) by A9, A11, A13, A14;
A20: Ls . o1 = ConsecutiveDelta2 (q,o1) by A8, A9, A13;
then reconsider h1 = Ls . o1 as BiFunction of (ConsecutiveSet2 (A,o1)),L ;
A21: h1 is symmetric

proof

let x, y be Element of ConsecutiveSet2 (A,o1); :: according to LATTICE5:def 5 :: thesis: h1 . (x,y) = h1 . (y,x)
A22: ConsecutiveDelta2 (q,o1) is symmetric by A7, A9, A13;
thus h1 . (x,y) = (ConsecutiveDelta2 (q,o1)) . (x,y) by A8, A9, A13
.= (ConsecutiveDelta2 (q,o1)) . (y,x) by A22
.= h1 . (y,x) by A8, A9, A13 ; :: thesis: verum

end;

A23: dom h1 = [:(ConsecutiveSet2 (A,o1)),(ConsecutiveSet2 (A,o1)):] by FUNCT_2:def 1;
A24: y in ConsecutiveSet2 (A,o2) by A9, A15, A17, A18;
A25: Ls . o2 = ConsecutiveDelta2 (q,o2) by A8, A9, A17;
then reconsider h2 = Ls . o2 as BiFunction of (ConsecutiveSet2 (A,o2)),L ;
A26: h2 is symmetric

proof

let x, y be Element of ConsecutiveSet2 (A,o2); :: according to LATTICE5:def 5 :: thesis: h2 . (x,y) = h2 . (y,x)
A27: ConsecutiveDelta2 (q,o2) is symmetric by A7, A9, A17;
thus h2 . (x,y) = (ConsecutiveDelta2 (q,o2)) . (x,y) by A8, A9, A17
.= (ConsecutiveDelta2 (q,o2)) . (y,x) by A27
.= h2 . (y,x) by A8, A9, A17 ; :: thesis: verum

end;

A28: dom h2 = [:(ConsecutiveSet2 (A,o2)),(ConsecutiveSet2 (A,o2)):] by FUNCT_2:def 1;

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

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

then A29: ConsecutiveSet2 (A,o1) c= ConsecutiveSet2 (A,o2) by Th21;
then A30: [y,x] in dom h2 by A19, A24, A28, ZFMISC_1:87;
ConsecutiveDelta2 (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 ConsecutiveSet2 (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;

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

then A32: ConsecutiveSet2 (A,o2) c= ConsecutiveSet2 (A,o1) by Th21;
then A33: [y,x] in dom h1 by A19, A24, A23, ZFMISC_1:87;
ConsecutiveDelta2 (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 ConsecutiveSet2 (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;

end;

end;

hence S₁[O2] by A6, A8, Th20; :: thesis: verum

end;

A35: S₁[ 0 ]

proof

let x, y be Element of ConsecutiveSet2 (A,0); :: according to LATTICE5:def 5 :: thesis: (ConsecutiveDelta2 (q,0)) . (x,y) = (ConsecutiveDelta2 (q,0)) . (y,x)
reconsider x9 = x, y9 = y as Element of A by Th14;
thus (ConsecutiveDelta2 (q,0)) . (x,y) = d . (x9,y9) by Th18
.= d . (y9,x9) by A1
.= (ConsecutiveDelta2 (q,0)) . (y,x) by Th18 ; :: thesis: verum

end;

for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A35, A2, A5);
hence ConsecutiveDelta2 (q,O) is symmetric ; :: thesis: verum