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

let O1 be Ordinal; :: thesis:
assume ConsecutiveDelta (q,O1) is BiFunction of (ConsecutiveSet (A,O1)),L ; :: thesis:
then reconsider CD = ConsecutiveDelta (q,O1) as BiFunction of (ConsecutiveSet (A,O1)),L ;
A2: ConsecutiveSet (A,(succ O1)) = new_set (ConsecutiveSet (A,O1)) by Th22;
ConsecutiveDelta (q,(succ O1)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),(Quadr (q,O1))) by Th27
.= new_bi_fun (CD,(Quadr (q,O1))) by Def15 ;
hence S₁[ succ O1] by A2; :: thesis:

end;

A3: 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) -> set = ConsecutiveDelta (q,$1);
let O1 be Ordinal; :: thesis:
assume that
A4: O1 <> 0 and
A5: O1 is limit_ordinal and
A6: for O2 being Ordinal st O2 in O1 holds
ConsecutiveDelta (q,O2) is BiFunction of (ConsecutiveSet (A,O2)),L ; :: thesis:
consider Ls being Sequence such that
A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H₁(O2) ) ) from ORDINAL2:sch 2();
A8: for O, O2 being Ordinal st O c= O2 & O2 in dom Ls holds
Ls . O c= Ls . O2

proof

let O be Ordinal; :: thesis:
defpred S₂[ Ordinal] means ( O c= $1 & $1 in dom Ls implies Ls . O c= Ls . $1 );
A9: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₂[O3] ) holds
S₂[O2]

proof

deffunc H₂( Ordinal) -> set = ConsecutiveDelta (q,$1);
let O2 be Ordinal; :: thesis:
assume that
A10: ( O2 <> 0 & O2 is limit_ordinal ) and
for O3 being Ordinal st O3 in O2 & O c= O3 & O3 in dom Ls holds
Ls . O c= Ls . O3 ; :: thesis:
assume that
A11: O c= O2 and
A12: O2 in dom Ls ; :: thesis:
consider Lt being Sequence such that
A13: ( dom Lt = O2 & ( for O3 being Ordinal st O3 in O2 holds
Lt . O3 = H₂(O3) ) ) from ORDINAL2:sch 2();
A14: Ls . O2 = ConsecutiveDelta (q,O2) by A7, A12
.= union (rng Lt) by A10, A13, Th28 ;

per cases ;

suppose O = O2 ; :: thesis:

hence Ls . O c= Ls . O2 ; :: thesis:

end;

suppose O <> O2 ; :: thesis:

then A15: O c< O2 by A11;
then A16: O in O2 by ORDINAL1:11;
then Ls . O = ConsecutiveDelta (q,O) by A7, A12, ORDINAL1:10
.= Lt . O by A13, A15, ORDINAL1:11 ;
then Ls . O in rng Lt by A13, A16, FUNCT_1:def 3;
hence Ls . O c= Ls . O2 by A14, ZFMISC_1:74; :: thesis:

end;

A17: for O2 being Ordinal st S₂[O2] holds
S₂[ succ O2]

proof

let O2 be Ordinal; :: thesis:
assume A18: ( O c= O2 & O2 in dom Ls implies Ls . O c= Ls . O2 ) ; :: thesis:
assume that
A19: O c= succ O2 and
A20: succ O2 in dom Ls ; :: thesis:

per cases ;

suppose O = succ O2 ; :: thesis:

hence Ls . O c= Ls . (succ O2) ; :: thesis:

end;

suppose O <> succ O2 ; :: thesis:

