let k, m, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st n > 0 holds
min* (f " {m}) <= n - 1
let f be Function of (Segm n),(Segm k); :: thesis: ( n > 0 implies min* (f " {m}) <= n - 1 )
A1: f " {m} c= n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " {m} or x in n )
assume x in f " {m} ; :: thesis: x in n
then x in dom f by FUNCT_1:def 7;
hence x in n ; :: thesis: verum

end;

assume n > 0 ; :: thesis: min* (f " {m}) <= n - 1
hence min* (f " {m}) <= n - 1 by A1, Th14; :: thesis: verum