let X be set ; :: thesis: ( ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear implies union X is T-Sequence )
assume that
A1: for a being set st a in X holds
a is T-Sequence and
A2: X is c=-linear ; :: thesis: union X is T-Sequence
( union X is Relation-like & union X is Function-like )

proof

thus for a being set st a in union X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def 1 :: thesis: union X is Function-like

proof

let a be set ; :: thesis: ( a in union X implies ex b, c being set st [b,c] = a )
assume a in union X ; :: thesis: ex b, c being set st [b,c] = a
then consider x being set such that
A3: a in x and
A4: x in X by TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A4;
for a being set st a in x holds
ex b, c being set st [b,c] = a by RELAT_1:def 1;
hence ex b, c being set st [b,c] = a by A3; :: thesis: verum

end;

let a be set ; :: according to FUNCT_1:def 1 :: thesis: for b₁, b₂ being number holds
( not [a,b₁] in union X or not [a,b₂] in union X or b₁ = b₂ )
let b, c be set ; :: thesis: ( not [a,b] in union X or not [a,c] in union X or b = c )
assume that
A5: [a,b] in union X and
A6: [a,c] in union X ; :: thesis: b = c
consider y being set such that
A7: [a,c] in y and
A8: y in X by A6, TARSKI:def 4;
reconsider y = y as T-Sequence by A1, A8;
consider x being set such that
A9: [a,b] in x and
A10: x in X by A5, TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A10;
x,y are_c=-comparable by A2, A10, A8, Def9;
then ( x c= y or y c= x ) by XBOOLE_0:def 9;
hence b = c by A9, A7, FUNCT_1:def 1; :: thesis: verum

end;

then reconsider F = union X as Function ;
defpred S₁[ set , set ] means ( $1 in X & ( for L being T-Sequence st L = $1 holds
dom L = $2 ) );
A11: 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
A12: a in X and
A13: for L being T-Sequence st L = a holds
dom L = b and
a in X and
A14: for L being T-Sequence st L = a holds
dom L = c ; :: thesis: b = c
reconsider a = a as T-Sequence by A1, A12;
dom a = b by A13;
hence b = c by A14; :: thesis: verum

end;

consider G being Function such that
A15: for a, b being set holds
( [a,b] in G iff ( a in X & S₁[a,b] ) ) from FUNCT_1:sch 1(A11);
A16: for a, b being set st [a,b] in G holds
b is Ordinal

proof

let a, b be set ; :: thesis: ( [a,b] in G implies b is Ordinal )
assume A17: [a,b] in G ; :: thesis: b is Ordinal
then a in X by A15;
then reconsider a = a as T-Sequence by A1;
dom a = b by A15, A17;
hence b is Ordinal ; :: thesis: verum

end;

for a being set st a in rng G holds
a is Ordinal

proof

let a be set ; :: thesis: ( a in rng G implies a is Ordinal )
assume a in rng G ; :: thesis: a is Ordinal
then consider b being set such that
A18: ( b in dom G & a = G . b ) by FUNCT_1:def 5;
[b,a] in G by A18, FUNCT_1:8;
hence a is Ordinal by A16; :: thesis: verum

end;

then consider A being Ordinal such that
A19: rng G c= A by Th36;
defpred S₂[ Ordinal] means for B being Ordinal st B in rng G holds
B c= $1;
for B being Ordinal st B in rng G holds
B c= A by A19, Def2;
then A20: ex A being Ordinal st S₂[A] ;
consider A being Ordinal such that
A21: ( S₂[A] & ( for C being Ordinal st S₂[C] holds
A c= C ) ) from ORDINAL1:sch 1(A20);
dom F = A

proof

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

proof

let a be set ; :: thesis: ( a in dom F implies a in A )
assume a in dom F ; :: thesis: a in A
then consider b being set such that
A22: [a,b] in F by RELAT_1:def 4;
consider x being set such that
A23: [a,b] in x and
A24: x in X by A22, TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A24;
for L being T-Sequence st L = x holds
dom L = dom x ;
then [x,(dom x)] in G by A15, A24;
then ( x in dom G & dom x = G . x ) by FUNCT_1:8;
then dom x in rng G by FUNCT_1:def 5;
then A25: dom x c= A by A21;
a in dom x by A23, RELAT_1:def 4;
hence a in A by A25; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in dom F )
assume A26: a in A ; :: thesis: a in dom F
then reconsider a9 = a as Ordinal by Th23;

now

assume A27: for L being T-Sequence st L in X holds
not a9 in dom L ; :: thesis: contradiction

now

let B be Ordinal; :: thesis: ( B in rng G implies B c= a9 )
assume B in rng G ; :: thesis: B c= a9
then consider c being set such that
A28: ( c in dom G & B = G . c ) by FUNCT_1:def 5;
A29: [c,B] in G by A28, FUNCT_1:8;
then c in X by A15;
then reconsider c = c as T-Sequence by A1;
( c in X & dom c = B ) by A15, A29;
hence B c= a9 by A27, Th26; :: thesis: verum

end;

then A30: A c= a9 by A21;
a9 c= A by A26, Def2;
then A = a by A30, XBOOLE_0:def 10;
hence contradiction by A26; :: thesis: verum

end;

then consider L being T-Sequence such that
A31: ( L in X & a in dom L ) ;
( L c= F & ex b being set st [a,b] in L ) by A31, RELAT_1:def 4, ZFMISC_1:92;
hence a in dom F by RELAT_1:def 4; :: thesis: verum

end;

hence union X is T-Sequence by Def7; :: thesis: verum