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

hence n >= k ; :: thesis: verum

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

hence n >= k ; :: thesis: verum