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;

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)

hence
h is Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA))
by GROUP_6:def 6; :: thesis: verumlet 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

end;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;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