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 that
A1: X <> {} and
A2: 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 )
A3: dom f = X by A2, 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 A4: 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 )
A5: ( 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 A3, A4, A5, FUNCT_1:27; :: thesis: verum

end;

assume A6: 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 :: thesis: for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h

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 A3, Th2;
hence ( f * g = f * h implies g = h ) by A6; :: thesis: verum

end;

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