let Omega1, Omega2 be non empty set ; :: thesis: for f being Function of Omega1,Omega2

for B being SetSequence of Omega2

for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let f be Function of Omega1,Omega2; :: thesis: for B being SetSequence of Omega2

for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let B be SetSequence of Omega2; :: thesis: for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let D be SetSequence of Omega1; :: thesis: ( ( for n being Element of NAT holds D . n = f " (B . n) ) implies f " (Union B) = Union D )

assume A1: for n being Element of NAT holds D . n = f " (B . n) ; :: thesis: f " (Union B) = Union D

set Z = rng D;

set Q = { (f " Y) where Y is Element of rng B : verum } ;

for x being object holds

( x in rng D iff x in { (f " Y) where Y is Element of rng B : verum } )

hence f " (Union B) = Union D by Th1; :: thesis: verum

for B being SetSequence of Omega2

for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let f be Function of Omega1,Omega2; :: thesis: for B being SetSequence of Omega2

for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let B be SetSequence of Omega2; :: thesis: for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds

f " (Union B) = Union D

let D be SetSequence of Omega1; :: thesis: ( ( for n being Element of NAT holds D . n = f " (B . n) ) implies f " (Union B) = Union D )

assume A1: for n being Element of NAT holds D . n = f " (B . n) ; :: thesis: f " (Union B) = Union D

set Z = rng D;

set Q = { (f " Y) where Y is Element of rng B : verum } ;

for x being object holds

( x in rng D iff x in { (f " Y) where Y is Element of rng B : verum } )

proof

then
rng D = { (f " Y) where Y is Element of rng B : verum }
by TARSKI:2;
let x be object ; :: thesis: ( x in rng D iff x in { (f " Y) where Y is Element of rng B : verum } )

then consider Y being Element of rng B such that

A4: x = f " Y ;

consider n being Element of NAT such that

A5: Y = B . n by FUNCT_2:113;

x = D . n by A1, A4, A5;

hence x in rng D by FUNCT_2:112; :: thesis: verum

end;hereby :: thesis: ( x in { (f " Y) where Y is Element of rng B : verum } implies x in rng D )

assume
x in { (f " Y) where Y is Element of rng B : verum }
; :: thesis: x in rng Dassume
x in rng D
; :: thesis: x in { (f " Y) where Y is Element of rng B : verum }

then consider n being Element of NAT such that

A2: x = D . n by FUNCT_2:113;

A3: x = f " (B . n) by A1, A2;

B . n in rng B by FUNCT_2:112;

hence x in { (f " Y) where Y is Element of rng B : verum } by A3; :: thesis: verum

end;then consider n being Element of NAT such that

A2: x = D . n by FUNCT_2:113;

A3: x = f " (B . n) by A1, A2;

B . n in rng B by FUNCT_2:112;

hence x in { (f " Y) where Y is Element of rng B : verum } by A3; :: thesis: verum

then consider Y being Element of rng B such that

A4: x = f " Y ;

consider n being Element of NAT such that

A5: Y = B . n by FUNCT_2:113;

x = D . n by A1, A4, A5;

hence x in rng D by FUNCT_2:112; :: thesis: verum

hence f " (Union B) = Union D by Th1; :: thesis: verum