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