let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₁ -valued non empty finite lower Function holds il. (T,0) in dom F
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite lower Function holds il. (T,0) in dom F
let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; :: thesis: il. (T,0) in dom F
consider l being object such that
A1: l in dom F by XBOOLE_0:def 1;
reconsider l = l as Element of NAT by A1;
consider f being sequence of NAT such that
A2: f is bijective and
A3: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,T ) and
A4: il. (T,0) = f . 0 by Def4;
rng f = NAT by A2, FUNCT_2:def 3;
then consider x being object such that
A5: x in dom f and
A6: l = f . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A5;
f . 0 <= f . x,T by A3;
hence il. (T,0) in dom F by A1, A4, A6, Def10; :: thesis: verum