theorem :: COMPOS_1:49

for S being COM-Struct
for m being Nat
for I being preProgram of S holds card (Reloc (I,m)) = card I