let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let W1, W2 be Subspace of M; W1 + W2 = W2 + W1
set A = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where u, v is Element of M : ( v in W2 & u in W1 ) } ;
A1:
{ (v + u) where u, v is Element of M : ( v in W2 & u in W1 ) } c= { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) }
A2:
the carrier of (W1 + W2) = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) }
by Def1;
{ (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } c= { (v + u) where u, v is Element of M : ( v in W2 & u in W1 ) }
then
{ (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } = { (v + u) where u, v is Element of M : ( v in W2 & u in W1 ) }
by A1;
hence
W1 + W2 = W2 + W1
by A2, Def1; verum