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))
.= 1 by A1, CARD_1:50 ; :: thesis: verum