let x, y, X be set ; :: thesis: 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; :: 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
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 ;
:: thesis: verum