theorem Th16: :: CARDFIN2:16

for s, t being finite set st card s <= card t holds
card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))