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