let x, y be set ; 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; ( 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 )
; (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;
hence
(Swap (f,x,y)) . x = f . y
by A3, A1, A2, FUNCT_7:31; verum