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 holds
f 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 holds
f is one-to-one
let g be Function of Y,Z; :: thesis: ( ( Z = {} implies Y = {} ) & g * f is one-to-one implies f is one-to-one )
assume ( Z <> {} or Y = {} ) ; :: thesis: ( not g * f is one-to-one or f is one-to-one )
then A1: Y = dom g by Def1;
rng f c= Y ;
hence ( not g * f is one-to-one or f is one-to-one ) by A1, FUNCT_1:25; :: thesis: verum