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