theorem Th14: :: COMPOS_1:23

for S being COM-Struct
for F, G being Program of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0