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

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]
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)) ) ) ) );
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 A4: ( a is Ordinal & b is T-Sequence & ( 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)) ) ) ) & a is Ordinal & c is T-Sequence & ( 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
then reconsider a = a as Ordinal ;
reconsider b = b as T-Sequence by A4;
reconsider c = c as T-Sequence by A4;
A5: ( 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 A4;
A6: ( 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 A4;
b = c from ORDINAL1:sch 3(A5, A6);
hence b = c ; :: thesis: verum

end;

consider G being Function such that
A7: for a, b being set holds
( [a,b] in G iff ( a in B & S₂[a,b] ) ) from FUNCT_1:sch 1(A3);
A8: 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 A7; :: thesis: verum

end;

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

end;

defpred S₃[ set , set ] means ex L being T-Sequence st
( L = G . $1 & $2 = F₂(L) );
A11: for a, b, c being set st a in B & S₃[a,b] & S₃[a,c] holds
b = c ;
A12: 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
A13: [a,c] in G by A8, RELAT_1:def 4;
reconsider L = c as T-Sequence by A7, A13;
take b = F₂(L); :: thesis: S₃[a,b]
take L ; :: thesis: ( L = G . a & b = F₂(L) )
thus L = G . a by A13, FUNCT_1:8; :: thesis: b = F₂(L)
thus b = F₂(L) ; :: thesis: verum

end;

consider F being Function such that
A14: ( dom F = B & ( for a being set st a in B holds
S₃[a,F . a] ) ) from FUNCT_1:sch 2(A11, A12);
reconsider L = F as T-Sequence by A14, 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 A14; :: 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 A15: D in B ; :: thesis: L . D = F₂((L | D))
then consider K being T-Sequence such that
A16: ( K = G . D & F . D = F₂(K) ) by A14;
D c= dom L by A14, A15, Def2;
then A17: dom (L | D) = D by RELAT_1:91;
A18: [D,K] in G by A8, A15, A16, FUNCT_1:8;
then A19: ( dom K = D & ( for B being Ordinal st B in D holds
K . B = F₂((K | B)) ) ) by A7;

A20: now

let C be Ordinal; :: thesis: ( C in D implies G . C = K | C )
assume A21: C in D ; :: thesis: G . C = K | C
then A22: C in B by A15, Th19;

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 A23: ( A = C & L = K | C ) ; :: thesis: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F₂((L | B)) ) )
A24: C c= D by A21, Def2;
hence A25: dom L = A by A19, A23, 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 A26: B in A ; :: thesis: L . B = F₂((L | B))
then ( B in D & B c= A ) by A23, A24, Def2;
then ( K . B = F₂((K | B)) & K | B = L | B ) by A7, A18, A23, FUNCT_1:82;
hence L . B = F₂((L | B)) by A23, A25, A26, FUNCT_1:70; :: thesis: verum

end;

then [C,(K | C)] in G by A7, A22;
hence G . C = K | C by FUNCT_1:8; :: thesis: verum

end;

now

let a be set ; :: thesis: ( a in D implies (L | D) . a = K . a )
assume A27: a in D ; :: thesis: (L | D) . a = K . a
then reconsider A = a as Ordinal by Th23;
A28: G . A = K | A by A20, A27;
A30: (L | D) . A = L . A by A27, FUNCT_1:72;
ex J being T-Sequence st
( J = G . A & F . A = F₂(J) ) by A14, A15, A27, Th19;
hence (L | D) . a = K . a by A7, A18, A27, A28, A30; :: thesis: verum

end;

hence L . D = F₂((L | D)) by A16, A17, A19, 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
A31: ( dom L = F₁() & ( 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 A31; :: 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 A31; :: thesis: verum