let X, Y be set ; for x, y being object st X,Y are_equipotent & x in X & y in Y holds
X \ {x},Y \ {y} are_equipotent
let x, y be object ; ( 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
and
A2:
dom f = X
and
A3:
rng f = Y
; WELLORD2:def 4 ( not x in X or not y in Y or X \ {x},Y \ {y} are_equipotent )
A4:
X \ {x},f .: (X \ {x}) are_equipotent
by A1, A2, Th32;
assume that
A5:
x in X
and
A6:
y in Y
; X \ {x},Y \ {y} are_equipotent
f . x in Y
by A2, A3, A5, FUNCT_1:def 3;
then A7:
Y \ {(f . x)},Y \ {y} are_equipotent
by A6, Th31;
f .: (X \ {x}) =
(f .: X) \ (Im (f,x))
by A1, FUNCT_1:64
.=
Y \ (Im (f,x))
by A2, A3, RELAT_1:113
.=
Y \ {(f . x)}
by A2, A5, FUNCT_1:59
;
hence
X \ {x},Y \ {y} are_equipotent
by A4, A7, WELLORD2:15; verum