let X, x be set ; :: thesis: for p, q being Permutation of X
for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x holds
( (p1 * q1) | X = p * q & (p1 * q1) . x = x )
let p, q be Permutation of X; :: thesis: for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x holds
( (p1 * q1) | X = p * q & (p1 * q1) . x = x )
let p1, q1 be Permutation of (X \/ {x}); :: thesis: ( p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x implies ( (p1 * q1) | X = p * q & (p1 * q1) . x = x ) )
assume A1: ( p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x ) ; :: thesis: ( (p1 * q1) | X = p * q & (p1 * q1) . x = x )
set X1 = X \/ {x};
set pq1 = p1 * q1;
set pq = p * q;
A2: ( X c= X \/ {x} & dom p = X & dom q = X & dom p1 = X \/ {x} & dom q1 = X \/ {x} & rng q = X & dom (p1 * q1) = X \/ {x} & dom (p * q) = X ) by FUNCT_2:67, FUNCT_2:def 3, XBOOLE_1:7;
then A3: ( dom ((p1 * q1) | X) = X & dom (q1 | X) = X ) by RELAT_1:91;
for y being set st y in dom (p * q) holds
(p * q) . y = ((p1 * q1) | X) . y

proof

let y be set ; :: thesis: ( y in dom (p * q) implies (p * q) . y = ((p1 * q1) | X) . y )
assume A4: y in dom (p * q) ; :: thesis: (p * q) . y = ((p1 * q1) | X) . y
q . y in rng q by A2, A4, FUNCT_1:def 5;
then ( (p1 * q1) . y = ((p1 * q1) | X) . y & (p * q) . y = p . (q . y) & (p1 * q1) . y = p1 . (q1 . y) & q1 . y = q . y & p1 . (q . y) = p . (q . y) ) by A1, A2, A3, A4, FUNCT_1:70, FUNCT_2:21;
hence (p * q) . y = ((p1 * q1) | X) . y ; :: thesis: verum

end;

hence (p1 * q1) | X = p * q by A2, A3, FUNCT_1:9; :: thesis: (p1 * q1) . x = x
x in {x} by TARSKI:def 1;
then x in X \/ {x} by XBOOLE_0:def 3;
hence (p1 * q1) . x = x by A1, FUNCT_2:21; :: thesis: verum