let R be Skew-Field; :: thesis: 0. R in center R
for s being Element of R holds (0. R) * s = s * (0. R)

proof

let s be Element of R; :: thesis: (0. R) * s = s * (0. R)
(0. R) * s = 0. R by VECTSP_1:7
.= s * (0. R) by VECTSP_1:6 ;
hence (0. R) * s = s * (0. R) ; :: thesis: verum

end;

hence 0. R in center R by Th18; :: thesis: verum