let X, Y be 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) )
let f be 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 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 B be basis of F; ( 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; verum