theorem :: EQUATION:2

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 g ** f is "onto" holds
g is "onto"