let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i, j, k being No-StopCode Instruction of S holds LastLoc ((i ';' j) ';' k) = 3
let i, j, k be No-StopCode Instruction of S; :: thesis: LastLoc ((i ';' j) ';' k) = 3
thus LastLoc ((i ';' j) ';' k) = (card ((i ';' j) ';' k)) - 1 by AFINSQ_1:91
.= 4 - 1 by Th13
.= 3 ; :: thesis: verum