theorem :: MSUALG_9:8

for I being set
for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G