defpred S₁[ Ordinal] means ex S being Function-yielding c=-monotone Sequence st
( dom S = succ $1 & ( for B being Ordinal st B in succ $1 holds
ex fB being ManySortedSet of F₂(B) st
( S . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(S | B)) ) ) ) );
A3: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A4: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
defpred S₂[ object , object ] means ( $1 is Ordinal & $2 is Function-yielding c=-monotone Sequence & ( for A being Ordinal st A = $1 holds
for S being Function-yielding c=-monotone Sequence st $2 = S holds
( dom S = succ A & ( for B being Ordinal st B in succ A holds
ex fB being ManySortedSet of F₂(B) st
( S . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(S | B)) ) ) ) ) ) );
A5: for e being object st e in D holds
ex u being object st S₂[e,u]

proof

let e be object ; :: thesis: ( e in D implies ex u being object st S₂[e,u] )
assume A6: e in D ; :: thesis: ex u being object st S₂[e,u]
then reconsider E = e as Ordinal ;
consider S being Function-yielding c=-monotone Sequence such that
A7: ( dom S = succ E & ( for B being Ordinal st B in succ E holds
ex fB being ManySortedSet of F₂(B) st
( S . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(S | B)) ) ) ) ) by A4, A6;
take S ; :: thesis: S₂[e,S]
thus S₂[e,S] by A7; :: thesis: verum

end;

consider f being Function such that
A8: dom f = D and
A9: for e being object st e in D holds
S₂[e,f . e] from CLASSES1:sch 1(A5);
reconsider f = f as Sequence by A8, ORDINAL1:def 7;
A10: for A, B being Ordinal st A c= B & A in D & B in D holds
f . A c= f . B

proof

let A, B be Ordinal; :: thesis: ( A c= B & A in D & B in D implies f . A c= f . B )
assume A11: ( A c= B & A in D & B in D ) ; :: thesis: f . A c= f . B
A in succ B by A11, ORDINAL1:22;
then A12: succ A c= succ B by ORDINAL1:21;
reconsider fA = f . A, fB = f . B as Function-yielding c=-monotone Sequence by A11, A9;
A13: dom fA = succ A by A9, A11;
A14: dom fB = succ B by A9, A11;
A15: for C being Ordinal st C in succ B holds
ex fC being ManySortedSet of F₂(C) st
( fB . C = fC & ( for x being object st x in F₂(C) holds
fC . x = F₃(x,(fB | C)) ) ) by A9, A11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . A or x in f . B )
assume A16: x in f . A ; :: thesis: x in f . B
x in fA by A16;
then consider a, z being object such that
A17: x = [a,z] by RELAT_1:def 1;
A18: ( a in dom fA & fA . a = z ) by A17, FUNCT_1:1, A16;
then reconsider a = a as Ordinal ;
defpred S₃[ Ordinal] means ( $1 c= a implies fA . $1 = fB . $1 );
A19: for F being Ordinal st ( for G being Ordinal st G in F holds
S₃[G] ) holds
S₃[F]

proof

let F be Ordinal; :: thesis: ( ( for G being Ordinal st G in F holds
S₃[G] ) implies S₃[F] )
assume A20: for G being Ordinal st G in F holds
S₃[G] ; :: thesis: S₃[F]
assume A21: F c= a ; :: thesis: fA . F = fB . F
then A22: F in dom fA by A17, FUNCT_1:1, A16, ORDINAL1:12;
then consider fCF being ManySortedSet of F₂(F) such that
A23: fA . F = fCF and
A24: for x being object st x in F₂(F) holds
fCF . x = F₃(x,(fA | F)) by A13, A9, A11;
consider fBF being ManySortedSet of F₂(F) such that
A25: fB . F = fBF and
A26: for x being object st x in F₂(F) holds
fBF . x = F₃(x,(fB | F)) by A15, A12, A21, A13, A18, ORDINAL1:12;
A27: ( dom (fA | F) = F & F = dom (fB | F) ) by RELAT_1:62, A22, A12, A13, A14, ORDINAL1:def 2;
for x being object st x in F holds
(fA | F) . x = (fB | F) . x

proof

let x be object ; :: thesis: ( x in F implies (fA | F) . x = (fB | F) . x )
assume A28: x in F ; :: thesis: (fA | F) . x = (fB | F) . x
reconsider x = x as Ordinal by A28;
(fA | F) . x = fA . x by A28, FUNCT_1:49
.= fB . x by A20, A28, A21, ORDINAL1:def 2 ;
hence (fA | F) . x = (fB | F) . x by A28, FUNCT_1:49; :: thesis: verum

