:: deftheorem Def10 defines *' HAHNBAN1:def 10 :
for K being non empty right_complementable Abelian add-associative right_zeroed right-distributive associative commutative doubleLoopStr
for V being non empty ModuleStr over K
for b₃ being non empty strict ModuleStr over K holds
( b₃ = V *' iff ( ( for x being set holds
( x in the carrier of b₃ iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of b₃ . (f,g) = f + g ) & 0. b₃ = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of b₃ . (x,f) = x * f ) ) );