let x be object ; :: thesis:
let X be set ; :: thesis:
let p, q be Permutation of X; :: thesis:
let p1, q1 be Permutation of (X \/ {x}); :: thesis:
assume that
A1: p1 | X = p and
A2: q1 | X = q and
A3: p1 . x = x and
A4: q1 . x = x ; :: thesis:
set pq = p * q;
set pq1 = p1 * q1;
set X1 = X \/ {x};
A5: X c= X \/ {x} by XBOOLE_1:7;
A6: rng q = X by FUNCT_2:def 3;
A7: dom q = X by FUNCT_2:52;
dom (p1 * q1) = X \/ {x} by FUNCT_2:52;
then A8: dom ((p1 * q1) | X) = X by RELAT_1:62, XBOOLE_1:7;
A9: dom (p * q) = X by FUNCT_2:52;
A10: dom p = X by FUNCT_2:52;
for y being object st y in dom (p * q) holds
(p * q) . y = ((p1 * q1) | X) . y

let y be object ; :: thesis:
assume A11: y in dom (p * q) ; :: thesis:
A12: (p * q) . y = p . (q . y) by A9, A11, FUNCT_2:15;
A13: (p1 * q1) . y = ((p1 * q1) | X) . y by A9, A8, A11, FUNCT_1:47;
A14: q . y in rng q by A7, A9, A11, FUNCT_1:def 3;
A15: (p1 * q1) . y = p1 . (q1 . y) by A5, A9, A11, FUNCT_2:15;
q1 . y = q . y by A2, A7, A9, A11, FUNCT_1:47;
hence (p * q) . y = ((p1 * q1) | X) . y by A1, A10, A6, A14, A13, A12, A15, FUNCT_1:47; :: thesis:

end;