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 Th29;
A2: dom (p +* (x,(p . y))) = dom p by Th29;
A3: ( X = {} implies X = {} ) ;
then A4: 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)) = {} ;
hence (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X by A3; :: thesis: verum

end;

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

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

proof

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

suppose A8: 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 Th34
.= p by A8, Th34 ;
hence (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X ; :: thesis: verum

end;

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

then A10: ((p +* (x,(p . y))) +* (y,(p . x))) . x = (p +* (x,(p . y))) . x by Th31
.= p . y by A4, A5, Th30 ;

A11: now :: thesis: for z being set st z in X & z <> x & z <> y holds
((p +* (x,(p . y))) +* (y,(p . x))) . z = p . z

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 and
A13: 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 A13, Th31
.= p . z by A12, Th31 ; :: thesis: verum

end;

A14: ((p +* (x,(p . y))) +* (y,(p . x))) . y = p . x by A2, A4, A5, Th30;

A15: now :: thesis: for pz being object holds
( ( pz in rng ((p +* (x,(p . y))) +* (y,(p . x))) implies pz in X ) & ( pz in X implies pz in rng ((p +* (x,(p . y))) +* (y,(p . x))) ) )

let pz be object ; :: 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 object such that
A16: z in dom ((p +* (x,(p . y))) +* (y,(p . x))) and
A17: pz = ((p +* (x,(p . y))) +* (y,(p . x))) . z by FUNCT_1:def 3;
A18: p . z in X by A1, A2, A6, A16, FUNCT_1:def 3;

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

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

hence pz in X by A4, A5, A6, A10, A17, FUNCT_1:def 3; :: thesis: verum

end;

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

hence pz in X by A2, A4, A7, A17, Th30; :: thesis: verum

end;

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

hence pz in X by A1, A2, A11, A16, A17, A18; :: thesis: verum

end;

end;

end;

assume pz in X ; :: thesis: b₁ in rng ((p +* (x,(p . y))) +* (y,(p . x)))
then consider z being object such that
A19: z in dom p and
A20: pz = p . z by A6, FUNCT_1:def 3;

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, A4, A14, A19, A20, FUNCT_1:def 3; :: 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, A4, A10, A19, A20, FUNCT_1:def 3; :: 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, A19;
hence pz in rng ((p +* (x,(p . y))) +* (y,(p . x))) by A1, A2, A19, A20, FUNCT_1:def 3; :: 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, A4, A5, FUNCT_2:def 1, RELSET_1:4;

now :: thesis: for z1, z2 being object st z1 in X & z2 in X & p2 . z1 = p2 . z2 holds
not z1 <> z2

let z1, z2 be object ; :: thesis: ( z1 in X & z2 in X & p2 . z1 = p2 . z2 implies not z1 <> z2 )
assume that
A21: z1 in X and
A22: z2 in X and
A23: p2 . z1 = p2 . z2 and
A24: 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 A5, A9, A10, A14, A23, FUNCT_2:19; :: thesis: verum

end;

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

hence contradiction by A5, A9, A10, A14, A23, FUNCT_2:19; :: thesis: verum

end;

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

then p2 . z2 = p . z2 by A11, A22, A24;
hence contradiction by A10, A22, A23, A25, FUNCT_2:19; :: thesis: verum

end;

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

then p2 . z1 = p . z1 by A11, A21, A24;
hence contradiction by A14, A21, A23, A26, FUNCT_2:19; :: thesis: verum

end;

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

then p2 . z2 = p . z2 by A11, A22, A24;
hence contradiction by A14, A22, A23, A27, FUNCT_2:19; :: thesis: verum

end;

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

then p2 . z1 = p . z1 by A11, A21, A24;
hence contradiction by A10, A21, A23, A28, FUNCT_2:19; :: thesis: verum

end;

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

then ( p2 . z1 = p . z1 & p2 . z2 = p . z2 ) by A11, A21, A22;
hence contradiction by A21, A22, A23, A24, FUNCT_2:19; :: thesis: verum

end;

end;

end;

then A29: p2 is one-to-one by A5, FUNCT_2:19;
rng p2 = X by A15, TARSKI:2;
then p2 is onto by FUNCT_2:def 3;
hence (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X by A29; :: thesis: verum

end;

end;

end;

end;

end;