let G be Group; :: thesis: for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f holds
Ker f = (1). G
let a be Element of G; :: thesis: for f being Endomorphism of G st a is_inner_wrt f holds
Ker f = (1). G
let f be Endomorphism of G; :: thesis: ( a is_inner_wrt f implies Ker f = (1). G )
assume A1: for x being Element of G holds f . x = x |^ a ; :: according to GROUP_22:def 2 :: thesis: Ker f = (1). G
for x being Element of G st x in Ker f holds
x in (1). G

proof

let x be Element of G; :: thesis: ( x in Ker f implies x in (1). G )
assume x in Ker f ; :: thesis: x in (1). G
then 1_ G = f . x by GROUP_6:41
.= x |^ a by A1 ;
then x = 1_ G by GROUP_3:18;
hence x in (1). G by GROUP_2:46; :: thesis: verum

end;

then A2: Ker f is Subgroup of (1). G by GROUP_2:58;
(1). G is Subgroup of Ker f by GROUP_2:65;
hence Ker f = (1). G by A2, GROUP_2:55; :: thesis: verum