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 A1: ( 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);
A2: ( 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 :: thesis: for z being object st z in dom (Swap (A,x,y)) holds
(Swap ((Swap (A,x,y)),x,y)) . z = A . z

let z be object ; :: 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 A3: ( 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 Th33
.= A . z by A3, Th33 ;
:: thesis: verum

end;

suppose A4: 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 A1, A2, Th29
.= A . z by A1, A4, Th31 ;
:: thesis: verum

end;

suppose A5: 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 A1, A2, Th31
.= A . z by A1, A5, Th29 ;
:: thesis: verum

end;

end;

end;

hence Swap ((Swap (A,x,y)),x,y) = A by A2; :: thesis: verum