let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let V be VectSp of K; :: thesis: for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let V1, V2, W be Subspace of V; :: thesis: for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let W1, W2 be Subspace of W; :: thesis: ( W1 = V1 & W2 = V2 implies W1 + W2 = V1 + V2 )
assume A1: ( W1 = V1 & W2 = V2 ) ; :: thesis: W1 + W2 = V1 + V2
reconsider W3 = W1 + W2 as Subspace of V by VECTSP_4:26;

now :: thesis: for v being Vector of V holds
( ( v in W3 implies v in V1 + V2 ) & ( v in V1 + V2 implies v in W3 ) )

let v be Vector of V; :: thesis: ( ( v in W3 implies v in V1 + V2 ) & ( v in V1 + V2 implies v in W3 ) )
A2: ( the carrier of W1 c= the carrier of W & the carrier of W2 c= the carrier of W ) by VECTSP_4:def 2;

hereby :: thesis: ( v in V1 + V2 implies v in W3 )

assume A3: v in W3 ; :: thesis: v in V1 + V2
then reconsider w = v as Vector of W by Th11;
consider w1, w2 being Vector of W such that
A4: ( w1 in W1 & w2 in W2 ) and
A5: w = w1 + w2 by A3, VECTSP_5:1;
reconsider v1 = w1, v2 = w2 as Vector of V by VECTSP_4:10;
v = v1 + v2 by A5, VECTSP_4:13;
hence v in V1 + V2 by A1, A4, VECTSP_5:1; :: thesis: verum

end;

assume v in V1 + V2 ; :: thesis: v in W3
then consider v1, v2 being Vector of V such that
A6: ( v1 in V1 & v2 in V2 ) and
A7: v = v1 + v2 by VECTSP_5:1;
( v1 in the carrier of W1 & v2 in the carrier of W2 ) by A1, A6;
then reconsider w1 = v1, w2 = v2 as Vector of W by A2;
v = w1 + w2 by A7, VECTSP_4:13;
hence v in W3 by A1, A6, VECTSP_5:1; :: thesis: verum

end;

hence W1 + W2 = V1 + V2 by VECTSP_4:30; :: thesis: verum