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 ;
p in NAT by ;
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 ; :: thesis: verum
end;
end;
hence ( x in Union A1 iff ex n being Nat st x in A1 . n ) ; :: thesis: verum