:: deftheorem Def17 defines RealVS HAHNBAN1:def 17 :
for V being non empty ModuleStr over F_Complex
for b₂ being strict RLSStruct holds
( b₂ = RealVS V iff ( addLoopStr(# the carrier of b₂, the addF of b₂, the ZeroF of b₂ #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of b₂ . (r,v) = [**r,0**] * v ) ) );