let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
let i1, i2, i3, i4 be No-StopCode Instruction of S; :: thesis: LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
thus LastLoc (((i1 ';' i2) ';' i3) ';' i4) = (card (((i1 ';' i2) ';' i3) ';' i4)) - 1 by AFINSQ_1:91
.= 5 - 1 by Th14
.= 4 ; :: thesis: verum