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