let R be Skew-Field; :: thesis: for y being Element of R holds

( y in center R iff for s being Element of R holds y * s = s * y )

let y be Element of R; :: thesis: ( y in center R iff for s being Element of R holds y * s = s * y )

( y in center R iff for s being Element of R holds y * s = s * y )

let y be Element of R; :: thesis: ( y in center R iff for s being Element of R holds y * s = s * y )

hereby :: thesis: ( ( for s being Element of R holds y * s = s * y ) implies y in center R )

assume
y in center R
; :: thesis: for s being Element of R holds y * s = s * y

then y in the carrier of (center R) ;

then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } by Def4;

then ex x being Element of R st

( x = y & ( for s being Element of R holds x * s = s * x ) ) ;

hence for s being Element of R holds y * s = s * y ; :: thesis: verum

end;then y in the carrier of (center R) ;

then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } by Def4;

then ex x being Element of R st

( x = y & ( for s being Element of R holds x * s = s * x ) ) ;

hence for s being Element of R holds y * s = s * y ; :: thesis: verum

now :: thesis: ( ( for s being Element of R holds y * s = s * y ) implies y in center R )

hence
( ( for s being Element of R holds y * s = s * y ) implies y in center R )
; :: thesis: verumassume
for s being Element of R holds y * s = s * y
; :: thesis: y in center R

then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

then y is Element of (center R) by Def4;

hence y in center R ; :: thesis: verum

end;then y in { x where x is Element of R : for s being Element of R holds x * s = s * x } ;

then y is Element of (center R) by Def4;

hence y in center R ; :: thesis: verum