let Q, X, Y, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds
f " Q c= (g * f) " (g .: Q)
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds
f " Q c= (g * f) " (g .: Q)
let g be Function of Y,Z; :: thesis: ( ( Z = {} implies Y = {} ) implies f " Q c= (g * f) " (g .: Q) )
assume ( Z <> {} or Y = {} ) ; :: thesis: f " Q c= (g * f) " (g .: Q)
then A1: dom g = Y by Def1;
rng f c= Y ;
hence f " Q c= (g * f) " (g .: Q) by A1, FUNCT_1:90; :: thesis: verum