let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed lower FinPartState of T holds LastLoc F = il. T,((card F) -' 1)
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being non empty programmed lower FinPartState of T holds LastLoc F = il. T,((card F) -' 1)
let F be non empty programmed lower FinPartState of T; :: thesis: LastLoc F = il. T,((card F) -' 1)
A1: LastLoc F in dom F by Th51;
consider k being natural number such that
A2: LastLoc F = il. T,k by Th26;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < card F by A1, A2, Th50;
then A3: k <= (card F) -' 1 by NAT_D:49;

per cases ( k < (card F) -' 1 or k = (card F) -' 1 ) by A3, 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:8;
then k + 1 < card F by NAT_1:14, XREAL_1:237;
then il. T,(k + 1) in dom F by Th50;
then il. T,(k + 1) <= LastLoc F by Th53;
then A5: k + 1 <= k by A2, Th28;
k <= k + 1 by NAT_1:11;
then k + 0 = k + 1 by A5, 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 A2; :: thesis: verum

end;

end;