let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
let h be Function; :: thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) )
assume A1: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) ) ; :: thesis: h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
set G = UAAutGroup UA;
set H = MSAAutGroup (MSAlg UA);
rng h c= the carrier of (MSAAutGroup (MSAlg UA)) by A1, Lm4;
then reconsider h' = h as Function of the carrier of (UAAutGroup UA),the carrier of (MSAAutGroup (MSAlg UA)) by A1, FUNCT_2:def 1, RELSET_1:11;

now

let a, b be Element of (UAAutGroup UA); :: thesis: h' . (a * b) = (h' . a) * (h' . b)
thus h' . (a * b) = (h' . a) * (h' . b) :: thesis: verum

proof

reconsider a' = a, b' = b as Element of UAAut UA ;
reconsider A = 0 .--> a', B = 0 .--> b' as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th39;
reconsider A' = A, B' = B as Element of (MSAAutGroup (MSAlg UA)) by Th34;
reconsider ha = h' . a, hb = h' . b as Element of MSAAut (MSAlg UA) ;
A2: ( ha = A' & hb = B' ) by A1;
A3: h' . (b' * a') = 0 .--> (b' * a') by A1, Th7;
thus h' . (a * b) = h' . (b' * a') by Def2
.= MSAlg (b' * a') by A3, 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 A2, Def8 ; :: thesis: verum

end;

end;

hence h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by GROUP_6:def 7; :: thesis: verum