let x, y, X be set ; for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. x = f /. y
let f be array of X; ( 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
dom (Swap (f,x,y)) = dom f
by FUNCT_7:99;
hence (Swap (f,x,y)) /. x =
(Swap (f,x,y)) . x
by A1, PARTFUN1:def 6
.=
f . y
by A1, Th29
.=
f /. y
by A1, PARTFUN1:def 6
;
verum