let X, Y, x, y be set ; :: thesis: ( X,Y are_equipotent & x in X & y in Y implies X \ {x},Y \ {y} are_equipotent )
given f being Function such that A1: ( f is one-to-one & dom f = X & rng f = Y ) ; :: according to WELLORD2:def 4 :: thesis: ( not x in X or not y in Y or X \ {x},Y \ {y} are_equipotent )
assume A2: ( x in X & y in Y ) ; :: thesis: X \ {x},Y \ {y} are_equipotent
A3: X \ {x},f .: (X \ {x}) are_equipotent by A1, Th60;
A4: f .: (X \ {x}) = (f .: X) \ (Im f,x) by A1, FUNCT_1:123
.= Y \ (Im f,x) by A1, RELAT_1:146
.= Y \ {(f . x)} by A1, A2, FUNCT_1:117 ;
f . x in Y by A1, A2, FUNCT_1:def 5;
then Y \ {(f . x)},Y \ {y} are_equipotent by A2, Th59;
hence X \ {x},Y \ {y} are_equipotent by A3, A4, WELLORD2:22; :: thesis: verum