let X be set ; ( ( 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
; 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
RELAT_1:def 1 union X is Function-like
let a,
b,
c be
object ;
FUNCT_1:def 1 ( 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
;
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;
verum
end;
then reconsider F = union X as Function ;
defpred S1[ 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 S1[a,b] & S1[a,c] holds
b = c
consider G being Function such that
A15:
for a, b being object holds
( [a,b] in G iff ( a in X & S1[a,b] ) )
from FUNCT_1:sch 1(A11);
A16:
for a, b being object st [a,b] in G holds
b is Ordinal
for a being object st a in rng G holds
a is Ordinal
then consider A being Ordinal such that
A19:
rng G c= A
by Th20;
defpred S2[ 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 S2[A]
;
consider A being Ordinal such that
A21:
( S2[A] & ( for C being Ordinal st S2[C] holds
A c= C ) )
from ORDINAL1:sch 1(A20);
dom F = A
hence
union X is Sequence
by Def7; verum