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 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

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 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let W1, W2 be Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let I2 be Basis of W2; :: thesis: ( W1 /\ W2 = (0). V implies I1 \/ I2 is Basis of (W1 + W2) )

assume P1: W1 /\ W2 = (0). V ; :: thesis: I1 \/ I2 is Basis of (W1 + W2)

set I = I1 \/ I2;

reconsider W = W1 + W2 as strict Subspace of V ;

reconsider WW1 = W1, WW2 = W2 as Subspace of W by VECTSP_5:7;

( the carrier of WW1 c= the carrier of W & the carrier of WW2 c= the carrier of W ) by VECTSP_4:def 2;

then ( I1 c= the carrier of W & I2 c= the carrier of W ) ;

then reconsider I0 = I1 \/ I2 as Subset of W by XBOOLE_1:8;

reconsider I10 = I1 as Basis of WW1 ;

reconsider I20 = I2 as Basis of WW2 ;

A2: WW1 /\ WW2 is Subspace of V by VECTSP_4:26;

A3: WW1 + WW2 is Subspace of V by VECTSP_4:26;

for x being object holds

( x in WW1 /\ WW2 iff x in (0). V )

( x in WW1 /\ WW2 iff x in (0). V ) ;

then A4: WW1 /\ WW2 = (0). V by A2, VECTSP_4:30

.= (0). W by VECTSP_4:36 ;

for x being object holds

( x in W iff x in WW1 + WW2 )

( x in W iff x in WW1 + WW2 ) ;

then W = WW1 + WW2 by A3, VECTSP_4:30;

then I0 is base by A4, FRds2, FRds3, VECTSP_5:def 4;

hence I1 \/ I2 is Basis of (W1 + W2) ; :: thesis: verum

for W1, W2 being Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

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 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let W1, W2 be Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2 st W1 /\ W2 = (0). V holds

I1 \/ I2 is Basis of (W1 + W2)

let I2 be Basis of W2; :: thesis: ( W1 /\ W2 = (0). V implies I1 \/ I2 is Basis of (W1 + W2) )

assume P1: W1 /\ W2 = (0). V ; :: thesis: I1 \/ I2 is Basis of (W1 + W2)

set I = I1 \/ I2;

reconsider W = W1 + W2 as strict Subspace of V ;

reconsider WW1 = W1, WW2 = W2 as Subspace of W by VECTSP_5:7;

( the carrier of WW1 c= the carrier of W & the carrier of WW2 c= the carrier of W ) by VECTSP_4:def 2;

then ( I1 c= the carrier of W & I2 c= the carrier of W ) ;

then reconsider I0 = I1 \/ I2 as Subset of W by XBOOLE_1:8;

reconsider I10 = I1 as Basis of WW1 ;

reconsider I20 = I2 as Basis of WW2 ;

A2: WW1 /\ WW2 is Subspace of V by VECTSP_4:26;

A3: WW1 + WW2 is Subspace of V by VECTSP_4:26;

for x being object holds

( x in WW1 /\ WW2 iff x in (0). V )

proof

then
for x being Vector of V holds
let x be object ; :: thesis: ( x in WW1 /\ WW2 iff x in (0). V )

then ( x in W1 & x in W2 ) by P1, VECTSP_5:3;

hence x in WW1 /\ WW2 by VECTSP_5:3; :: thesis: verum

end;hereby :: thesis: ( x in (0). V implies x in WW1 /\ WW2 )

assume
x in (0). V
; :: thesis: x in WW1 /\ WW2assume
x in WW1 /\ WW2
; :: thesis: x in (0). V

then ( x in WW1 & x in WW2 ) by VECTSP_5:3;

hence x in (0). V by P1, VECTSP_5:3; :: thesis: verum

end;then ( x in WW1 & x in WW2 ) by VECTSP_5:3;

hence x in (0). V by P1, VECTSP_5:3; :: thesis: verum

then ( x in W1 & x in W2 ) by P1, VECTSP_5:3;

hence x in WW1 /\ WW2 by VECTSP_5:3; :: thesis: verum

( x in WW1 /\ WW2 iff x in (0). V ) ;

then A4: WW1 /\ WW2 = (0). V by A2, VECTSP_4:30

.= (0). W by VECTSP_4:36 ;

for x being object holds

( x in W iff x in WW1 + WW2 )

proof

then
for x being Vector of V holds
let x be object ; :: thesis: ( x in W iff x in WW1 + WW2 )

then consider x1, x2 being Vector of W such that

B2: ( x1 in WW1 & x2 in WW2 & x = x1 + x2 ) by VECTSP_5:1;

thus x in W by B2; :: thesis: verum

end;hereby :: thesis: ( x in WW1 + WW2 implies x in W )

assume
x in WW1 + WW2
; :: thesis: x in Wassume
x in W
; :: thesis: x in WW1 + WW2

then consider x1, x2 being Vector of V such that

B2: ( x1 in W1 & x2 in W2 & x = x1 + x2 ) by VECTSP_5:1;

x1 in W1 + W2 by B2, VECTSP_5:2;

then reconsider xx1 = x1 as Vector of W ;

x2 in W1 + W2 by B2, VECTSP_5:2;

then reconsider xx2 = x2 as Vector of W ;

x = xx1 + xx2 by B2, VECTSP_4:13;

hence x in WW1 + WW2 by B2, VECTSP_5:1; :: thesis: verum

end;then consider x1, x2 being Vector of V such that

B2: ( x1 in W1 & x2 in W2 & x = x1 + x2 ) by VECTSP_5:1;

x1 in W1 + W2 by B2, VECTSP_5:2;

then reconsider xx1 = x1 as Vector of W ;

x2 in W1 + W2 by B2, VECTSP_5:2;

then reconsider xx2 = x2 as Vector of W ;

x = xx1 + xx2 by B2, VECTSP_4:13;

hence x in WW1 + WW2 by B2, VECTSP_5:1; :: thesis: verum

then consider x1, x2 being Vector of W such that

B2: ( x1 in WW1 & x2 in WW2 & x = x1 + x2 ) by VECTSP_5:1;

thus x in W by B2; :: thesis: verum

( x in W iff x in WW1 + WW2 ) ;

then W = WW1 + WW2 by A3, VECTSP_4:30;

then I0 is base by A4, FRds2, FRds3, VECTSP_5:def 4;

hence I1 \/ I2 is Basis of (W1 + W2) ; :: thesis: verum