let X be set ; 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 ; ( 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
; 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}); ( p1 . x = x implies ex p being Permutation of X st p1 | X = p )
assume A2:
p1 . x = x
; 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 ;
TARSKI:def 3 ( not y in rng (p1 | X) or y in X )
assume A9:
y in rng (p1 | X)
;
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
;
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;
verum
end;
X c= rng (p1 | X)
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; verum