let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N; :: thesis: for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower
let i be Element of the Instructions of T; :: thesis: (il. T,0 ) .--> i is lower
set F = (il. T,0 ) .--> i;
let l be Element of NAT ; :: according to AMI_WSTD:def 20 :: thesis: ( l in dom ((il. T,0 ) .--> i) implies for m being Element of NAT st m <= l,T holds
m in dom ((il. T,0 ) .--> i) )
assume A1: l in dom ((il. T,0 ) .--> i) ; :: thesis: for m being Element of NAT st m <= l,T holds
m in dom ((il. T,0 ) .--> i)
let m be Element of NAT ; :: thesis: ( m <= l,T implies m in dom ((il. T,0 ) .--> i) )
assume A2: m <= l,T ; :: thesis: m in dom ((il. T,0 ) .--> i)
consider k being natural number such that
A3: m = il. T,k by Th26;
dom ((il. T,0 ) .--> i) = {(il. T,0 )} by FUNCOP_1:19;
then A4: l = il. T,0 by A1, TARSKI:def 1;
then ( 0 <= k & k <= 0 ) by A2, A3, Th28, NAT_1:2;
hence m in dom ((il. T,0 ) .--> i) by A1, A4, A3, XXREAL_0:1; :: thesis: verum