theorem Th15: :: AUTALG_1:15

for I being set
for A being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "onto" & G is "onto" holds
G ** F is "onto"