let i be Instruction of SCMPDS ; :: thesis: card (Load i) = 1
A1: dom (Load i) = {0 } by FUNCOP_1:19;
thus card (Load i) = card (dom (Load i)) by CARD_1:104
.= 1 by A1, CARD_1:50 ; :: thesis: verum