let k, n, m be Element of 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 )
assume A1: n > 0 ; :: thesis: min* (f " {m}) <= n - 1
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 A2: x in f " {m} ; :: thesis: x in n
x in dom f by A2, FUNCT_1:def 13;
hence x in n ; :: thesis: verum

end;

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