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

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

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

then A4:
h is one-to-one
by GROUP_6:1;
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;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

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