theorem :: COMPOS_1:52

for S being COM-Struct
for i being Instruction of S holds
( dom (Load i) = {0} & (Load i) . 0 = i ) ;