let x, y be set ; :: thesis: for A, B being array st x in dom A & y in dom A & A is permutation of B holds
( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )
let A, B be array; :: thesis: ( x in dom A & y in dom A & A is permutation of B implies ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) )
set X = dom A;
assume A1: ( x in dom A & y in dom A & A is permutation of B ) ; :: thesis: ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )
then dom A = dom B by Th37;
then ( Swap (A,x,y) is permutation of A & B is permutation of Swap (B,x,y) ) by A1, Th43;
hence ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) by A1, Th40; :: thesis: verum