let f be Function; :: thesis: for x, y, z being object st z <> x & z <> y holds
(Swap (f,x,y)) . z = f . z
let x, y, z be object ; :: thesis: ( z <> x & z <> y implies (Swap (f,x,y)) . z = f . z )
assume A1: ( z <> x & z <> y ) ; :: thesis: (Swap (f,x,y)) . z = f . z

per cases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ;

suppose ( x in dom f & y in dom f ) ; :: thesis: (Swap (f,x,y)) . z = f . z

then Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def 12;
hence (Swap (f,x,y)) . z = (f +* (x,(f . y))) . z by A1, FUNCT_7:32
.= f . z by A1, FUNCT_7:32 ;
:: thesis: verum

end;

suppose ( not x in dom f or not y in dom f ) ; :: thesis: (Swap (f,x,y)) . z = f . z

hence (Swap (f,x,y)) . z = f . z by FUNCT_7:def 12; :: thesis: verum

end;

end;