let X be set ; :: thesis: for p being Permutation of X
for x, y being Element of X holds (p +* x,(p . y)) +* y,(p . x) is Permutation of X
let p be Permutation of X; :: thesis: for x, y being Element of X holds (p +* x,(p . y)) +* y,(p . x) is Permutation of X
let x, y be Element of X; :: thesis: (p +* x,(p . y)) +* y,(p . x) is Permutation of X
set p1 = p +* x,(p . y);
set p2 = (p +* x,(p . y)) +* y,(p . x);
A1: dom ((p +* x,(p . y)) +* y,(p . x)) = dom (p +* x,(p . y)) by Th32;
A2: dom (p +* x,(p . y)) = dom p by Th32;
B3: ( X = {} implies X = {} ) ;
then A3: dom p = X by FUNCT_2:def 1;

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: (p +* x,(p . y)) +* y,(p . x) is Permutation of X

then (p +* x,(p . y)) +* y,(p . x) = {} by A1, A2;
hence (p +* x,(p . y)) +* y,(p . x) is Permutation of X by A1, A2, B3; :: thesis: verum

end;

suppose A4: not X is empty ; :: thesis: (p +* x,(p . y)) +* y,(p . x) is Permutation of X

A5: rng p = X by FUNCT_2:def 3;
then A6: p . x in X by A3, A4, FUNCT_1:def 5;
thus (p +* x,(p . y)) +* y,(p . x) is Permutation of X :: thesis: verum

proof

per cases ( x = y or x <> y ) ;

suppose A7: x = y ; :: thesis: (p +* x,(p . y)) +* y,(p . x) is Permutation of X

then (p +* x,(p . y)) +* y,(p . x) = p +* x,(p . y) by Th37
.= p by A7, Th37 ;
hence (p +* x,(p . y)) +* y,(p . x) is Permutation of X ; :: thesis: verum

end;

suppose A8: x <> y ; :: thesis: (p +* x,(p . y)) +* y,(p . x) is Permutation of X

then A9: ((p +* x,(p . y)) +* y,(p . x)) . x = (p +* x,(p . y)) . x by Th34
.= p . y by A3, A4, Th33 ;
A10: ((p +* x,(p . y)) +* y,(p . x)) . y = p . x by A2, A3, A4, Th33;

A11: now

let z be set ; :: thesis: ( z in X & z <> x & z <> y implies ((p +* x,(p . y)) +* y,(p . x)) . z = p . z )
assume that
z in X and
A12: ( z <> x & z <> y ) ; :: thesis: ((p +* x,(p . y)) +* y,(p . x)) . z = p . z
thus ((p +* x,(p . y)) +* y,(p . x)) . z = (p +* x,(p . y)) . z by A12, Th34
.= p . z by A12, Th34 ; :: thesis: verum

end;

A13: now

let pz be set ; :: thesis: ( ( pz in rng ((p +* x,(p . y)) +* y,(p . x)) implies pz in X ) & ( pz in X implies b₁ in rng ((p +* x,(p . y)) +* y,(p . x)) ) )

hereby :: thesis: ( pz in X implies b₁ in rng ((p +* x,(p . y)) +* y,(p . x)) )

assume pz in rng ((p +* x,(p . y)) +* y,(p . x)) ; :: thesis: pz in X
then consider z being set such that
A14: ( z in dom ((p +* x,(p . y)) +* y,(p . x)) & pz = ((p +* x,(p . y)) +* y,(p . x)) . z ) by FUNCT_1:def 5;
A15: p . z in X by A1, A2, A5, A14, FUNCT_1:def 5;

per cases ( z = x or z = y or ( z <> x & z <> y ) ) ;

suppose z = x ; :: thesis: pz in X

hence pz in X by A3, A4, A5, A9, A14, FUNCT_1:def 5; :: thesis: verum

end;

suppose z = y ; :: thesis: pz in X

hence pz in X by A2, A3, A6, A14, Th33; :: thesis: verum

end;

suppose ( z <> x & z <> y ) ; :: thesis: pz in X

hence pz in X by A1, A2, A11, A14, A15; :: thesis: verum

end;

end;

end;

assume pz in X ; :: thesis: b₁ in rng ((p +* x,(p . y)) +* y,(p . x))
then consider z being set such that
A16: ( z in dom p & pz = p . z ) by A5, FUNCT_1:def 5;

