theorem Th13: :: EQUATION:13

for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f