end;

then A29: fA | F = fB | F by A27, FUNCT_1:2;
A30: ( dom fCF = F₂(F) & F₂(F) = dom fBF ) by PARTFUN1:def 2;
for x being object st x in F₂(F) holds
fCF . x = fBF . x

proof

let x be object ; :: thesis: ( x in F₂(F) implies fCF . x = fBF . x )
assume A31: x in F₂(F) ; :: thesis: fCF . x = fBF . x
fCF . x = F₃(x,(fA | F)) by A31, A24;
hence fCF . x = fBF . x by A31, A26, A29; :: thesis: verum

end;

hence fA . F = fB . F by A23, A25, A30, FUNCT_1:2; :: thesis: verum

end;

for D being Ordinal holds S₃[D] from ORDINAL1:sch 2(A19);
then fA . a = fB . a ;
hence x in f . B by A12, A18, A13, A14, FUNCT_1:1, A17; :: thesis: verum

end;

A32: for A, B being set st A in D & B in D & A c= B holds
f . A c= f . B by A10;
for x being object st x in rng f holds
x is Function

proof

let x be object ; :: thesis: ( x in rng f implies x is Function )
assume x in rng f ; :: thesis: x is Function
then ex y being object st
( y in dom f & f . y = x ) by FUNCT_1:def 3;
hence x is Function by A8, A9; :: thesis: verum

end;

then reconsider f = f as Function-yielding c=-monotone Sequence by A32, Def1, A8, COHSP_1:def 11, FUNCT_1:def 13;
A33: for x, y being set st x in rng f & y in rng f holds
x,y are_c=-comparable

proof

let x, y be set ; :: thesis: ( x in rng f & y in rng f implies x,y are_c=-comparable )
assume A34: ( x in rng f & y in rng f ) ; :: thesis: x,y are_c=-comparable
consider A being object such that
A35: ( A in dom f & f . A = x ) by A34, FUNCT_1:def 3;
consider B being object such that
A36: ( B in dom f & f . B = y ) by A34, FUNCT_1:def 3;
reconsider A = A, B = B as Ordinal by A35, A36;
( A c= B or B c= A ) ;
then ( f . A c= f . B or f . B c= f . A ) by A10, A35, A36, A8;
hence x,y are_c=-comparable by A35, A36, XBOOLE_0:def 9; :: thesis: verum

end;

A37: for x being object st x in rng f holds
x is Sequence

proof

let x be object ; :: thesis: ( x in rng f implies x is Sequence )
assume x in rng f ; :: thesis: x is Sequence
then ex y being object st
( y in dom f & f . y = x ) by FUNCT_1:def 3;
hence x is Sequence by A8, A9; :: thesis: verum

end;

reconsider U = union (rng f) as Sequence by A33, A37, ORDINAL1:def 8, ORDINAL1:34;
A38: for x being object st x in rng U holds
x is Function

proof

let x be object ; :: thesis: ( x in rng U implies x is Function )
assume x in rng U ; :: thesis: x is Function
then consider y being object such that
A39: ( y in dom U & U . y = x ) by FUNCT_1:def 3;
consider A being Ordinal such that
A40: ( A in dom f & y in dom (f . A) ) by Th1, A39;
A41: (f . A) . y = U . y by A40, Th2;
reconsider fA = f . A as Function-yielding c=-monotone Sequence by A40, A8, A9;
dom fA = succ A by A8, A9, A40;
then reconsider y = y as Ordinal by A40;
for y being Ordinal st y in succ A holds
ex fC being ManySortedSet of F₂(y) st
( fA . y = fC & ( for x being object st x in F₂(y) holds
fC . x = F₃(x,(fA | y)) ) ) by A8, A9, A40;
hence x is Function by A41, A39; :: thesis: verum

end;

then A42: rng U is functional by FUNCT_1:def 13;
A43: U is Function-yielding by A38, FUNCT_1:def 13;
A44: for a, b being set st a in dom U & b in dom U & a c= b holds
U . a c= U . b

proof

let a, b be set ; :: thesis: ( a in dom U & b in dom U & a c= b implies U . a c= U . b )
assume A45: ( a in dom U & b in dom U & a c= b ) ; :: thesis: U . a c= U . b
consider A being Ordinal such that
A46: ( A in dom f & a in dom (f . A) ) by Th1, A45;
consider B being Ordinal such that
A47: ( B in dom f & b in dom (f . B) ) by Th1, A45;
reconsider fA = f . A, fB = f . B as Function-yielding c=-monotone Sequence by A46, A47, A8, A9;
A48: ( (f . B) . b = U . b & (f . A) . a = U . a ) by A46, A47, Th2;

