let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1
let i be No-StopCode Instruction of S; :: thesis: for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1
let J be MacroInstruction of S; :: thesis: card (i ';' J) = (card J) + 1
thus card (i ';' J) = ((card (Macro i)) + (card J)) - 1 by COMPOS_1:20
.= (2 + (card J)) - 1 by COMPOS_1:56
.= (card J) + 1 ; :: thesis: verum