let K be Field; :: thesis: for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let V be VectSp of K; :: thesis: for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let W1, W2 be Subspace of V; :: thesis: for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let I1 be Basis of W1; :: thesis: for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let I2 be Basis of W2; :: thesis: for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let I be Subset of V; :: thesis: ( V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 implies Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
assume that
A1: V is_the_direct_sum_of W1,W2 and
A2: I = I1 \/ I2 ; :: thesis: Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider II1 = I1 as Subset of V by XBOOLE_1:1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider II2 = I2 as Subset of V by XBOOLE_1:1;
A5: ModuleStr(# the carrier of W1, the addF of W1, the ZeroF of W1, the lmult of W1 #) = Lin I1 by VECTSP_7:def 3
.= Lin II1 by VECTSP_9:17 ;
A6: ModuleStr(# the carrier of W2, the addF of W2, the ZeroF of W2, the lmult of W2 #) = Lin I2 by VECTSP_7:def 3
.= Lin II2 by VECTSP_9:17 ;
for x being Vector of V holds
( x in W1 + W2 iff x in (Lin II1) + (Lin II2) )

proof

let x be Vector of V; :: thesis: ( x in W1 + W2 iff x in (Lin II1) + (Lin II2) )

hereby :: thesis: ( x in (Lin II1) + (Lin II2) implies x in W1 + W2 )

assume x in W1 + W2 ; :: thesis: x in (Lin II1) + (Lin II2)
then consider x1, x2 being Vector of V such that
B1: ( x1 in W1 & x2 in W2 & x = x1 + x2 ) by VECTSP_5:1;
B2: x1 in Lin II1 by A5, B1;
x2 in Lin II2 by A6, B1;
hence x in (Lin II1) + (Lin II2) by B1, B2, VECTSP_5:1; :: thesis: verum

end;

assume x in (Lin II1) + (Lin II2) ; :: thesis: x in W1 + W2
then consider x1, x2 being Vector of V such that
B1: ( x1 in Lin II1 & x2 in Lin II2 & x = x1 + x2 ) by VECTSP_5:1;
B2: x1 in W1 by A5, B1;
x2 in W2 by A6, B1;
hence x in W1 + W2 by B1, B2, VECTSP_5:1; :: thesis: verum

end;

then A7: W1 + W2 = (Lin II1) + (Lin II2) by VECTSP_4:30;
thus ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = W1 + W2 by A1, VECTSP_5:def 4
.= Lin I by A2, A7, VECTSP_7:15 ; :: thesis: verum