theorem Th2: :: MSUALG_3:2

for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )