let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let L be lower-bounded LATTICE; :: thesis: for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let O be Ordinal; :: thesis: for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let q be QuadrSeq of d; :: thesis: d c= ConsecutiveDelta (q,O)
defpred S₁[ Ordinal] means d c= ConsecutiveDelta (q,$1);
A1: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S₁[O1] ) holds
S₁[O2]

proof

deffunc H₁( 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₁[O1] ) implies S₁[O2] )
assume that
A2: O2 <> 0 and
A3: O2 is limit_ordinal and
for O1 being Ordinal st O1 in O2 holds
d c= ConsecutiveDelta (q,O1) ; :: thesis: S₁[O2]
A4: {} in O2 by A2, ORDINAL3:8;
consider Ls being Sequence such that
A5: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
Ls . {} = ConsecutiveDelta (q,{}) by A2, A5, ORDINAL3:8
.= d by Th26 ;
then A6: d in rng Ls by A5, A4, FUNCT_1:def 3;
ConsecutiveDelta (q,O2) = union (rng Ls) by A2, A3, A5, Th28;
hence S₁[O2] by A6, ZFMISC_1:74; :: thesis: verum

end;

A7: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
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 ;
then A8: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O1)) by Th19;
assume d c= ConsecutiveDelta (q,O1) ; :: thesis: S₁[ succ O1]
hence S₁[ succ O1] by A8, XBOOLE_1:1; :: thesis: verum

end;

A9: S₁[ 0 ] by Th26;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A9, A7, A1);
hence d c= ConsecutiveDelta (q,O) ; :: thesis: verum