A1: f is Function of X,X by FUNCT_2:66;
per cases ( X = {} or X <> {} ) ;
suppose A2: X = {} ; :: thesis: f . g is Element of X
then {} = dom f by A1;
then f . g = {} by FUNCT_1:def 2;
hence f . g is Element of X by A2, SUBSET_1:def 1; :: thesis: verum
end;
suppose X <> {} ; :: thesis: f . g is Element of X
hence f . g is Element of X by A1, FUNCT_2:5; :: thesis: verum
end;
end;