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

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