let X, Y be non empty set ; :: thesis: 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) )
let f be Function of X,Y; :: thesis: for F being Filter of X holds
( f .: F is filter_base of Y & <.(f .: F).] = filter_image (f,F) )
let F be Filter of X; :: thesis: ( f .: F is filter_base of Y & <.(f .: F).] = filter_image (f,F) )
reconsider F1 = F as basis of F by Th03;
( f .: (# F1) is filter_base of Y & <.(f .: (# F1)).] = filter_image (f,F) ) by Th12;
hence ( f .: F is filter_base of Y & <.(f .: F).] = filter_image (f,F) ) ; :: thesis: verum