let S be COM-Struct ; :: thesis: for i being Instruction of S holds card (Macro i) = 2
let i be Instruction of S; :: thesis: card (Macro i) = 2
thus card (Macro i) = (card (Load i)) + (card (Stop S)) by AFINSQ_1:17
.= (card (Load i)) + 1 by AFINSQ_1:34
.= 1 + 1 by Th38
.= 2 ; :: thesis: verum