let X be set ; :: thesis: for f being Function of X,X st f is one-to-one & rng f = X holds
f is Permutation of X
let f be Function of X,X; :: thesis: ( f is one-to-one & rng f = X implies f is Permutation of X )
assume A1: ( f is one-to-one & rng f = X ) ; :: thesis: f is Permutation of X
then f is onto by Def3;
hence f is Permutation of X by A1; :: thesis: verum