let x, y, z, X be set ; :: thesis: for f being array of X st z in dom f & z <> x & z <> y holds
(Swap (f,x,y)) /. z = f /. z
let f be array of X; :: thesis: ( z in dom f & z <> x & z <> y implies (Swap (f,x,y)) /. z = f /. z )
assume A1: ( z in dom f & z <> x & z <> y ) ; :: thesis: (Swap (f,x,y)) /. z = f /. z
dom (Swap (f,x,y)) = dom f by FUNCT_7:99;
hence (Swap (f,x,y)) /. z = (Swap (f,x,y)) . z by A1, PARTFUN1:def 6
.= f . z by A1, Th33
.= f /. z by A1, PARTFUN1:def 6 ;
:: thesis: verum