per cases ( B c= A or A c= B ) ;

suppose B c= A ; :: thesis: U . a c= U . b

then A49: fB c= fA by A10, A46, A47, A8;
[b,(fB . b)] in fB by A47, FUNCT_1:1;
then ( b in dom fA & fA . b = fB . b ) by A49, FUNCT_1:1;
hence U . a c= U . b by A48, COHSP_1:def 11, A45, A46; :: thesis: verum

end;

suppose A c= B ; :: thesis: U . a c= U . b

then A50: fA c= fB by A10, A46, A47, A8;
[a,(fA . a)] in fA by A46, FUNCT_1:1;
then ( a in dom fB & fB . a = fA . a ) by A50, FUNCT_1:1;
hence U . a c= U . b by A45, A47, A48, COHSP_1:def 11; :: thesis: verum

end;

end;

end;

then reconsider U = U as Function-yielding c=-monotone Sequence by A43, COHSP_1:def 11;
A51: for A being Ordinal st A in dom U holds
dom (U . A) = F₂(A)

proof

let y be Ordinal; :: thesis: ( y in dom U implies dom (U . y) = F₂(y) )
assume A52: y in dom U ; :: thesis: dom (U . y) = F₂(y)
consider A being Ordinal such that
A53: ( A in dom f & y in dom (f . A) ) by Th1, A52;
A54: (f . A) . y = U . y by A53, Th2;
reconsider fA = f . A as Function-yielding c=-monotone Sequence by A53, A8, A9;
A55: dom fA = succ A by A8, A9, A53;
reconsider y = y as Ordinal ;
ex fC being ManySortedSet of F₂(y) st
( fA . y = fC & ( for x being object st x in F₂(y) holds
fC . x = F₃(x,(fA | y)) ) ) by A55, A8, A9, A53;
hence dom (U . y) = F₂(y) by A54, PARTFUN1:def 2; :: thesis: verum

end;

A56: dom U c= D

proof

let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in dom U or a in D )
assume A57: a in dom U ; :: thesis: a in D
consider A being Ordinal such that
A58: ( A in dom f & a in dom (f . A) ) by Th1, A57;
reconsider fA = f . A as Function-yielding c=-monotone Sequence by A58, A8, A9;
A59: dom fA = succ A by A8, A9, A58;
succ A c= D by A58, A8, ORDINAL1:21;
hence a in D by A58, A59; :: thesis: verum

end;

A60: D c= dom U

proof

let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not A in D or A in dom U )
assume A61: A in D ; :: thesis: A in dom U
reconsider fA = f . A as Function-yielding c=-monotone Sequence by A61, A9;
( dom fA = succ A & ( for B being Ordinal st B in succ A holds
ex fB being ManySortedSet of F₂(B) st
( fA . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(fA | B)) ) ) ) ) by A61, A9;
then succ A c= dom U by Th2, A61, A8;
hence A in dom U by ORDINAL1:21; :: thesis: verum

end;

then A62: D = dom U by A56, XBOOLE_0:def 10;
set UU = union (rng U);
defpred S₃[ object , object ] means ( ( $1 in dom (union (rng U)) implies $2 = (union (rng U)) . $1 ) & ( not $1 in dom (union (rng U)) implies $2 = F₃($1,U) ) );
A63: for e being object st e in F₂(D) holds
ex u being object st S₃[e,u]

proof

let e be object ; :: thesis: ( e in F₂(D) implies ex u being object st S₃[e,u] )
( e in dom (union (rng U)) or not e in dom (union (rng U)) ) ;
hence ( e in F₂(D) implies ex u being object st S₃[e,u] ) ; :: thesis: verum

end;

