let B, A be set ; :: thesis: for f being Function of A,B st card B in card A & B <> {} holds
ex x, y being set 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 set 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 set 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 set st x in dom f & y in dom f & f . x = f . y holds
x = y by A3;
then f is one-to-one by FUNCT_1:def 8;
then dom f,f .: (dom f) are_equipotent by CARD_1:60;
then dom f, rng f are_equipotent by RELAT_1:146;
then A5: card A = card (rng f) by A4, CARD_1:21;
rng f c= B by RELAT_1:def 19;
then card A c= card B by A5, CARD_1:27;
hence contradiction by A1, CARD_1:14; :: thesis: verum