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

proof

let x be set ; :: 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