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