let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (),(MSAEndMonoid (MSAlg UA))

reconsider i = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th7;
set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA);
set M = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #);
reconsider e = id the carrier of UA as Element of UAEnd UA by Th2;
let h be Function; :: thesis: ( dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) implies h is Homomorphism of (),(MSAEndMonoid (MSAlg UA)) )

assume that
A1: dom h = UAEnd UA and
A2: for x being object st x in UAEnd UA holds
h . x = 0 .--> x ; :: thesis: h is Homomorphism of (),(MSAEndMonoid (MSAlg UA))
A3: the carrier of () = dom h by ;
1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) = i ;
then A4: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) by Def6;
then rng h c= the carrier of (MSAEndMonoid (MSAlg UA)) by A1, A2, Lm3;
then reconsider h9 = h as Function of (),(MSAEndMonoid (MSAlg UA)) by ;
A5: h9 . e = 0 .--> e by A2;
A6: for a, b being Element of () holds h9 . (a * b) = (h9 . a) * (h9 . b)
proof
let a, b be Element of (); :: thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
reconsider a9 = a, b9 = b as Element of UAEnd UA by Def3;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th12;
reconsider ha = h9 . a, hb = h9 . b as Element of MSAEnd (MSAlg UA) by Def6;
A7: h9 . (b9 * a9) = 0 .--> (b9 * a9) by ;
reconsider A9 = A, B9 = B as Element of (MSAEndMonoid (MSAlg UA)) by ;
A8: ( ha = A9 & hb = B9 ) by A2;
thus h9 . (a * b) = h9 . (b9 * a9) by Th4
.= MSAlg (b9 * a9) by
.= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26
.= B ** (MSAlg a9) by MSUHOM_1:def 3
.= B ** A by MSUHOM_1:def 3
.= (h9 . a) * (h9 . b) by ; :: thesis: verum
end;
h9 . (1. ()) = h9 . e by Def3
.= MSAlg e by
.= i by MSUHOM_1:25
.= 1_ (MSAEndMonoid (MSAlg UA)) by Def6 ;
then h9 . (1_ ()) = 1_ (MSAEndMonoid (MSAlg UA)) ;
hence h is Homomorphism of (),(MSAEndMonoid (MSAlg UA)) by ; :: thesis: verum