consider d being Function such that
A64: dom d = F₂(D) and
A65: for e being object st e in F₂(D) holds
S₃[e,d . e] from CLASSES1:sch 1(A63);
reconsider d = d as ManySortedSet of F₂(D) by PARTFUN1:def 2, A64, RELAT_1:def 18;
set d1 = 1 --> d;
set U1 = U ^ (1 --> d);
A66: dom (1 --> d) = 1 ;
then A67: ( dom (U ^ (1 --> d)) = D +^ 1 & D +^ 1 = succ D ) by A62, ORDINAL4:def 1, ORDINAL2:31;
A68: (rng U) \/ {d} is functional by A42;
0 in 1 by TARSKI:def 1, CARD_1:49;
then A69: ( (U ^ (1 --> d)) . (D +^ 0) = (1 --> d) . 0 & (1 --> d) . 0 = d ) by A66, A62, ORDINAL4:def 1, FUNCOP_1:7;
rng (1 --> d) = {d} by FUNCOP_1:8;
then A70: U ^ (1 --> d) is Function-yielding by A68, ORDINAL4:2;
for A, B being set st A in dom (U ^ (1 --> d)) & B in dom (U ^ (1 --> d)) & A c= B holds
(U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B

proof

let A, B be set ; :: thesis: ( A in dom (U ^ (1 --> d)) & B in dom (U ^ (1 --> d)) & A c= B implies (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B )
assume A71: ( A in dom (U ^ (1 --> d)) & B in dom (U ^ (1 --> d)) & A c= B ) ; :: thesis: (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B
reconsider A = A, B = B as Ordinal by A71;

per cases ( ( A in D & B in D ) or ( A in D & B = D ) or ( A = D & B in D ) or ( A = D & B = D ) ) by A67, A71, ORDINAL1:8;

suppose A72: ( A in D & B in D ) ; :: thesis: (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B

then ( (U ^ (1 --> d)) . A = U . A & (U ^ (1 --> d)) . B = U . B ) by ORDINAL4:def 1, A60;
hence (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B by A44, A60, A71, A72; :: thesis: verum

end;

suppose A73: ( A in D & B = D ) ; :: thesis: (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B

then A74: ( (U ^ (1 --> d)) . A = U . A & (U ^ (1 --> d)) . B = d ) by ORDINAL2:27, A69, ORDINAL4:def 1, A60;
consider E being Ordinal such that
A75: ( E in dom f & A in dom (f . E) ) by Th1, A73, A60;
reconsider fE = f . E as Function-yielding c=-monotone Sequence by A75, A8, A9;
dom fE = succ E by A8, A9, A75;
then consider fC being ManySortedSet of F₂(A) such that
A76: fE . A = fC and
for x being object st x in F₂(A) holds
fC . x = F₃(x,(fE | A)) by A8, A9, A75;
A77: fC = U . A by A76, A75, Th2;
U . A c= d

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in U . A or [x,y] in d )
assume A78: [x,y] in U . A ; :: thesis: [x,y] in d
A79: dom fC = F₂(A) by PARTFUN1:def 2;
A80: ( x in dom fC & fC . x = y ) by A77, A78, FUNCT_1:1;
A81: F₂(A) c= F₂(D) by A2, A73, ORDINAL1:def 2;
dom fC c= dom (union (rng U)) by A77, Th2, A60, A73;
then d . x = (union (rng U)) . x by A80, A65, A79, A81;
hence [x,y] in d by A80, A77, Th2, A60, A73, FUNCT_1:1, A81, A79, A64; :: thesis: verum

end;

hence (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B by A74; :: thesis: verum

end;

suppose ( A = D & B in D ) ; :: thesis: (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B

hence (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B by A71, ORDINAL1:12; :: thesis: verum

end;

suppose ( A = D & B = D ) ; :: thesis: (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B

hence (U ^ (1 --> d)) . A c= (U ^ (1 --> d)) . B ; :: thesis: verum

end;

end;

end;

then reconsider U1 = U ^ (1 --> d) as Function-yielding c=-monotone Sequence by A70, COHSP_1:def 11;
take U1 ; :: thesis: ( dom U1 = succ D & ( for B being Ordinal st B in succ D holds
ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) ) ) )
thus dom U1 = succ D by A67; :: thesis: for B being Ordinal st B in succ D holds
ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) )
let B be Ordinal; :: thesis: ( B in succ D implies ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) ) )
assume A82: B in succ D ; :: thesis: ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) )
A83: dom U = (dom U1) /\ (dom U) by A62, A67, XBOOLE_1:7, XBOOLE_1:28;
for x being object st x in dom U holds
U . x = U1 . x by ORDINAL4:def 1;
then A84: U = U1 | D by A62, A83, FUNCT_1:46;

per cases ( B in D or B = D ) by A82, ORDINAL1:8;

suppose A85: B in D ; :: thesis: ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) )

