let X, Y be set ; :: thesis: for S being with_empty_element Subset-Family of X
for f being Function of X,Y holds f .: S is with_empty_element Subset-Family of Y
let S be with_empty_element Subset-Family of X; :: thesis: for f being Function of X,Y holds f .: S is with_empty_element Subset-Family of Y
let f be Function of X,Y; :: thesis: f .: S is with_empty_element Subset-Family of Y
( {} is Subset of Y & {} is Subset of X & {} in S & {} = f .: {} ) by SETFAM_1:def 8;
then {} in f .: S by FUNCT_2:def 10;
hence f .: S is with_empty_element Subset-Family of Y ; :: thesis: verum