:: deftheorem Def7 defines SubJoin RUSUB_2:def 7 :
for V being RealUnitarySpace
for b₂ being BinOp of (Subspaces V) holds
( b₂ = SubJoin V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b₂ . (A1,A2) = W1 + W2 );