theorem Th3: :: RANDOM_3:3

for Omega1, Omega2 being non empty set
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