let X, x be set ; :: 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
set pX = p1 | X;
A3:
( X c= X \/ {x} & dom p1 = X \/ {x} & rng p1 = X \/ {x} )
by FUNCT_2:67, FUNCT_2:def 3, XBOOLE_1:7;
then A4:
( dom (p1 | X) = X & rng (p1 | X) c= X \/ {x} )
by RELAT_1:91, RELAT_1:99;
A5:
X c= rng (p1 | X)
rng (p1 | X) c= X
proof
let y be
set ;
:: 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 x' being
set such that A10:
(
x' in dom (p1 | X) &
(p1 | X) . x' = y )
by A9, FUNCT_1:def 5;
assume A11:
not
y in X
;
:: thesis: contradiction
y in rng (p1 | X)
by A10, FUNCT_1:def 5;
then
y in {x}
by A4, A11, XBOOLE_0:def 3;
then
(
y = x &
p1 is
one-to-one &
(p1 | X) . x' = p1 . x' )
by A10, FUNCT_1:70, TARSKI:def 1;
hence
contradiction
by A1, A2, A3, A4, A9, A10, FUNCT_1:def 8;
:: thesis: verum
end;
then A12:
( rng (p1 | X) = X & p1 | X is one-to-one )
by A5, FUNCT_1:84, XBOOLE_0:def 10;
then reconsider pX = p1 | X as Function of X,X by A4, FUNCT_2:3;
pX is onto
by A12, FUNCT_2:def 3;
then
pX is Permutation of X
by A12;
hence
ex p being Permutation of X st p1 | X = p
; :: thesis: verum