let x, y be set ; :: thesis: for A being array st x in dom A & y in dom A holds
Swap ((Swap (A,x,y)),x,y) = A
let A be array; :: thesis: ( x in dom A & y in dom A implies Swap ((Swap (A,x,y)),x,y) = A )
assume Z0: ( x in dom A & y in dom A ) ; :: thesis: Swap ((Swap (A,x,y)),x,y) = A
set B = Swap (A,x,y);
set C = Swap ((Swap (A,x,y)),x,y);
A0: ( dom (Swap ((Swap (A,x,y)),x,y)) = dom (Swap (A,x,y)) & dom (Swap (A,x,y)) = dom A ) by FUNCT_7:99;

now

let z be set ; :: thesis: ( z in dom (Swap (A,x,y)) implies (Swap ((Swap (A,x,y)),x,y)) . b₁ = A . b₁ )
assume z in dom (Swap (A,x,y)) ; :: thesis: (Swap ((Swap (A,x,y)),x,y)) . b₁ = A . b₁

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

suppose C1: ( z <> x & z <> y ) ; :: thesis: (Swap ((Swap (A,x,y)),x,y)) . b₁ = A . b₁

hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . z by TSc
.= A . z by C1, TSc ;
:: thesis: verum

end;

suppose C1: z = x ; :: thesis: (Swap ((Swap (A,x,y)),x,y)) . b₁ = A . b₁

hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . y by Z0, A0, TSa
.= A . z by Z0, C1, TSb ;
:: thesis: verum

end;

suppose C1: z = y ; :: thesis: (Swap ((Swap (A,x,y)),x,y)) . b₁ = A . b₁

hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . x by Z0, A0, TSb
.= A . z by Z0, C1, TSa ;
:: thesis: verum

end;

end;

end;

hence Swap ((Swap (A,x,y)),x,y) = A by A0, FUNCT_1:2; :: thesis: verum