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 S_{1}[ Ordinal] means ConsecutiveDelta (q,$1) is BiFunction of (ConsecutiveSet (A,$1)),L;

A1: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

S_{1}[O2] ) holds

S_{1}[O1]

then A58: S_{1}[ 0 ]
by Th26;

for O being Ordinal holds S_{1}[O]
from ORDINAL2:sch 1(A58, A1, A3);

hence ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L ; :: thesis: verum

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 S

A1: for O1 being Ordinal st S

S

proof

A3:
for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
let O1 be Ordinal; :: thesis: ( S_{1}[O1] implies S_{1}[ succ O1] )

assume ConsecutiveDelta (q,O1) is BiFunction of (ConsecutiveSet (A,O1)),L ; :: thesis: S_{1}[ 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 S_{1}[ succ O1]
by A2; :: thesis: verum

end;assume ConsecutiveDelta (q,O1) is BiFunction of (ConsecutiveSet (A,O1)),L ; :: thesis: S

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

S

S

proof

ConsecutiveSet (A,{}) = A
by Th21;
deffunc H_{1}( 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

S_{1}[O2] ) implies S_{1}[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: S_{1}[O1]

consider Ls being Sequence such that

A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H_{1}(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

x,y are_c=-comparable

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)

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_{2}( 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_{2}(O2) ) )
from ORDINAL2:sch 2();

Ls is Function-yielding

A36: rng (doms LsF) = { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }

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 }

x,y are_c=-comparable

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_{1}[O1]
by A57, A33, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S

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: S

consider Ls being Sequence such that

A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H

A8: for O, O2 being Ordinal st O c= O2 & O2 in dom Ls holds

Ls . O c= Ls . O2

proof

for x, y being set st x in rng Ls & y in rng Ls holds
let O be Ordinal; :: thesis: for O2 being Ordinal st O c= O2 & O2 in dom Ls holds

Ls . O c= Ls . O2

defpred S_{2}[ 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_{2}[O3] ) holds

S_{2}[O2]
_{2}[O2] holds

S_{2}[ succ O2]
_{2}[ 0 ]
;

thus for O2 being Ordinal holds S_{2}[O2]
from ORDINAL2:sch 1(A23, A17, A9); :: thesis: verum

end;Ls . O c= Ls . O2

defpred S

A9: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S

S

proof

A17:
for O2 being Ordinal st S
deffunc H_{2}( 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

S_{2}[O3] ) implies S_{2}[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: S_{2}[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 = H_{2}(O3) ) )
from ORDINAL2:sch 2();

A14: Ls . O2 = ConsecutiveDelta (q,O2) by A7, A12

.= union (rng Lt) by A10, A13, Th28 ;

end;let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S

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: S

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 = H

A14: Ls . O2 = ConsecutiveDelta (q,O2) by A7, A12

.= union (rng Lt) by A10, A13, Th28 ;

per cases
( O = O2 or O <> O2 )
;

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;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

S

proof

A23:
S
let O2 be Ordinal; :: thesis: ( S_{2}[O2] implies S_{2}[ succ O2] )

assume A18: ( O c= O2 & O2 in dom Ls implies Ls . O c= Ls . O2 ) ; :: thesis: S_{2}[ succ O2]

assume that

A19: O c= succ O2 and

A20: succ O2 in dom Ls ; :: thesis: Ls . O c= Ls . (succ O2)

end;assume A18: ( O c= O2 & O2 in dom Ls implies Ls . O c= Ls . O2 ) ; :: thesis: S

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 )
;

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;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

thus for O2 being Ordinal holds S

x,y are_c=-comparable

proof

then A30:
rng Ls is c=-linear
;
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;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

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

then
union (rng Ls) in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L)
by A30, TREES_2:40;
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;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

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

consider Ts being Sequence such that

A34: ( dom Ts = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ts . O2 = H

Ls is Function-yielding

proof

then reconsider LsF = Ls as Function-yielding Function ;
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;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

A36: rng (doms LsF) = { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }

proof

{} in O1
by A4, ORDINAL3:8;
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)

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;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 rng (doms LsF) )
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;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

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

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

for x, y being set st x in RTs & y in RTs holds
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 }

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;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 { [: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 } )
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;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

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

x,y are_c=-comparable

proof

then A56:
RTs is c=-linear
;
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;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

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

then A58: S

for O being Ordinal holds S

hence ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L ; :: thesis: verum