let X, Y be set ; :: thesis: for f being Function of X,Y st X <> {} & Y <> {} holds
( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
let f be Function of X,Y; :: thesis: ( X <> {} & Y <> {} implies ( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) )
assume A1: ( X <> {} & Y <> {} ) ; :: thesis: ( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
then A2: dom f = X by Def1;
thus ( f is one-to-one implies for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) :: thesis: ( ( for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ) implies f is one-to-one )

proof

assume A3: f is one-to-one ; :: thesis: for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h
let Z be set ; :: thesis: for g, h being Function of Z,X st f * g = f * h holds
g = h
let g, h be Function of Z,X; :: thesis: ( f * g = f * h implies g = h )
( rng g c= X & rng h c= X & dom g = Z & dom h = Z ) by A1, Def1;
hence ( f * g = f * h implies g = h ) by A2, A3, FUNCT_1:49; :: thesis: verum

end;

assume A4: for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h ; :: thesis: f is one-to-one

now

let g, h be Function; :: thesis: ( rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h implies g = h )
assume ( rng g c= dom f & rng h c= dom f & dom g = dom h ) ; :: thesis: ( f * g = f * h implies g = h )
then ( g is Function of (dom g),X & h is Function of (dom g),X ) by A2, Th4;
hence ( f * g = f * h implies g = h ) by A4; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:49; :: thesis: verum