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 that
A1: f is one-to-one and
A2: rng f = X ; :: thesis: f is Permutation of X
f is onto by A2;
hence f is Permutation of X by A1; :: thesis: verum