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 )

( 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

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

end;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

thus
( ex n being Nat st x in A1 . n implies x in union (rng A1) )
:: thesis: verum
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;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

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;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