let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAAut UA & ( for x being object 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 object 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 object 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 h9 = h as Function of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by A1, FUNCT_2:def 1, RELSET_1:4;
now :: thesis: for a, b being Element of (UAAutGroup UA) holds h9 . (a * b) = (h9 . a) * (h9 . b)
let a, b be Element of (UAAutGroup UA); :: thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
thus h9 . (a * b) = (h9 . a) * (h9 . b) :: thesis: verum
proof
reconsider a9 = a, b9 = b as Element of UAAut UA ;
A3: h9 . (b9 * a9) = 0 .--> (b9 * a9) by A2, Th6;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th32;
reconsider ha = h9 . a, hb = h9 . b as Element of MSAAut (MSAlg UA) ;
reconsider A9 = A, B9 = B as Element of (MSAAutGroup (MSAlg UA)) by Th27;
A4: ( ha = A9 & hb = B9 ) by A2;
thus h9 . (a * b) = h9 . (b9 * a9) by Def2
.= MSAlg (b9 * a9) by A3, 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 A4, Def6 ; :: thesis: verum
end;
end;
hence h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) by GROUP_6:def 6; :: thesis: verum