let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1

let W1, W2 be Subspace of V; :: thesis: W1 + W2 = W2 + W1

set A = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;

set B = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ;

A1: { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

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

hence W1 + W2 = W2 + W1 by A2, Def1; :: thesis: verum

let W1, W2 be Subspace of V; :: thesis: W1 + W2 = W2 + W1

set A = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ;

set B = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ;

A1: { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } c= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

proof

A2:
the carrier of (W1 + W2) = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }
by Def1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } )

assume x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

then ex u, v being VECTOR of V st

( x = v + u & v in W2 & u in W1 ) ;

hence x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: verum

end;assume x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }

then ex u, v being VECTOR of V st

( x = v + u & v in W2 & u in W1 ) ;

hence x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: verum

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

proof

then
{ (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } = { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }
by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } or x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } )

assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }

then ex u, v being VECTOR of V st

( x = v + u & v in W1 & u in W2 ) ;

hence x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: verum

end;assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) }

then ex u, v being VECTOR of V st

( x = v + u & v in W1 & u in W2 ) ;

hence x in { (v + u) where u, v is VECTOR of V : ( v in W2 & u in W1 ) } ; :: thesis: verum

hence W1 + W2 = W2 + W1 by A2, Def1; :: thesis: verum