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)

.= 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

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

f " (Intersection B) =
(f " Omega2) \ (f " (union (rng (Complement B))))
by FUNCT_1:69
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;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

.= 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