let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))
reconsider i = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th10;
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 Th3;
let h be Function; :: thesis: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds
h . x = 0 .--> x ) implies h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) )
assume that
A1: dom h = UAEnd UA and
A2: for x being set st x in UAEnd UA holds
h . x = 0 .--> x ; :: thesis: h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA))
A3: the carrier of (UAEndMonoid UA) = dom h by A1, Def3;
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 h' = h as Function of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A3, FUNCT_2:def 1, RELSET_1:11;
A5: h' . e = 0 .--> e by A2;
A6: for a, b being Element of holds h' . (a * b) = (h' . a) * (h' . b)

proof

let a, b be Element of ; :: thesis: h' . (a * b) = (h' . a) * (h' . b)
reconsider a' = a, b' = b as Element of UAEnd UA by Def3;
reconsider A = 0 .--> a', B = 0 .--> b' as ManySortedFunction of ,(MSAlg UA) by Th16;
reconsider ha = h' . a, hb = h' . b as Element of MSAEnd (MSAlg UA) by Def6;
A7: h' . (b' * a') = 0 .--> (b' * a') by A2, Th4;
reconsider A' = A, B' = B as Element of by A4, Th12;
A8: ( ha = A' & hb = B' ) by A2;
thus h' . (a * b) = h' . (b' * a') by Th5
.= MSAlg (b' * a') by A7, MSUHOM_1:def 3
.= (MSAlg b') ** (MSAlg a') by MSUHOM_1:26
.= B ** (MSAlg a') by MSUHOM_1:def 3
.= B ** A by MSUHOM_1:def 3
.= (h' . a) * (h' . b) by A8, Th13 ; :: thesis: verum

end;

h' . (1. (UAEndMonoid UA)) = h' . e by Def3
.= MSAlg e by A5, MSUHOM_1:def 3
.= i by MSUHOM_1:25
.= 1_ (MSAEndMonoid (MSAlg UA)) by Def6 ;
then h' . (1_ (UAEndMonoid UA)) = 1_ (MSAEndMonoid (MSAlg UA)) ;
hence h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A6, GROUP_1:def 17, GROUP_6:def 7; :: thesis: verum