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

let D be SetSequence of Omega1; :: thesis: ( ( for n being Element of NAT holds D . n = f " (B . n) ) implies f " () = Intersection D )
assume A1: for n being Element of NAT holds D . n = f " (B . n) ; :: thesis:
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 () . n = f " (() . n)
proof
let n be Element of NAT ; :: thesis: () . n = f " (() . n)
thus () . 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 " (() . n) by PROB_1:def 2 ; :: thesis: verum
end;
f " () = (f " Omega2) \ (f " (union (rng ()))) by FUNCT_1:69
.= Omega1 \ (f " (Union ())) by FUNCT_2:40
.= Omega1 \ (Union ()) by
.= Omega1 \ (union (rng ())) ;
hence f " () = Intersection D ; :: thesis: verum