let T, S be 1-sorted ; :: thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
f " is one-to-one
let f be Function of T,S; :: thesis: ( rng f = [#] S & f is one-to-one implies f " is one-to-one )
assume A1: ( rng f = [#] S & f is one-to-one ) ; :: thesis: f " is one-to-one
then f " is one-to-one by FUNCT_1:62;
hence f " is one-to-one by A1, Def4; :: thesis: verum