consider E being Ordinal such that
A86: ( E in dom f & B in dom (f . E) ) by Th1, A85, A60;
reconsider fE = f . E as Function-yielding c=-monotone Sequence by A86, A8, A9;
dom fE = succ E by A8, A9, A86;
then consider fC being ManySortedSet of F₂(B) such that
A87: fE . B = fC and
A88: for x being object st x in F₂(B) holds
fC . x = F₃(x,(fE | B)) by A8, A9, A86;
A89: fC = U . B by A87, A86, Th2;
take fC ; :: thesis: ( U1 . B = fC & ( for x being object st x in F₂(B) holds
fC . x = F₃(x,(U1 | B)) ) )
thus fC = U1 . B by A85, ORDINAL4:def 1, A60, A89; :: thesis: for x being object st x in F₂(B) holds
fC . x = F₃(x,(U1 | B))
f . E in rng f by A86, FUNCT_1:def 3;
then f . E c= U by ZFMISC_1:74;
then A90: fE | B tolerates U | B by RELAT_1:76, PARTFUN1:54;
( dom (fE | B) = B & dom (U | B) = B ) by A86, A85, ORDINAL1:def 2, A60, RELAT_1:62;
then A91: fE | B = U | B by A90, PARTFUN1:55;
let x be object ; :: thesis: ( x in F₂(B) implies fC . x = F₃(x,(U1 | B)) )
assume A92: x in F₂(B) ; :: thesis: fC . x = F₃(x,(U1 | B))
U1 | B = (U1 | D) | B by A85, ORDINAL1:def 2, RELAT_1:74;
hence fC . x = F₃(x,(U1 | B)) by A84, A88, A92, A91; :: thesis: verum

end;

suppose A93: B = D ; :: thesis: ex fB being ManySortedSet of F₂(B) st
( U1 . B = fB & ( for x being object st x in F₂(B) holds
fB . x = F₃(x,(U1 | B)) ) )

then reconsider dB = d as ManySortedSet of F₂(B) ;
take dB ; :: thesis: ( U1 . B = dB & ( for x being object st x in F₂(B) holds
dB . x = F₃(x,(U1 | B)) ) )
thus dB = U1 . B by ORDINAL2:27, A69, A93; :: thesis: for x being object st x in F₂(B) holds
dB . x = F₃(x,(U1 | B))
let x be object ; :: thesis: ( x in F₂(B) implies dB . x = F₃(x,(U1 | B)) )
assume A94: x in F₂(B) ; :: thesis: dB . x = F₃(x,(U1 | B))

per cases ( x in dom (union (rng U)) or not x in dom (union (rng U)) ) ;

suppose A95: x in dom (union (rng U)) ; :: thesis: dB . x = F₃(x,(U1 | B))

then A96: d . x = (union (rng U)) . x by A65, A93, A94;
consider A being Ordinal such that
A97: ( A in dom U & x in dom (U . A) ) by A95, Th1;
consider E being Ordinal such that
A98: ( E in dom f & A in dom (f . E) ) by A97, Th1;
reconsider fE = f . E as Function-yielding c=-monotone Sequence by A98, A8, A9;
dom fE = succ E by A8, A9, A98;
then consider fC being ManySortedSet of F₂(A) such that
A99: fE . A = fC and
A100: for x being object st x in F₂(A) holds
fC . x = F₃(x,(fE | A)) by A8, A9, A98;
A101: dom fC = F₂(A) by PARTFUN1:def 2;
A102: fC = U . A by A99, A98, Th2;
then A103: fC . x = F₃(x,(fE | A)) by A97, A101, A100;
f . E in rng f by A98, FUNCT_1:def 3;
then A104: fE | A c= U | A by RELAT_1:76, ZFMISC_1:74;
( dom (fE | A) = A & dom (U | A) = A ) by RELAT_1:62, A98, A97, ORDINAL1:def 2;
then fC . x = F₃(x,(U | A)) by A103, A104, PARTFUN1:54, PARTFUN1:55;
then fC . x = F₃(x,(U1 | D)) by A84, A51, A1, A97;
hence dB . x = F₃(x,(U1 | B)) by A96, A102, A97, Th2, A93; :: thesis: verum

end;

suppose not x in dom (union (rng U)) ; :: thesis: dB . x = F₃(x,(U1 | B))

hence dB . x = F₃(x,(U1 | B)) by A94, A65, A93, A84; :: thesis: verum

end;

end;

end;

end;

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A3);
hence ex S being Function-yielding c=-monotone Sequence st
( dom S = succ F₁() & ( for A being Ordinal st A in succ F₁() holds
ex SA being ManySortedSet of F₂(A) st
( S . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₃(o,(S | A)) ) ) ) ) ; :: thesis: verum