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