theorem :: SCMFSA6A:40

for n being Nat
for I, J being Program of st n in dom (Reloc (J,(card I))) holds
(I ";" J) . n = (Reloc (J,(card I))) . n