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 } )
proof
let x be object ; :: thesis: ( x in rng D iff x in { (f " Y) where Y is Element of rng B : verum } )
hereby :: thesis: ( x in { (f " Y) where Y is Element of rng B : verum } implies x in rng D )
assume 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;
assume x in { (f " Y) where Y is Element of rng B : verum } ; :: thesis: x in rng D
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;
then rng D = { (f " Y) where Y is Element of rng B : verum } by TARSKI:2;
hence f " (Union B) = Union D by Th1; :: thesis: verum