let UA be Universal_Algebra; 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; ( 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
; 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);
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
;
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; verum