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

proof

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

proof

let a be object ; :: thesis: ( a in union X implies ex b, c being object st [b,c] = a )
assume a in union X ; :: thesis: ex b, c being object 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 Sequence by A1, A4;
for a being object st a in x holds
ex b, c being object st [b,c] = a by RELAT_1:def 1;
hence ex b, c being object st [b,c] = a by A3; :: thesis: verum

end;

let a, b, c be object ; :: according to FUNCT_1:def 1 :: 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 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 Sequence by A1, A10;
x,y are_c=-comparable by A2, A10, A8;
then ( x c= y or y c= x ) ;
hence b = c by A9, A7, FUNCT_1:def 1; :: thesis: verum

end;

then reconsider F = union X as Function ;
defpred S₁[ object , object ] means ( $1 in X & ( for L being Sequence st L = $1 holds
dom L = $2 ) );
A11: for a, b, c being object st S₁[a,b] & S₁[a,c] holds
b = c

proof

let a, b, c be object ; :: thesis: ( S₁[a,b] & S₁[a,c] implies b = c )
assume that
A12: a in X and
A13: for L being Sequence st L = a holds
dom L = b and
a in X and
A14: for L being Sequence st L = a holds
dom L = c ; :: thesis: b = c
reconsider a = a as 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 object holds
( [a,b] in G iff ( a in X & S₁[a,b] ) ) from FUNCT_1:sch 1(A11);
A16: for a, b being object st [a,b] in G holds
b is Ordinal

proof

let a, b be object ; :: 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 Sequence by A1;
dom a = b by A15, A17;
hence b is Ordinal ; :: thesis: verum

end;

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

proof

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

end;

then consider A being Ordinal such that
A19: rng G c= A by Th20;
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 object 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 object ; :: thesis: ( a in dom F implies a in A )
assume a in dom F ; :: thesis: a in A
then consider b being object such that
A22: [a,b] in F by XTUPLE_0:def 12;
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 Sequence by A1, A24;
for L being 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:1;
then dom x in rng G by FUNCT_1:def 3;
then A25: dom x c= A by A21;
a in dom x by A23, XTUPLE_0:def 12;
hence a in A by A25; :: thesis: verum

end;

let a be object ; :: 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 Th9;

now :: thesis: ex L being Sequence st
( L in X & a9 in dom L )

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

now :: thesis: for B being Ordinal st B in rng G holds
B c= a9

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 object such that
A28: ( c in dom G & B = G . c ) by FUNCT_1:def 3;
A29: [c,B] in G by A28, FUNCT_1:1;
then c in X by A15;
then reconsider c = c as Sequence by A1;
( c in X & dom c = B ) by A15, A29;
hence B c= a9 by A27, Th12; :: thesis: verum

end;

then A30: A c= a9 by A21;
a9 c= A by A26, Def2;
then A: A = a by A30, XBOOLE_0:def 10;
reconsider aa = a as set by TARSKI:1;
not aa in aa ;
hence contradiction by A, A26; :: thesis: verum

end;

then consider L being Sequence such that
A31: ( L in X & a in dom L ) ;
( L c= F & ex b being object st [a,b] in L ) by A31, XTUPLE_0:def 12, ZFMISC_1:74;
hence a in dom F by XTUPLE_0:def 12; :: thesis: verum

end;

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