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 that
A1: dom h = UAAut UA and
A2: 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 H = MSAAutGroup (MSAlg UA);
set G = UAAutGroup UA;
rng h c= the carrier of (MSAAutGroup (MSAlg UA)) by A1, A2, 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 ; :: 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 ;
A3: h' . (b' * a') = 0 .--> (b' * a') by A2, Th7;
reconsider A = 0 .--> a', B = 0 .--> b' as ManySortedFunction of ,(MSAlg UA) by Th39;
reconsider ha = h' . a, hb = h' . b as Element of MSAAut (MSAlg UA) ;
reconsider A' = A, B' = B as Element of by Th34;
A4: ( ha = A' & hb = B' ) by A2;
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 A4, Def8 ; :: thesis: verum

end;

end;

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