theorem :: FUNCT_2:20

for X, Y, Z being set
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