let A, B be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum