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)) /. y = f /. x
let f be array of X; :: thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) /. y = f /. x )
assume A1: ( x in dom f & y in dom f ) ; :: thesis: (Swap (f,x,y)) /. y = f /. x
dom (Swap (f,x,y)) = dom f by FUNCT_7:99;
hence (Swap (f,x,y)) /. y = (Swap (f,x,y)) . y by A1, PARTFUN1:def 6
.= f . x by A1, Th31
.= f /. x by A1, PARTFUN1:def 6 ;
:: thesis: verum