let X, Y, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z
let g be Function of Y,Z; :: thesis: ( Z <> {} & rng f = Y & rng g = Z implies rng (g * f) = Z )
assume Z <> {} ; :: thesis: ( not rng f = Y or not rng g = Z or rng (g * f) = Z )
then dom g = Y by Def1;
hence ( not rng f = Y or not rng g = Z or rng (g * f) = Z ) by RELAT_1:28; :: thesis: verum