let s be finite set ; :: thesis: for t being non empty finite set st card s = 23 & card t = 365 holds
2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
let t be non empty finite set ; :: thesis: ( card s = 23 & card t = 365 implies 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume Z0: card s = 23 ; :: thesis: ( not card t = 365 or 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume Z1: card t = 365 ; :: thesis: 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
then card (not-one-to-one (s,t)) = (365 |^ 23) - ((365 !) / ((365 -' 23) !)) by Th8, Z0;
hence 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) by birthdaycomputation, CARD_FIN:4, Z0, Z1; :: thesis: verum