theorem Th13bThmBA2: :: CARDFIL2:37

for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X
for B being basis of F holds
( f .: (# B) is basis of (filter_image (f,F)) & <.(f .: (# B)).] = filter_image (f,F) )