let A, B be set ; for f being Function of A,B st card B in card A & B <> {} holds
ex x, y being object st
( x in A & y in A & x <> y & f . x = f . y )
let f be Function of A,B; ( card B in card A & B <> {} implies ex x, y being object st
( x in A & y in A & x <> y & f . x = f . y ) )
assume that
A1:
card B in card A
and
A2:
B <> {}
and
A3:
for x, y being object st x in A & y in A & x <> y holds
f . x <> f . y
; contradiction
A4:
dom f = A
by A2, FUNCT_2:def 1;
then
for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y
by A3;
then
f is one-to-one
;
then
dom f,f .: (dom f) are_equipotent
by CARD_1:33;
then
dom f, rng f are_equipotent
by RELAT_1:113;
then A5:
card A = card (rng f)
by A4, CARD_1:5;
rng f c= B
by RELAT_1:def 19;
then
card A c= card B
by A5, CARD_1:11;
hence
contradiction
by A1, CARD_1:4; verum