let X be set ; :: thesis:
let x be object ; :: thesis:
assume A1: not x in X ; :: thesis:
let p1 be Permutation of (X \/ {x}); :: thesis:
assume A2: p1 . x = x ; :: thesis:
A3: X c= X \/ {x} by XBOOLE_1:7;
set pX = p1 | X;
A4: dom p1 = X \/ {x} by FUNCT_2:52;
then A5: dom (p1 | X) = X by RELAT_1:62, XBOOLE_1:7;
A6: rng p1 = X \/ {x} by FUNCT_2:def 3;
then A7: rng (p1 | X) c= X \/ {x} by RELAT_1:70;
A8: rng (p1 | X) c= X

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: y in rng (p1 | X) ; :: thesis:
consider x9 being object such that
A10: x9 in dom (p1 | X) and
A11: (p1 | X) . x9 = y by A9, FUNCT_1:def 3;
assume A12: not y in X ; :: thesis:
y in rng (p1 | X) by A10, A11, FUNCT_1:def 3;
then y in {x} by A7, A12, XBOOLE_0:def 3;
then A13: y = x by TARSKI:def 1;
(p1 | X) . x9 = p1 . x9 by A10, FUNCT_1:47;
hence contradiction by A1, A2, A3, A4, A5, A7, A9, A10, A11, A13, FUNCT_1:def 4; :: thesis:

end;

X c= rng (p1 | X)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: y in X ; :: thesis:
consider x9 being object such that
A15: x9 in dom p1 and
A16: p1 . x9 = y by A3, A6, A14, FUNCT_1:def 3;
A17: x9 in X

assume not x9 in X ; :: thesis:
then x9 in {x} by A4, A15, XBOOLE_0:def 3;
hence contradiction by A1, A2, A14, A16, TARSKI:def 1; :: thesis:

end;

then (p1 | X) . x9 = p1 . x9 by A5, FUNCT_1:47;
hence y in rng (p1 | X) by A5, A16, A17, FUNCT_1:def 3; :: thesis:

end;

then A18: rng (p1 | X) = X by A8;
A19: p1 | X is one-to-one by FUNCT_1:52;
reconsider pX = p1 | X as Function of X,X by A5, A18, FUNCT_2:1;
pX is onto by A18, FUNCT_2:def 3;
hence ex p being Permutation of X st p1 | X = p by A19; :: thesis: