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 LastLoc F = il. (T,((card F) -' 1))
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 LastLoc F = il. (T,((card F) -' 1))
let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; :: thesis: LastLoc F = il. (T,((card F) -' 1))
consider k being Nat such that
A1: LastLoc F = il. (T,k) by Th6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
LastLoc F in dom F by Th28;
then k < card F by A1, Th27;
then A2: k <= (card F) -' 1 by NAT_D:49;

per cases ( k < (card F) -' 1 or k = (card F) -' 1 ) by A2, XXREAL_0:1;

suppose k < (card F) -' 1 ; :: thesis: LastLoc F = il. (T,((card F) -' 1))

then k + 1 < ((card F) -' 1) + 1 by XREAL_1:6;
then k + 1 < card F by NAT_1:14, XREAL_1:235;
then il. (T,(k + 1)) in dom F by Th27;
then il. (T,(k + 1)) <= LastLoc F,T by Th30;
then A3: k + 1 <= k by A1, Th8;
k <= k + 1 by NAT_1:11;
then k + 0 = k + 1 by A3, XXREAL_0:1;
hence LastLoc F = il. (T,((card F) -' 1)) ; :: thesis: verum

end;

suppose k = (card F) -' 1 ; :: thesis: LastLoc F = il. (T,((card F) -' 1))

hence LastLoc F = il. (T,((card F) -' 1)) by A1; :: thesis: verum

end;

end;