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

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