defpred S₁[ Ordinal] means ex L being T-Sequence st
( dom L = $1 & ( for B being Ordinal st B in $1 holds
L . B = F₂((L | B)) ) );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

defpred S₂[ set , set ] means ( $1 is Ordinal & $2 is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = $1 & L = $2 holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) ) ) );
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st
( dom L = C & ( for D being Ordinal st D in C holds
L . D = F₂((L | D)) ) ) ; :: thesis: S₁[B]
A3: for a, b, c being set st S₂[a,b] & S₂[a,c] holds
b = c

proof

let a, b, c be set ; :: thesis: ( S₂[a,b] & S₂[a,c] implies b = c )
assume that
A4: a is Ordinal and
A5: b is T-Sequence and
A6: for A being Ordinal
for L being T-Sequence st A = a & L = b holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) ) and
a is Ordinal and
A7: c is T-Sequence and
A8: for A being Ordinal
for L being T-Sequence st A = a & L = c holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) ) ; :: thesis: b = c
reconsider c = c as T-Sequence by A7;
reconsider a = a as Ordinal by A4;
A9: ( dom c = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = c | B holds
c . B = F₂(L) ) ) by A8;
reconsider b = b as T-Sequence by A5;
A10: ( dom b = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = b | B holds
b . B = F₂(L) ) ) by A6;
b = c from ORDINAL1:sch 3(A10, A9);
hence b = c ; :: thesis: verum

end;

consider G being Function such that
A11: for a, b being set holds
( [a,b] in G iff ( a in B & S₂[a,b] ) ) from FUNCT_1:sch 1(A3);
defpred S₃[ set , set ] means ex L being T-Sequence st
( L = G . $1 & $2 = F₂(L) );
A12: dom G = B

proof

thus for a being set st a in dom G holds
a in B :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= dom G

proof

let a be set ; :: thesis: ( a in dom G implies a in B )
assume a in dom G ; :: thesis: a in B
then ex b being set st [a,b] in G by RELAT_1:def 4;
hence a in B by A11; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in dom G )
assume A13: a in B ; :: thesis: a in dom G
then reconsider a9 = a as Ordinal by Th23;
consider L being T-Sequence such that
A14: ( dom L = a9 & ( for D being Ordinal st D in a9 holds
L . D = F₂((L | D)) ) ) by A2, A13;
for A being Ordinal
for K being T-Sequence st A = a9 & K = L holds
( dom K = A & ( for B being Ordinal st B in A holds
K . B = F₂((K | B)) ) ) by A14;
then [a9,L] in G by A11, A13;
hence a in dom G by RELAT_1:def 4; :: thesis: verum

end;

A15: for a being set st a in B holds
ex b being set st S₃[a,b]

proof

let a be set ; :: thesis: ( a in B implies ex b being set st S₃[a,b] )
assume a in B ; :: thesis: ex b being set st S₃[a,b]
then consider c being set such that
A16: [a,c] in G by A12, RELAT_1:def 4;
reconsider L = c as T-Sequence by A11, A16;
take b = F₂(L); :: thesis: S₃[a,b]
take L ; :: thesis: ( L = G . a & b = F₂(L) )
thus L = G . a by A16, FUNCT_1:8; :: thesis: b = F₂(L)
thus b = F₂(L) ; :: thesis: verum

end;

A17: for a, b, c being set st a in B & S₃[a,b] & S₃[a,c] holds
b = c ;
consider F being Function such that
A18: ( dom F = B & ( for a being set st a in B holds
S₃[a,F . a] ) ) from FUNCT_1:sch 2(A17, A15);
reconsider L = F as T-Sequence by A18, Def7;
take L ; :: thesis: ( dom L = B & ( for B being Ordinal st B in B holds
L . B = F₂((L | B)) ) )
thus dom L = B by A18; :: thesis: for B being Ordinal st B in B holds
L . B = F₂((L | B))
let D be Ordinal; :: thesis: ( D in B implies L . D = F₂((L | D)) )
assume A19: D in B ; :: thesis: L . D = F₂((L | D))
then consider K being T-Sequence such that
A20: K = G . D and
A21: F . D = F₂(K) by A18;
A22: [D,K] in G by A12, A19, A20, FUNCT_1:8;
then A23: dom K = D by A11;

A24: now

let C be Ordinal; :: thesis: ( C in D implies G . C = K | C )
assume A25: C in D ; :: thesis: G . C = K | C

A26: now

let A be Ordinal; :: thesis: for L being T-Sequence st A = C & L = K | C holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) )
let L be T-Sequence; :: thesis: ( A = C & L = K | C implies ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) ) )
assume that
A27: A = C and
A28: L = K | C ; :: thesis: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) )
A29: C c= D by A25, Def2;
hence A30: dom L = A by A23, A27, A28, RELAT_1:91; :: thesis: for B being Ordinal st B in A holds
L . B = F₂((L | B))
let B be Ordinal; :: thesis: ( B in A implies L . B = F₂((L | B)) )
assume A31: B in A ; :: thesis: L . B = F₂((L | B))
then B c= A by Def2;
then A32: K | B = L | B by A27, A28, FUNCT_1:82;
K . B = F₂((K | B)) by A11, A22, A27, A29, A31;
hence L . B = F₂((L | B)) by A28, A30, A31, A32, FUNCT_1:70; :: thesis: verum

end;

C in B by A19, A25, Th19;
then [C,(K | C)] in G by A11, A26;
hence G . C = K | C by FUNCT_1:8; :: thesis: verum

end;

A33: now

let a be set ; :: thesis: ( a in D implies (L | D) . a = K . a )
assume A34: a in D ; :: thesis: (L | D) . a = K . a
then reconsider A = a as Ordinal by Th23;
A35: ( G . A = K | A & (L | D) . A = L . A ) by A24, A34, FUNCT_1:72;
ex J being T-Sequence st
( J = G . A & F . A = F₂(J) ) by A18, A19, A34, Th19;
hence (L | D) . a = K . a by A11, A22, A34, A35; :: thesis: verum

end;

D c= dom L by A18, A19, Def2;
then dom (L | D) = D by RELAT_1:91;
hence L . D = F₂((L | D)) by A21, A23, A33, FUNCT_1:9; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
then consider L being T-Sequence such that
A36: dom L = F₁() and
A37: for B being Ordinal st B in F₁() holds
L . B = F₂((L | B)) ;
take L ; :: thesis: ( dom L = F₁() & ( for B being Ordinal
for L1 being T-Sequence st B in F₁() & L1 = L | B holds
L . B = F₂(L1) ) )
thus dom L = F₁() by A36; :: thesis: for B being Ordinal
for L1 being T-Sequence st B in F₁() & L1 = L | B holds
L . B = F₂(L1)
let B be Ordinal; :: thesis: for L1 being T-Sequence st B in F₁() & L1 = L | B holds
L . B = F₂(L1)
let L1 be T-Sequence; :: thesis: ( B in F₁() & L1 = L | B implies L . B = F₂(L1) )
assume ( B in F₁() & L1 = L | B ) ; :: thesis: L . B = F₂(L1)
hence L . B = F₂(L1) by A37; :: thesis: verum