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