let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st f is onto holds
n >= k
let f be Function of (Segm n),(Segm k); :: thesis: ( f is onto implies n >= k )
assume A1: f is onto ; :: thesis: n >= k

now :: thesis: n >= k

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: n >= k

hence n >= k ; :: thesis: verum

end;

suppose A2: k <> 0 ; :: thesis: n >= k

A3: rng f = k by A1, FUNCT_2:def 3;
dom f = n by A2, FUNCT_2:def 1;
then Segm (card k) c= Segm (card n) by A3, CARD_1:12;
then A4: card k <= card n by NAT_1:39;
thus n >= k by A4; :: thesis: verum

end;

end;

end;

hence n >= k ; :: thesis: verum