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 " (Intersection B) = Intersection 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 " (Intersection B) = Intersection 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 " (Intersection B) = Intersection D
let D be SetSequence of Omega1; :: thesis: ( ( for n being Element of NAT holds D . n = f " (B . n) ) implies f " (Intersection B) = Intersection D )
assume A1: for n being Element of NAT holds D . n = f " (B . n) ; :: thesis: f " (Intersection B) = Intersection D
set Z = { (f " (B . n)) where n is Element of NAT : verum } ;
set Q = { (f " Y) where Y is Element of rng B : verum } ;
set E = Complement D;
A2: for n being Element of NAT holds (Complement D) . n = f " ((Complement B) . n)

proof

let n be Element of NAT ; :: thesis: (Complement D) . n = f " ((Complement B) . n)
thus (Complement D) . n = (D . n) ` by PROB_1:def 2
.= (f " (B . n)) ` by A1
.= (f " Omega2) \ (f " (B . n)) by FUNCT_2:40
.= f " ((B . n) `) by FUNCT_1:69
.= f " ((Complement B) . n) by PROB_1:def 2 ; :: thesis: verum

end;

f " (Intersection B) = (f " Omega2) \ (f " (union (rng (Complement B)))) by FUNCT_1:69
.= Omega1 \ (f " (Union (Complement B))) by FUNCT_2:40
.= Omega1 \ (Union (Complement D)) by Th2, A2
.= Omega1 \ (union (rng (Complement D))) ;
hence f " (Intersection B) = Intersection D ; :: thesis: verum