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

proof

let s be Element of R; :: thesis: (1_ R) * s = s * (1_ R)
(1_ R) * s = s by VECTSP_1:def 8
.= s * (1_ R) by VECTSP_1:def 4 ;
hence (1_ R) * s = s * (1_ R) ; :: thesis: verum

end;

hence 1_ R in center R by Th18; :: thesis: verum