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 ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
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 ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let O be Ordinal; :: thesis: for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let q be QuadrSeq of d; :: thesis: ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
defpred S1[ Ordinal] means ConsecutiveDelta (q,$1) is BiFunction of (ConsecutiveSet (A,$1)),L;
A1: 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 BiFunction of (ConsecutiveSet (A,O1)),L ; :: thesis: S1[ succ O1]
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 S1[ succ O1] by A2; :: thesis: verum
end;
A3: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
deffunc H1( Ordinal) -> set = ConsecutiveDelta (q,$1);
let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
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: S1[O1]
consider Ls being Sequence such that
A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(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: for O2 being Ordinal st O c= O2 & O2 in dom Ls holds
Ls . O c= Ls . O2
defpred S2[ 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
S2[O3] ) holds
S2[O2]
proof
deffunc H2( Ordinal) -> set = ConsecutiveDelta (q,$1);
let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S2[O3] ) implies S2[O2] )
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: S2[O2]
assume that
A11: O c= O2 and
A12: O2 in dom Ls ; :: thesis: Ls . O c= Ls . O2
consider Lt being Sequence such that
A13: ( dom Lt = O2 & ( for O3 being Ordinal st O3 in O2 holds
Lt . O3 = H2(O3) ) ) from ORDINAL2:sch 2();
 A14: Ls . O2 = ConsecutiveDelta (q,O2) by A7, A12
.= union (rng Lt) by A10, A13, Th28 ;
per cases ( O = O2 or O <> O2 ) ;
suppose O = O2 ; :: thesis: Ls . O c= Ls . O2
hence Ls . O c= Ls . O2 ; :: thesis: verum
end;
suppose O <> O2 ; :: thesis: Ls . O c= Ls . O2
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: verum
end;
end;
end;
A17: for O2 being Ordinal st S2[O2] holds
S2[ succ O2]
proof
let O2 be Ordinal; :: thesis: ( S2[O2] implies S2[ succ O2] )
assume A18: ( O c= O2 & O2 in dom Ls implies Ls . O c= Ls . O2 ) ; :: thesis: S2[ succ O2]
assume that
A19: O c= succ O2 and
A20: succ O2 in dom Ls ; :: thesis: Ls . O c= Ls . (succ O2)
per cases ( O = succ O2 or O <> succ O2 ) ;
suppose O = succ O2 ; :: thesis: Ls . O c= Ls . (succ O2)
hence Ls . O c= Ls . (succ O2) ; :: thesis: verum
end;
suppose O <> succ O2 ; :: thesis: Ls . O c= Ls . (succ O2)
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: verum
end;
end;
end;
A23: S2[ 0 ] ;
thus for O2 being Ordinal holds S2[O2] from ORDINAL2:sch 1(A23, A17, A9); :: thesis: verum
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: ( x in rng Ls & y in rng Ls implies x,y are_c=-comparable )
assume that
A24: x in rng Ls and
A25: y in rng Ls ; :: thesis: x,y are_c=-comparable
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: verum
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: ( not z in rng Ls or z in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L) )
assume z in rng Ls ; :: thesis: z in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L)
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: verum
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 H2( 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 = H2(O2) ) ) from ORDINAL2:sch 2();
 Ls is Function-yielding
proof
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 Ls or Ls . x is set )
assume A35: x in dom Ls ; :: thesis: Ls . x is set
then reconsider o = x as Ordinal ;
Ls . o = ConsecutiveDelta (q,o) by A7, A35;
hence Ls . x is set by A6, A7, A35; :: thesis: verum
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: { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } c= rng (doms LsF)
proof
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in rng (doms LsF) or Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } )
assume Z in rng (doms LsF) ; :: thesis: Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
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: verum
end;
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } or Z in rng (doms LsF) )
assume Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ; :: thesis: Z in rng (doms LsF)
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: verum
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: { [:a,a:] where a is Element of RTs : a in RTs } c= { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
proof
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } or Z in { [:a,a:] where a is Element of RTs : a in RTs } )
assume Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ; :: thesis: Z in { [:a,a:] where a is Element of RTs : a in RTs }
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: verum
end;
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in { [:a,a:] where a is Element of RTs : a in RTs } or Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } )
assume Z in { [:a,a:] where a is Element of RTs : a in RTs } ; :: thesis: Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
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: verum
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: ( x in RTs & y in RTs implies x,y are_c=-comparable )
assume that
A48: x in RTs and
A49: y in RTs ; :: thesis: x,y are_c=-comparable
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: verum
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 S1[O1] by A57, A33, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum
end;
ConsecutiveSet (A,{}) = A by Th21;
then A58: S1[ 0 ] by Th26;
for O being Ordinal holds S1[O] from ORDINAL2:sch 1(A58, A1, A3);
 hence ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L ; :: thesis: verum