let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let d be BiFunction of A,L; :: thesis: ( d is zeroed implies for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed )
assume A1: d is zeroed ; :: thesis: for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let q be QuadrSeq of d; :: thesis: for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let O be Ordinal; :: thesis: ConsecutiveDelta2 (q,O) is zeroed
defpred S₁[ Ordinal] means ConsecutiveDelta2 (q,$1) is zeroed ;
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 zeroed ; :: thesis: S₁[ succ O1]
then A3: new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1))) is zeroed by Th10;
let z be Element of ConsecutiveSet2 (A,(succ O1)); :: according to LATTICE5:def 6 :: thesis: (ConsecutiveDelta2 (q,(succ O1))) . (z,z) = Bottom L
reconsider z9 = z as Element of new_set2 (ConsecutiveSet2 (A,O1)) by Th15;
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))) . (z,z) = (new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (z9,z9)
.= Bottom L by A3 ;
:: thesis: verum

end;

A4: 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
A5: ( O2 <> 0 & O2 is limit_ordinal ) and
A6: for O1 being Ordinal st O1 in O2 holds
ConsecutiveDelta2 (q,O1) is zeroed ; :: thesis: S₁[O2]
set CS = ConsecutiveSet2 (A,O2);
consider Ls being Sequence such that
A7: ( 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 A5, A7, 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
A8: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ts . O1 = H₂(O1) ) ) from ORDINAL2:sch 2();
A9: ConsecutiveSet2 (A,O2) = union (rng Ts) by A5, A8, Th16;
f is zeroed

proof

let x be Element of ConsecutiveSet2 (A,O2); :: according to LATTICE5:def 6 :: thesis: f . (x,x) = Bottom L
consider y being set such that
A10: x in y and
A11: y in rng Ts by A9, TARSKI:def 4;
consider o being object such that
A12: o in dom Ts and
A13: y = Ts . o by A11, FUNCT_1:def 3;
reconsider o = o as Ordinal by A12;
A14: Ls . o = ConsecutiveDelta2 (q,o) by A7, A8, A12;
then reconsider h = Ls . o as BiFunction of (ConsecutiveSet2 (A,o)),L ;
reconsider x9 = x as Element of ConsecutiveSet2 (A,o) by A8, A10, A12, A13;
A15: dom h = [:(ConsecutiveSet2 (A,o)),(ConsecutiveSet2 (A,o)):] by FUNCT_2:def 1;
A16: h is zeroed

proof

let z be Element of ConsecutiveSet2 (A,o); :: according to LATTICE5:def 6 :: thesis: h . (z,z) = Bottom L
A17: ConsecutiveDelta2 (q,o) is zeroed by A6, A8, A12;
thus h . (z,z) = (ConsecutiveDelta2 (q,o)) . (z,z) by A7, A8, A12
.= Bottom L by A17 ; :: thesis: verum

end;

ConsecutiveDelta2 (q,o) in rng Ls by A7, A8, A12, A14, FUNCT_1:def 3;
then A18: h c= f by A14, ZFMISC_1:74;
x in ConsecutiveSet2 (A,o) by A8, A10, A12, A13;
then [x,x] in dom h by A15, ZFMISC_1:87;
hence f . (x,x) = h . (x9,x9) by A18, GRFUNC_1:2
.= Bottom L by A16 ;
:: thesis: verum

end;

hence S₁[O2] by A5, A7, Th20; :: thesis: verum

end;

A19: S₁[ 0 ]

proof

let z be Element of ConsecutiveSet2 (A,0); :: according to LATTICE5:def 6 :: thesis: (ConsecutiveDelta2 (q,0)) . (z,z) = Bottom L
reconsider z9 = z as Element of A by Th14;
thus (ConsecutiveDelta2 (q,0)) . (z,z) = d . (z9,z9) by Th18
.= Bottom L by A1 ; :: thesis: verum

end;

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