let X, Y be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st Y <> {} & g * f = id X holds
( f is one-to-one & rng g = X )
let f be Function of X,Y; :: thesis: for g being Function of Y,X st Y <> {} & g * f = id X holds
( f is one-to-one & rng g = X )
let g be Function of Y,X; :: thesis: ( Y <> {} & g * f = id X implies ( f is one-to-one & rng g = X ) )
assume that
A1: Y <> {} and
A2: g * f = id X ; :: thesis: ( f is one-to-one & rng g = X )
dom f = X by A1, Def1;
hence f is one-to-one by A2, FUNCT_1:53; :: thesis: rng g = X
rng (g * f) = X by A2, RELAT_1:71;
then X c= rng g by RELAT_1:45;
hence rng g = X by XBOOLE_0:def 10; :: thesis: verum