then O c< succ O2 by A19;
then A21: O in succ O2 by ORDINAL1:11;
A22: O2 in succ O2 by ORDINAL1:6;
then O2 in dom Ls by A20, ORDINAL1:10;
then reconsider cd2 = ConsecutiveDelta (q,O2) as BiFunction of (ConsecutiveSet (A,O2)),L by A6, A7;
Ls . (succ O2) = ConsecutiveDelta (q,(succ O2)) by A7, A20
.= new_bi_fun ((BiFun ((ConsecutiveDelta (q,O2)),(ConsecutiveSet (A,O2)),L)),(Quadr (q,O2))) by Th27
.= new_bi_fun (cd2,(Quadr (q,O2))) by Def15 ;
then ConsecutiveDelta (q,O2) c= Ls . (succ O2) by Th19;
then Ls . O2 c= Ls . (succ O2) by A7, A20, A22, ORDINAL1:10;
hence Ls . O c= Ls . (succ O2) by A18, A20, A21, A22, ORDINAL1:10, ORDINAL1:22; :: thesis:

end;

A23: S₂[ 0 ] ;
thus for O2 being Ordinal holds S₂[O2] from ORDINAL2:sch 1(A23, A17, A9); :: thesis:

end;

for x, y being set st x in rng Ls & y in rng Ls holds
x,y are_c=-comparable

proof

let x, y be set ; :: thesis:
assume that
A24: x in rng Ls and
A25: y in rng Ls ; :: thesis:
consider o1 being object such that
A26: o1 in dom Ls and
A27: Ls . o1 = x by A24, FUNCT_1:def 3;
consider o2 being object such that
A28: o2 in dom Ls and
A29: Ls . o2 = y by A25, FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A26, A28;
( o19 c= o29 or o29 c= o19 ) ;
then ( x c= y or y c= x ) by A8, A26, A27, A28, A29;
hence x,y are_c=-comparable ; :: thesis:

end;

then A30: rng Ls is c=-linear ;
set Y = the carrier of L;
set X = [:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):];
set f = union (rng Ls);
rng Ls c= PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng Ls ; :: thesis:
then consider o being object such that
A31: o in dom Ls and
A32: z = Ls . o by FUNCT_1:def 3;
reconsider o = o as Ordinal by A31;
Ls . o = ConsecutiveDelta (q,o) by A7, A31;
then reconsider h = Ls . o as BiFunction of (ConsecutiveSet (A,o)),L by A6, A7, A31;
o c= O1 by A7, A31, ORDINAL1:def 2;
then ( dom h = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):] & ConsecutiveSet (A,o) c= ConsecutiveSet (A,O1) ) by Th29, FUNCT_2:def 1;
then ( rng h c= the carrier of L & dom h c= [:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] ) by ZFMISC_1:96;
hence z in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L) by A32, PARTFUN1:def 3; :: thesis:

end;

then union (rng Ls) in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L) by A30, TREES_2:40;
then A33: ex g being Function st
( union (rng Ls) = g & dom g c= [:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] & rng g c= the carrier of L ) by PARTFUN1:def 3;
reconsider o1 = O1 as non empty Ordinal by A4;
set YY = { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ;
deffunc H₂( Ordinal) -> set = ConsecutiveSet (A,$1);
consider Ts being Sequence such that
A34: ( dom Ts = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ts . O2 = H₂(O2) ) ) from ORDINAL2:sch 2();
Ls is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume A35: x in dom Ls ; :: thesis:
then reconsider o = x as Ordinal ;
Ls . o = ConsecutiveDelta (q,o) by A7, A35;
hence Ls . x is set by A6, A7, A35; :: thesis:

end;

then reconsider LsF = Ls as Function-yielding Function ;
A36: rng (doms LsF) = { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }

proof

thus rng (doms LsF) c= { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } :: according to XBOOLE_0:def 10 :: thesis:

proof

let Z be object ; :: according to TARSKI:def 3 :: thesis:
assume Z in rng (doms LsF) ; :: thesis:
then consider o being object such that
A37: o in dom (doms LsF) and
A38: Z = (doms LsF) . o by FUNCT_1:def 3;
A39: o in dom LsF by A37, FUNCT_6:59;
then reconsider o9 = o as Element of o1 by A7;
Ls . o9 = ConsecutiveDelta (q,o9) by A7;
then reconsider ls = Ls . o9 as BiFunction of (ConsecutiveSet (A,o9)),L by A6;
Z = dom ls by A38, A39, FUNCT_6:22
.= [:(ConsecutiveSet (A,o9)),(ConsecutiveSet (A,o9)):] by FUNCT_2:def 1 ;
hence Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ; :: thesis:

