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 & x in X ) by TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A3;
( x = x & ( 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 A4: ( [a,b] in union X & [a,c] in union X ) ; :: thesis: b = c
then consider x being set such that
A5: ( [a,b] in x & x in X ) by TARSKI:def 4;
consider y being set such that
A6: ( [a,c] in y & y in X ) by A4, TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A5;
reconsider y = y as T-Sequence by A1, A6;
x,y are_c=-comparable by A2, A5, A6, Def9;
then ( x c= y or y c= x ) by XBOOLE_0:def 9;
hence b = c by A5, A6, 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 ) );
A7: 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 A8: ( a in X & ( for L being T-Sequence st L = a holds
dom L = b ) & a in X & ( for L being T-Sequence st L = a holds
dom L = c ) ) ; :: thesis: b = c
then reconsider a = a as T-Sequence by A1;
( dom a = b & dom a = c ) by A8;
hence b = c ; :: thesis: verum

end;

consider G being Function such that
A9: for a, b being set holds
( [a,b] in G iff ( a in X & S₁[a,b] ) ) from FUNCT_1:sch 1(A7);
A10: 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 A11: [a,b] in G ; :: thesis: b is Ordinal
then ( a in X & ( for L being T-Sequence st L = a holds
dom L = b ) ) by A9;
then reconsider a = a as T-Sequence by A1;
dom a = b by A9, A11;
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
A12: ( b in dom G & a = G . b ) by FUNCT_1:def 5;
[b,a] in G by A12, FUNCT_1:8;
hence a is Ordinal by A10; :: thesis: verum

end;

then consider A being Ordinal such that
A13: 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 A13, Def2;
then A14: ex A being Ordinal st S₂[A] ;
consider A being Ordinal such that
A15: ( S₂[A] & ( for C being Ordinal st S₂[C] holds
A c= C ) ) from ORDINAL1:sch 1(A14);
F is T-Sequence-like

proof

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
A16: [a,b] in F by RELAT_1:def 4;
consider x being set such that
A17: ( [a,b] in x & x in X ) by A16, TARSKI:def 4;
reconsider x = x as T-Sequence by A1, A17;
A18: a in dom x by A17, RELAT_1:def 4;
for L being T-Sequence st L = x holds
dom L = dom x ;
then [x,(dom x)] in G by A9, A17;
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 dom x c= A by A15;
hence a in A by A18; :: thesis: verum

end;

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

now

assume A20: for L being T-Sequence st L in X holds
not a' in dom L ; :: thesis: contradiction

now

let B be Ordinal; :: thesis: ( B in rng G implies B c= a' )
assume B in rng G ; :: thesis: B c= a'
then consider c being set such that
A21: ( c in dom G & B = G . c ) by FUNCT_1:def 5;
A22: [c,B] in G by A21, FUNCT_1:8;
then c in X by A9;
then reconsider c = c as T-Sequence by A1;
( c in X & dom c = B ) by A9, A22;
hence B c= a' by A20, Th26; :: thesis: verum

end;

then A23: A c= a' by A15;
a' c= A by A19, Def2;
then A = a by A23, XBOOLE_0:def 10;
hence contradiction by A19; :: thesis: verum

end;

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

end;

hence dom F is ordinal ; :: according to ORDINAL1:def 7 :: thesis: verum

end;

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