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