let x, y be set ; :: thesis: for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . x = f . y
let f be Function; :: thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) . x = f . y )
assume A1: ( x in dom f & y in dom f ) ; :: thesis: (Swap (f,x,y)) . x = f . y
then A2: Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def 12;
A3: dom f = dom (f +* (x,(f . y))) by FUNCT_7:30;

now :: thesis: ( x <> y implies (Swap (f,x,y)) . x = f . y )

assume x <> y ; :: thesis: (Swap (f,x,y)) . x = f . y
then (Swap (f,x,y)) . x = (f +* (x,(f . y))) . x by A2, FUNCT_7:32;
hence (Swap (f,x,y)) . x = f . y by A1, FUNCT_7:31; :: thesis: verum

end;

hence (Swap (f,x,y)) . x = f . y by A3, A1, A2, FUNCT_7:31; :: thesis: verum