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