theorem Th11: :: SCMFSA6A:21
for I, J being Program of holds card (I ";" J) = (card I) + (card J)