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