theorem Th1: :: MSUALG_3:1

for I being set
for F being ManySortedFunction of I holds
( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )