let G be Group; :: thesis: for a being Element of G holds

( a in center G iff for b being Element of G holds a * b = b * a )

let a be Element of G; :: thesis: ( a in center G iff for b being Element of G holds a * b = b * a )

thus ( a in center G implies for b being Element of G holds a * b = b * a ) :: thesis: ( ( for b being Element of G holds a * b = b * a ) implies a in center G )

then a in { c where c is Element of G : for b being Element of G holds c * b = b * c } ;

then a in the carrier of (center G) by Def10;

hence a in center G by STRUCT_0:def 5; :: thesis: verum

( a in center G iff for b being Element of G holds a * b = b * a )

let a be Element of G; :: thesis: ( a in center G iff for b being Element of G holds a * b = b * a )

thus ( a in center G implies for b being Element of G holds a * b = b * a ) :: thesis: ( ( for b being Element of G holds a * b = b * a ) implies a in center G )

proof

assume
for b being Element of G holds a * b = b * a
; :: thesis: a in center G
assume
a in center G
; :: thesis: for b being Element of G holds a * b = b * a

then a in the carrier of (center G) by STRUCT_0:def 5;

then a in { b where b is Element of G : for c being Element of G holds b * c = c * b } by Def10;

then ex b being Element of G st

( a = b & ( for c being Element of G holds b * c = c * b ) ) ;

hence for b being Element of G holds a * b = b * a ; :: thesis: verum

end;then a in the carrier of (center G) by STRUCT_0:def 5;

then a in { b where b is Element of G : for c being Element of G holds b * c = c * b } by Def10;

then ex b being Element of G st

( a = b & ( for c being Element of G holds b * c = c * b ) ) ;

hence for b being Element of G holds a * b = b * a ; :: thesis: verum

then a in { c where c is Element of G : for b being Element of G holds c * b = b * c } ;

then a in the carrier of (center G) by Def10;

hence a in center G by STRUCT_0:def 5; :: thesis: verum