:: deftheorem defines ';' COMPOS_1:def 23 :
for S being COM-Struct
for F, G being non empty preProgram of S holds F ';' G = (CutLastLoc F) +* (Reloc (G,((card F) -' 1)));