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

( 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