let UA be Universal_Algebra; :: thesis: 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)
let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); :: thesis: for f being Element of UAAut UA st F = 0 .--> f holds
F in MSAAut (MSAlg UA)
let f be Element of UAAut UA; :: thesis: ( F = 0 .--> f implies F in MSAAut (MSAlg UA) )
assume F = 0 .--> f ; :: thesis: F in MSAAut (MSAlg UA)
then A1: F = MSAlg f by MSUHOM_1:def 3;
f is_isomorphism by Def1;
then MSAlg f is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20;
then F is_isomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9;
hence F in MSAAut (MSAlg UA) by Def5; :: thesis: verum