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 Z0: ( 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 ThDom;
then ( Swap (A,x,y) is permutation of A & B is permutation of Swap (B,x,y) ) by Z0, Th13;
hence ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) by Z0, ThTr; :: thesis: verum