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 A1: card s = 23 ; :: thesis: ( not card t = 365 or 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume A2: 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 Th16, A1;
hence 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) by Lm1, A1, A2, CARD_FIN:4; :: thesis: verum