for A, B being 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 )