let V be Z_Module; :: thesis: for W1, W2 being free 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 free 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 ZMODUL03:20 ;

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 ZMODUL03:20 ;

for x being Vector of V holds

( x in W1 + W2 iff x in (Lin II1) + (Lin II2) )

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, ZMODUL02:72 ; :: thesis: verum

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 free 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 ZMODUL03:20 ;

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 ZMODUL03:20 ;

for x being Vector of V holds

( x in W1 + W2 iff x in (Lin II1) + (Lin II2) )

proof

then A7:
W1 + W2 = (Lin II1) + (Lin II2)
by VECTSP_4:30;
let x be Vector of V; :: thesis: ( x in W1 + W2 iff x in (Lin II1) + (Lin II2) )

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;hereby :: thesis: ( x in (Lin II1) + (Lin II2) implies x in W1 + W2 )

assume
x in (Lin II1) + (Lin II2)
; :: thesis: x in W1 + W2assume
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;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

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

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, ZMODUL02:72 ; :: thesis: verum