let X, x be set ; :: thesis: for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Nat st x in A1 . n )
let A1 be SetSequence of X; :: thesis: ( x in Union A1 iff ex n being Nat st x in A1 . n )
set DX = union (rng A1);
for x being set holds
( x in union (rng A1) iff ex n being Nat st x in A1 . n )

proof

let x be set ; :: thesis: ( x in union (rng A1) iff ex n being Nat st x in A1 . n )
thus ( x in union (rng A1) implies ex n being Nat st x in A1 . n ) :: thesis: ( ex n being Nat st x in A1 . n implies x in union (rng A1) )

proof

assume x in union (rng A1) ; :: thesis: ex n being Nat st x in A1 . n
then consider Y being set such that
A1: x in Y and
A2: Y in rng A1 by TARSKI:def 4;
consider p being object such that
A3: p in dom A1 and
A4: Y = A1 . p by A2, FUNCT_1:def 3;
p in NAT by A3, FUNCT_2:def 1;
hence ex n being Nat st x in A1 . n by A1, A4; :: thesis: verum

end;

thus ( ex n being Nat st x in A1 . n implies x in union (rng A1) ) :: thesis: verum

proof

given n being Nat such that A5: x in A1 . n ; :: thesis: x in union (rng A1)
n in NAT by ORDINAL1:def 12;
then n in dom A1 by FUNCT_2:def 1;
then A1 . n in rng A1 by FUNCT_1:def 3;
hence x in union (rng A1) by A5, TARSKI:def 4; :: thesis: verum

end;

end;

hence ( x in Union A1 iff ex n being Nat st x in A1 . n ) ; :: thesis: verum