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

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

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

assume
n > 0
; :: thesis: min* (f " {m}) <= n - 1
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 x in f " {m} ; :: thesis: x in n

then x in dom f by FUNCT_1:def 7;

hence x in n ; :: thesis: verum

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