end;

let Z be object ; :: according to TARSKI:def 3 :: thesis:
assume Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ; :: thesis:
then consider o being Element of o1 such that
A40: Z = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):] ;
Ls . o = ConsecutiveDelta (q,o) by A7;
then reconsider ls = Ls . o as BiFunction of (ConsecutiveSet (A,o)),L by A6;
o in dom LsF by A7;
then A41: o in dom (doms LsF) by FUNCT_6:59;
Z = dom ls by A40, FUNCT_2:def 1
.= (doms LsF) . o by A7, FUNCT_6:22 ;
hence Z in rng (doms LsF) by A41, FUNCT_1:def 3; :: thesis:

end;

{} in O1 by A4, ORDINAL3:8;
then reconsider RTs = rng Ts as non empty set by A34, FUNCT_1:3;
reconsider f = union (rng Ls) as Function by A33;
A42: dom f = union (rng (doms LsF)) by Th1;
A43: { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } = { [:a,a:] where a is Element of RTs : a in RTs }

proof

set XX = { [:a,a:] where a is Element of RTs : a in RTs } ;
thus { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } c= { [:a,a:] where a is Element of RTs : a in RTs } :: according to XBOOLE_0:def 10 :: thesis:

proof

let Z be object ; :: according to TARSKI:def 3 :: thesis:
assume Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ; :: thesis:
then consider o being Element of o1 such that
A44: Z = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):] ;
Ts . o = ConsecutiveSet (A,o) by A34;
then reconsider CoS = ConsecutiveSet (A,o) as Element of RTs by A34, FUNCT_1:def 3;
Z = [:CoS,CoS:] by A44;
hence Z in { [:a,a:] where a is Element of RTs : a in RTs } ; :: thesis:

end;

let Z be object ; :: according to TARSKI:def 3 :: thesis:
assume Z in { [:a,a:] where a is Element of RTs : a in RTs } ; :: thesis:
then consider a being Element of RTs such that
A45: Z = [:a,a:] and
a in RTs ;
consider o being object such that
A46: o in dom Ts and
A47: a = Ts . o by FUNCT_1:def 3;
reconsider o9 = o as Ordinal by A46;
a = ConsecutiveSet (A,o9) by A34, A46, A47;
hence Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } by A34, A45, A46; :: thesis:

end;

for x, y being set st x in RTs & y in RTs holds
x,y are_c=-comparable

proof

let x, y be set ; :: thesis:
assume that
A48: x in RTs and
A49: y in RTs ; :: thesis:
consider o1 being object such that
A50: o1 in dom Ts and
A51: Ts . o1 = x by A48, FUNCT_1:def 3;
consider o2 being object such that
A52: o2 in dom Ts and
A53: Ts . o2 = y by A49, FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A50, A52;
A54: Ts . o29 = ConsecutiveSet (A,o29) by A34, A52;
A55: ( o19 c= o29 or o29 c= o19 ) ;
Ts . o19 = ConsecutiveSet (A,o19) by A34, A50;
then ( x c= y or y c= x ) by A51, A53, A54, A55, Th29;
hence x,y are_c=-comparable ; :: thesis:

end;

then A56: RTs is c=-linear ;
A57: ConsecutiveDelta (q,O1) = union (rng Ls) by A4, A5, A7, Th28;
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] = [:(union (rng Ts)),(ConsecutiveSet (A,O1)):] by A4, A5, A34, Th23
.= [:(union RTs),(union RTs):] by A4, A5, A34, Th23
.= dom f by A42, A36, A56, A43, Th3 ;
hence S₁[O1] by A57, A33, FUNCT_2:def 1, RELSET_1:4; :: thesis:

end;

ConsecutiveSet (A,{}) = A by Th21;
then A58: S₁[ 0 ] by Th26;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A58, A1, A3);
hence ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L ; :: thesis: