let n, k be Nat; for f being Function of n,k st n = 0 & k = 0 holds
( f is onto & f is "increasing )
let f be Function of n,k; ( n = 0 & k = 0 implies ( f is onto & f is "increasing ) )
assume that
A1:
n = 0
and
A2:
k = 0
; ( f is onto & f is "increasing )
A3:
for l, m being Nat st l in k & m in k & l < m holds
min* (f " {l}) < min* (f " {m})
by A2;
rng f = {}
by A1;
hence
( f is onto & f is "increasing )
by A1, A2, A3, Def1, FUNCT_2:def 3; verum