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 (UAEndMonoid UA),(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 (UAEndMonoid UA),(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 (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 h9 = h as Function of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A3, FUNCT_2:def 1, RELSET_1:4;
A5: h9 . e = 0 .--> e by A2;
A6: for a, b being Element of (UAEndMonoid UA) holds h9 . (a * b) = (h9 . a) * (h9 . b)
proof
let a, b be Element of (UAEndMonoid UA); :: 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 A2, Th3;
reconsider A9 = A, B9 = B as Element of (MSAEndMonoid (MSAlg UA)) by A4, Th9;
A8: ( ha = A9 & hb = B9 ) by A2;
thus h9 . (a * b) = h9 . (b9 * a9) by Th4
.= MSAlg (b9 * a9) by A7, MSUHOM_1:def 3
.= (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 A8, Th10 ; :: thesis: verum
end;
h9 . (1. (UAEndMonoid UA)) = h9 . e by Def3
.= MSAlg e by A5, MSUHOM_1:def 3
.= i by MSUHOM_1:25
.= 1_ (MSAEndMonoid (MSAlg UA)) by Def6 ;
then h9 . (1_ (UAEndMonoid UA)) = 1_ (MSAEndMonoid (MSAlg UA)) ;
hence h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A6, GROUP_1:def 13, GROUP_6:def 6; :: thesis: verum