let s, t be non empty finite set ; :: thesis: ( card s = 23 & card t = 365 implies prob (not-one-to-one (s,t)) > 1 / 2 )
assume A1: card s = 23 ; :: thesis: ( not card t = 365 or prob (not-one-to-one (s,t)) > 1 / 2 )
assume A2: card t = 365 ; :: thesis: prob (not-one-to-one (s,t)) > 1 / 2
set E = not-one-to-one (s,t);
set comega = card (Funcs (s,t));
(2 * (card (not-one-to-one (s,t)))) / 2 > (card (Funcs (s,t))) / 2 by Th17, A1, A2, XREAL_1:74;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / 2) / (card (Funcs (s,t))) by XREAL_1:74;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / (card (Funcs (s,t)))) / 2 ;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > 1 / 2 by XCMPLX_0:def 7;
hence prob (not-one-to-one (s,t)) > 1 / 2 by RPR_1:def 1; :: thesis: verum