let UA be Universal_Algebra; :: thesis: for h being Homomorphism of (UAAutGroup UA),(MSAAutGroup (MSAlg UA)) st ( for x being object 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 object st x in UAAut UA holds
h . x = 0 .--> x ) implies h is bijective )
set G = UAAutGroup UA;
assume A1: for x being object st x in UAAut UA holds
h . x = 0 .--> x ; :: thesis: h is bijective
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 . b = 0 .--> b by A1
.= [:{0},{b}:] ;
h . a = 0 .--> a by A1
.= [:{0},{a}:] ;
then {a} = {b} by A2, A3, ZFMISC_1:110;
hence a = b by ZFMISC_1:3; :: thesis: verum
end;
then A4: h is one-to-one by GROUP_6:1;
dom h = UAAut UA by FUNCT_2:def 1;
then rng h = the carrier of (MSAAutGroup (MSAlg UA)) by A1, Lm4;
then h is onto ;
hence h is bijective by A4; :: thesis: verum