let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: ( F is empty implies F is lower )
assume F: F is empty ; :: thesis: F is lower
let l be Element of NAT ; :: according to AMI_WSTD:def 10 :: thesis: ( l in dom F implies for m being Element of NAT st m <= l,S holds
m in dom F )
assume l in dom F ; :: thesis: for m being Element of NAT st m <= l,S holds
m in dom F
hence for m being Element of NAT st m <= l,S holds
m in dom F by F; :: thesis: verum