let UA be Universal_Algebra; :: thesis: for F being ManySortedFunction of (MSAlg UA),(MSAlg UA)
for f being Element of UAEnd UA st F = 0 .--> f holds
F in MSAEnd (MSAlg UA)
let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); :: thesis: for f being Element of UAEnd UA st F = 0 .--> f holds
F in MSAEnd (MSAlg UA)
let f be Element of UAEnd UA; :: thesis: ( F = 0 .--> f implies F in MSAEnd (MSAlg UA) )
assume F = 0 .--> f ; :: thesis: F in MSAEnd (MSAlg UA)
then A1: F = MSAlg f by MSUHOM_1:def 3;
f is_homomorphism by Def1;
then MSAlg f is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16;
then F is_homomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9;
hence F in MSAEnd (MSAlg UA) by Def4; :: thesis: verum