let V be RealLinearSpace; :: 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 RLSUB_1:27;
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 RLSUB_1: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 Th8;
consider w1, w2 being VECTOR of W such that
A4: ( w1 in W1 & w2 in W2 ) and
A5: w = w1 + w2 by A3, RLSUB_2:1;
reconsider v1 = w1, v2 = w2 as VECTOR of V by RLSUB_1:10;
v = v1 + v2 by A5, RLSUB_1:13;
hence v in V1 + V2 by A1, A4, RLSUB_2: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 RLSUB_2: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, RLSUB_1:13;
hence v in W3 by A1, A6, RLSUB_2:1; :: thesis: verum
end;
hence W1 + W2 = V1 + V2 by RLSUB_1:31; :: thesis: verum