let x be object ; for X being set
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 X be set ; 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; 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}); ( p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x implies ( (p1 * q1) | X = p * q & (p1 * q1) . x = x ) )
assume that
A1:
p1 | X = p
and
A2:
q1 | X = q
and
A3:
p1 . x = x
and
A4:
q1 . x = x
; ( (p1 * q1) | X = p * q & (p1 * q1) . x = x )
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
proof
let y be
object ;
( y in dom (p * q) implies (p * q) . y = ((p1 * q1) | X) . y )
assume A11:
y in dom (p * q)
;
(p * q) . y = ((p1 * q1) | X) . y
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;
verum
end;
hence
(p1 * q1) | X = p * q
by A8, FUNCT_1:2, FUNCT_2:52; (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 A3, A4, FUNCT_2:15; verum