let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2
let V1 be finite-dimensional VectSp of K; :: thesis: for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2
let W1, W2 be Subspace of V1; :: thesis: ( W1 /\ W2 = (0). V1 implies for w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2 )
assume A1: W1 /\ W2 = (0). V1 ; :: thesis: for w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2
let w1 be OrdBasis of W1; :: thesis: for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2
let w2 be OrdBasis of W2; :: thesis: w1 ^ w2 is OrdBasis of W1 + W2
reconsider R1 = rng w1 as Basis of W1 by MATRLIN:def 2;
reconsider R2 = rng w2 as Basis of W2 by MATRLIN:def 2;
A2: R1 \/ R2 = rng (w1 ^ w2) by FINSEQ_1:31;
A3: R1 misses R2
proof
assume R1 meets R2 ; :: thesis: contradiction
then consider x being object such that
A4: x in R1 and
A5: x in R2 by XBOOLE_0:3;
( x in W1 & x in W2 ) by A4, A5;
then x in W1 /\ W2 by VECTSP_5:3;
then x in the carrier of ((0). V1) by A1;
then x in {(0. V1)} by VECTSP_4:def 3;
then x = 0. V1 by TARSKI:def 1
.= 0. W1 by VECTSP_4:11 ;
then not R1 is linearly-independent by A4, VECTSP_7:2;
hence contradiction by VECTSP_7:def 3; :: thesis: verum
end;
A6: R1 \/ R2 is Basis of (W1 + W2) by A1, Th3;
then reconsider w12 = w1 ^ w2 as FinSequence of (W1 + W2) by A2, FINSEQ_1:def 4;
( w1 is one-to-one & w2 is one-to-one ) by MATRLIN:def 2;
then w12 is one-to-one by A3, FINSEQ_3:91;
hence w1 ^ w2 is OrdBasis of W1 + W2 by A6, A2, MATRLIN:def 2; :: thesis: verum