theorem Th11: :: COMPOS_1:20

for S being COM-Struct
for F being Program of S
for G being non empty preProgram of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )