let R be Skew-Field; :: thesis: the carrier of (center R) c= the carrier of R

for x being object st x in the carrier of (center R) holds

x in the carrier of R

for x being object st x in the carrier of (center R) holds

x in the carrier of R

proof

hence
the carrier of (center R) c= the carrier of R
; :: thesis: verum
let y be object ; :: thesis: ( y in the carrier of (center R) implies y in the carrier of R )

assume y in the carrier of (center R) ; :: thesis: y in the carrier of 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 y in the carrier of R ; :: thesis: verum

end;assume y in the carrier of (center R) ; :: thesis: y in the carrier of 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 y in the carrier of R ; :: thesis: verum