let x, y be set ; :: thesis: for A being array st x in dom A & y in dom A holds
( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )
let A be array; :: thesis: ( x in dom A & y in dom A implies ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) ) )
set X = dom A;
assume Z0: ( x in dom A & y in dom A ) ; :: thesis: ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )
thus Swap (A,x,y) is permutation of A :: thesis: A is permutation of Swap (A,x,y)

proof

reconsider X = dom A as non empty set by Z0;
reconsider x = x, y = y as Element of X by Z0;
reconsider f = Swap ((id X),x,y) as Permutation of (dom A) ;
take f ; :: according to EXCHSORT:def 9 :: thesis: Swap (A,x,y) = A * f
thus Swap (A,x,y) = A * f by Th12; :: thesis: verum

end;

hence A is permutation of Swap (A,x,y) by ThSym; :: thesis: verum