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

now

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 card k c= card n by A3, CARD_1:12;
then A4: card k <= card n by NAT_1:39;
card n = n by CARD_1:def 2;
hence n >= k by A4, CARD_1:def 2; :: thesis: verum

end;

end;

end;

hence n >= k ; :: thesis: verum