per cases ( z = x or z = y or ( z <> x & z <> y ) ) ;

suppose z = x ; :: thesis: b₁ in rng ((p +* x,(p . y)) +* y,(p . x))

hence pz in rng ((p +* x,(p . y)) +* y,(p . x)) by A1, A2, A3, A10, A16, FUNCT_1:def 5; :: thesis: verum

end;

suppose z = y ; :: thesis: b₁ in rng ((p +* x,(p . y)) +* y,(p . x))

hence pz in rng ((p +* x,(p . y)) +* y,(p . x)) by A1, A2, A3, A9, A16, FUNCT_1:def 5; :: thesis: verum

end;

suppose ( z <> x & z <> y ) ; :: thesis: b₁ in rng ((p +* x,(p . y)) +* y,(p . x))

then ((p +* x,(p . y)) +* y,(p . x)) . z = p . z by A11, A16;
hence pz in rng ((p +* x,(p . y)) +* y,(p . x)) by A1, A2, A16, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

then rng ((p +* x,(p . y)) +* y,(p . x)) = X by TARSKI:2;
then reconsider p2 = (p +* x,(p . y)) +* y,(p . x) as Function of X,X by A1, A2, A3, A4, FUNCT_2:def 1, RELSET_1:11;
p2 is bijective

proof

now

let z1, z2 be set ; :: thesis: ( z1 in X & z2 in X & p2 . z1 = p2 . z2 implies not z1 <> z2 )
assume that
A17: z1 in X and
A18: z2 in X and
A19: p2 . z1 = p2 . z2 and
A20: z1 <> z2 ; :: thesis: contradiction

per cases ( ( z1 = x & z2 = y ) or ( z1 = y & z2 = x ) or ( z1 = x & z2 <> y ) or ( z1 <> x & z2 = y ) or ( z1 = y & z2 <> x ) or ( z1 <> y & z2 = x ) or ( z1 <> y & z2 <> x & z1 <> x & z2 <> y ) ) ;

suppose ( z1 = x & z2 = y ) ; :: thesis: contradiction

hence contradiction by A4, A8, A9, A10, A19, FUNCT_2:25; :: thesis: verum

end;

suppose ( z1 = y & z2 = x ) ; :: thesis: contradiction

hence contradiction by A4, A8, A9, A10, A19, FUNCT_2:25; :: thesis: verum

end;

suppose A21: ( z1 = x & z2 <> y ) ; :: thesis: contradiction

then p2 . z2 = p . z2 by A11, A18, A20;
hence contradiction by A9, A18, A19, A21, FUNCT_2:25; :: thesis: verum

end;

suppose A22: ( z1 <> x & z2 = y ) ; :: thesis: contradiction

then p2 . z1 = p . z1 by A11, A17, A20;
hence contradiction by A10, A17, A19, A22, FUNCT_2:25; :: thesis: verum

end;

suppose A23: ( z1 = y & z2 <> x ) ; :: thesis: contradiction

then p2 . z2 = p . z2 by A11, A18, A20;
hence contradiction by A10, A18, A19, A23, FUNCT_2:25; :: thesis: verum

end;

suppose A24: ( z1 <> y & z2 = x ) ; :: thesis: contradiction

then p2 . z1 = p . z1 by A11, A17, A20;
hence contradiction by A9, A17, A19, A24, FUNCT_2:25; :: thesis: verum

end;

suppose A25: ( z1 <> y & z2 <> x & z1 <> x & z2 <> y ) ; :: thesis: contradiction

then A26: p2 . z1 = p . z1 by A11, A17;
p2 . z2 = p . z2 by A11, A18, A25;
hence contradiction by A17, A18, A19, A20, A26, FUNCT_2:25; :: thesis: verum

end;

end;

end;

hence p2 is one-to-one by A4, FUNCT_2:25; :: according to FUNCT_2:def 4 :: thesis: p2 is onto
thus rng p2 = X by A13, TARSKI:2; :: according to FUNCT_2:def 3 :: thesis: verum

end;

hence (p +* x,(p . y)) +* y,(p . x) is Permutation of X ; :: thesis: verum

end;

end;

end;

end;

end;