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 S1[ Ordinal] means ConsecutiveDelta (q,\$1) is symmetric ;
A2: for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be Ordinal; :: thesis: ( S1[O1] implies S1[ succ O1] )
assume ConsecutiveDelta (q,O1) is symmetric ; :: thesis: S1[ 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;
A5: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) holds
S1[O2]
proof
deffunc H1( 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
S1[O1] ) implies S1[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: S1[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 = H1(O1) ) ) from ConsecutiveDelta (q,O2) = union (rng Ls) by A6, A8, Th28;
then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet (A,O2)),L ;
deffunc H2( 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 = H2(O1) ) ) from A10: ConsecutiveSet (A,O2) = union (rng Ts) by A6, A9, Th23;
f is symmetric
proof
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 ;
consider o1 being object such that
A13: o1 in dom Ts and
A14: x1 = Ts . o1 by ;
consider y1 being set such that
A15: y in y1 and
A16: y1 in rng Ts by ;
consider o2 being object such that
A17: o2 in dom Ts and
A18: y1 = Ts . o2 by ;
reconsider o1 = o1, o2 = o2 as Ordinal by ;
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
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;
A23: dom h1 = [:(ConsecutiveSet (A,o1)),(ConsecutiveSet (A,o1)):] by FUNCT_2:def 1;
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
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;
A28: dom h2 = [:(ConsecutiveSet (A,o2)),(ConsecutiveSet (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: ConsecutiveSet (A,o1) c= ConsecutiveSet (A,o2) by Th29;
then A30: [y,x] in dom h2 by ;
ConsecutiveDelta (q,o2) in rng Ls by ;
then A31: h2 c= f by ;
reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o2) by A9, A15, A17, A18, A19, A29;
[x,y] in dom h2 by ;
hence f . (x,y) = h2 . (x9,y9) by
.= h2 . (y9,x9) by A26
.= f . (y,x) by ;
:: thesis: verum
end;
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 ;
ConsecutiveDelta (q,o1) in rng Ls by ;
then A34: h1 c= f by ;
reconsider x9 = x, y9 = y as Element of ConsecutiveSet (A,o1) by A9, A11, A13, A14, A24, A32;
[x,y] in dom h1 by ;
hence f . (x,y) = h1 . (x9,y9) by
.= h1 . (y9,x9) by A21
.= f . (y,x) by ;
:: thesis: verum
end;
end;
end;
hence S1[O2] by A6, A8, Th28; :: thesis: verum
end;
A35: S1[ 0 ]
proof
let x, y be Element of ConsecutiveSet (A,0); :: according to LATTICE5:def 5 :: thesis: () . (x,y) = () . (y,x)
reconsider x9 = x, y9 = y as Element of A by Th21;
thus () . (x,y) = d . (x9,y9) by Th26
.= d . (y9,x9) by A1
.= () . (y,x) by Th26 ; :: thesis: verum
end;
for O being Ordinal holds S1[O] from hence ConsecutiveDelta (q,O) is symmetric ; :: thesis: verum