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 A1: ( 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 A1;
reconsider x = x, y = y as Element of X by A1;
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 Th42; :: thesis: verum
end;
hence A is permutation of Swap (A,x,y) by Th39; :: thesis: verum