let A, B be set ; :: thesis: for f being Function of A,B st card A in card B holds
ex x being object st
( x in B & ( for y being object st y in A holds
f . y <> x ) )
let f be Function of A,B; :: thesis: ( card A in card B implies ex x being object st
( x in B & ( for y being object st y in A holds
f . y <> x ) ) )
assume that
A1: card A in card B and
A2: for x being object st x in B holds
ex y being object st
( y in A & f . y = x ) ; :: thesis: contradiction
A3: dom f = A by A1, CARD_1:27, FUNCT_2:def 1;
rng f = B

proof

thus rng f c= B by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: B c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in rng f )
assume x in B ; :: thesis: x in rng f
then ex y being object st
( y in A & f . y = x ) by A2;
hence x in rng f by A3, FUNCT_1:def 3; :: thesis: verum

end;

then card B c= card A by A3, CARD_1:12;
hence contradiction by A1, CARD_1:4; :: thesis: verum