let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I being MacroInstruction of S holds LastLoc I = (card I) - 1
let I be MacroInstruction of S; :: thesis: LastLoc I = (card I) - 1
card I > 0 by NAT_1:3;
then A: card I >= 0 + 1 by NAT_1:13;
thus LastLoc I = (card I) -' 1 by AFINSQ_1:70
.= (card I) - 1 by A, XREAL_1:233 ; :: thesis: verum