theorem Th17: :: MSUALG_9:17

for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x