let X be with_empty_element set ; :: thesis: for F being FinSequence of X ex G being Function of NAT,X st
( ( for i being Nat holds F . i = G . i ) & Union F = Union G )
let F be FinSequence of X; :: thesis: ex G being Function of NAT,X st
( ( for i being Nat holds F . i = G . i ) & Union F = Union G )
defpred S₁[ Element of NAT , set ] means ( ( $1 in dom F implies F . $1 = $2 ) & ( not $1 in dom F implies $2 = {} ) );
A1: for i being Element of NAT ex y being Element of X st S₁[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of X st S₁[i,y]

per cases ( i in dom F or not i in dom F ) ;

suppose A2: i in dom F ; :: thesis: ex y being Element of X st S₁[i,y]

then ( F . i in rng F & rng F c= X ) by FUNCT_1:3;
then reconsider y = F . i as Element of X ;
take y ; :: thesis: S₁[i,y]
thus S₁[i,y] by A2; :: thesis: verum

end;

suppose A3: not i in dom F ; :: thesis: ex y being Element of X st S₁[i,y]

reconsider y = {} as Element of X by SETFAM_1:def 8;
take y ; :: thesis: S₁[i,y]
thus S₁[i,y] by A3; :: thesis: verum

end;

end;

end;

consider G being Function of NAT,X such that
A4: for i being Element of NAT holds S₁[i,G . i] from FUNCT_2:sch 3(A1);
take G ; :: thesis: ( ( for i being Nat holds F . i = G . i ) & Union F = Union G )

A5: now :: thesis: for i being Nat holds F . i = G . i

let i be Nat; :: thesis: F . b₁ = G . b₁

per cases ( i in dom F or not i in dom F ) ;

suppose i in dom F ; :: thesis: F . b₁ = G . b₁

hence F . i = G . i by A4; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: F . b₁ = G . b₁

reconsider j = i as Element of NAT by ORDINAL1:def 12;
S₁[j,G . j] by A4;
hence F . i = G . i by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

B1: ( Union F = union (rng F) & Union G = union (rng G) ) by CARD_3:def 4;

now :: thesis: for x being object st x in Union F holds
x in Union G

let x be object ; :: thesis: ( x in Union F implies x in Union G )
assume x in Union F ; :: thesis: x in Union G
then consider A being set such that
A7: ( x in A & A in rng F ) by B1, TARSKI:def 4;
consider k being object such that
A8: ( k in dom F & A = F . k ) by A7, FUNCT_1:def 3;
reconsider k = k as Nat by A8;
dom G = NAT by FUNCT_2:def 1;
then ( A = G . k & G . k in rng G ) by A5, A8, FUNCT_1:3;
hence x in Union G by A7, B1, TARSKI:def 4; :: thesis: verum

end;

then A9: Union F c= Union G by TARSKI:def 3;

now :: thesis: for x being object st x in Union G holds
x in Union F

let x be object ; :: thesis: ( x in Union G implies x in Union F )
assume x in Union G ; :: thesis: x in Union F
then consider A being set such that
A10: ( x in A & A in rng G ) by B1, TARSKI:def 4;
consider k being object such that
A11: ( k in dom G & A = G . k ) by A10, FUNCT_1:def 3;
reconsider k = k as Nat by A11;

A12: now :: thesis: k in dom F

assume not k in dom F ; :: thesis: contradiction
then F . k = {} by FUNCT_1:def 2;
hence contradiction by A5, A10, A11; :: thesis: verum

end;

A13: F . k = G . k by A5;
F . k in rng F by A12, FUNCT_1:3;
hence x in Union F by B1, A10, A11, A13, TARSKI:def 4; :: thesis: verum

end;

then Union G c= Union F by TARSKI:def 3;
hence ( ( for i being Nat holds F . i = G . i ) & Union F = Union G ) by A5, A9, XBOOLE_0:def 10; :: thesis: verum