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
thus card (Load i) = card (dom (Load i))
.= 1 by CARD_1:30 ; :: thesis: verum