theorem Th25: :: GROUP_23:4

for I being non empty set
for A, B, f being ManySortedSet of I holds
( f is ManySortedFunction of A,B iff for i being Element of I holds f . i is Function of (A . i),(B . i) )