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)

.= 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

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

h9 . (1. (UAEndMonoid UA)) =
h9 . e
by Def3
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;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

.= 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