theorem :: COMPOS_1:50

for S being COM-Struct
for x being set
for i being Instruction of S holds
( x in dom (Load i) iff x = 0 ) by TARSKI:def 1;