let UA be Universal_Algebra; :: thesis: for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
h is bijective
let h be Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)); :: thesis: ( ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies h is bijective )
assume A1: for x being set st x in UAAut UA holds
h . x = 0 .--> x ; :: thesis: h is bijective
set G = UAAutGroup UA;
thus h is bijective :: thesis: verum

proof

thus h is one-to-one :: according to FUNCT_2:def 4 :: thesis: h is onto

proof

for a, b being Element of (UAAutGroup UA) st h . a = h . b holds
a = b

proof

let a, b be Element of (UAAutGroup UA); :: thesis: ( h . a = h . b implies a = b )
assume A2: h . a = h . b ; :: thesis: a = b
A3: h . a = 0 .--> a by A1
.= [:{0 },{a}:] ;
h . b = 0 .--> b by A1
.= [:{0 },{b}:] ;
then {a} = {b} by A2, A3, ZFMISC_1:134;
hence a = b by ZFMISC_1:6; :: thesis: verum

end;

hence h is one-to-one by GROUP_6:1; :: thesis: verum

end;

dom h = UAAut UA by FUNCT_2:def 1;
hence rng h = the carrier of (MSAAutGroup (MSAlg UA)) by A1, Lm4; :: according to FUNCT_2:def 3 :: thesis: verum

end;