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