theorem Th27: :: AUTALG_1:27
for UA being Universal_Algebra
for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAAut UA st F = 0 .--> f holds
F in MSAAut (MSAlg UA)