let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st n = 0 & k = 0 holds
( f is onto & f is "increasing )
let f be Function of (Segm n),(Segm k); :: thesis: ( n = 0 & k = 0 implies ( f is onto & f is "increasing ) )
assume that
A1: n = 0 and
A2: k = 0 ; :: thesis: ( f is onto & f is "increasing )
rng f = {} by A1;
hence ( f is onto & f is "increasing ) by A1, A2, FUNCT_2:def 3; :: thesis: verum