theorem Th13: :: CARDFIL2:35

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