theorem Th15: :: SCMFSA6A:25

for I, J, K being Program of holds (I ";" J) ";" K = I ";" (J ";" K)