let X be set ; :: thesis: for x being object st not x in X holds
for p1 being Permutation of (X \/ {x}) st p1 . x = x holds
ex p being Permutation of X st p1 | X = p
let x be object ; :: thesis: ( not x in X implies for p1 being Permutation of (X \/ {x}) st p1 . x = x holds
ex p being Permutation of X st p1 | X = p )
assume A1: not x in X ; :: thesis: for p1 being Permutation of (X \/ {x}) st p1 . x = x holds
ex p being Permutation of X st p1 | X = p
let p1 be Permutation of (X \/ {x}); :: thesis: ( p1 . x = x implies ex p being Permutation of X st p1 | X = p )
assume A2: p1 . x = x ; :: thesis: ex p being Permutation of X st p1 | X = p
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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p1 | X) or y in X )
assume A9: y in rng (p1 | X) ; :: thesis: y in X
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: contradiction
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: verum

end;

X c= rng (p1 | X)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in rng (p1 | X) )
assume A14: y in X ; :: thesis: y in rng (p1 | X)
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

proof

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

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: verum

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: verum