:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :
for R being Skew-Field
for s being Element of R
for b₃ being strict VectSp of center R holds
( b₃ = VectSp_over_center s iff ( addLoopStr(# the carrier of b₃, the addF of b₃, the ZeroF of b₃ #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b₃ = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) );