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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } or x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ; :: thesis: x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) }
then consider v, u being Element of M such that
A3: x = v + u and
A4: ( v in W1 & u in W2 ) ;
thus x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } by A3, A4; :: thesis: verum

end;

{ (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } c= { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } ; :: thesis: x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
then consider v, u being Element of M such that
A5: x = v + u and
A6: ( v in W2 & u in W1 ) ;
thus x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by A5, A6; :: thesis: verum

end;

then { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } = { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } by A2, XBOOLE_0:def 10;
hence W1 + W2 = W2 + W1 by A1, VECTSP_4:37; :: thesis: verum