let A be non empty set ; :: thesis: for y being Element of A
for f being Permutation of A ex x being Element of A st f . x = y
let y be Element of A; :: thesis: for f being Permutation of A ex x being Element of A st f . x = y
let f be Permutation of A; :: thesis: ex x being Element of A st f . x = y
rng f = A by FUNCT_2:def 3;
then ex x being object st
( x in dom f & f . x = y ) by FUNCT_1:def 3;
hence ex x being Element of A st f . x = y ; :: thesis: verum