let S be COM-Struct ; :: thesis: for i being Instruction of S holds card (Load i) = 1
let i be Instruction of S; :: thesis: card (Load i) = 1
A1: dom (Load i) = {0} by FUNCOP_1:13;
thus card (Load i) = card (dom (Load i))
.= 1 by A1, CARD_1:30 ; :: thesis: verum