theorem :: COMPOS_1:77

for S being COM-Struct
for F, G being Program of S
for n being Nat st n < LastLoc F holds
F . n = (F ';' G) . n