let X, z, x, y 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 Z0: ( 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 Z0, PARTFUN1:def 6
.= f . z by Z0, TSc
.= f /. z by Z0, PARTFUN1:def 6 ;
:: thesis: verum