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 b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let V1 be finite-dimensional VectSp of K; :: thesis: for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let W1, W2 be Subspace of V1; :: thesis: ( W1 /\ W2 = (0). V1 implies for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A1: W1 /\ W2 = (0). V1 ; :: thesis: for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let b1 be OrdBasis of W1; :: thesis: for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let b2 be OrdBasis of W2; :: thesis: for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let b be OrdBasis of W1 + W2; :: thesis: ( b = b1 ^ b2 implies for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A2: b = b1 ^ b2 ; :: thesis: for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let v, v1, v2 be Vector of (W1 + W2); :: thesis: for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let w1 be Vector of W1; :: thesis: for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
let w2 be Vector of W2; :: thesis: ( v = v1 + v2 & v1 = w1 & v2 = w2 implies v |-- b = (w1 |-- b1) ^ (w2 |-- b2) )
assume A3: ( v = v1 + v2 & v1 = w1 & v2 = w2 ) ; :: thesis: v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
set vb = v |-- b;
set wb1 = w1 |-- b1;
set wb2 = w2 |-- b2;
consider L1 being Linear_Combination of W1 such that
A4: ( w1 = Sum L1 & Carrier L1 c= rng b1 ) and
A5: for k being Nat st 1 <= k & k <= len (w1 |-- b1) holds
(w1 |-- b1) /. k = L1 . (b1 /. k) by MATRLIN:def 9;
A6: W1 is Subspace of W1 + W2 by VECTSP_5:11;
then consider K1 being Linear_Combination of W1 + W2 such that
A7: ( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 ) by Lm4;
consider L2 being Linear_Combination of W2 such that
A8: ( w2 = Sum L2 & Carrier L2 c= rng b2 ) and
A9: for k being Nat st 1 <= k & k <= len (w2 |-- b2) holds
(w2 |-- b2) /. k = L2 . (b2 /. k) by MATRLIN:def 9;
A10: W2 is Subspace of W1 + W2 by VECTSP_5:11;
then consider K2 being Linear_Combination of W1 + W2 such that
A11: ( Carrier K2 = Carrier L2 & Sum K2 = Sum L2 & K2 | the carrier of W2 = L2 ) by Lm4;
consider L being Linear_Combination of W1 + W2 such that
A12: ( v = Sum L & Carrier L c= rng b ) and
A13: for k being Nat st 1 <= k & k <= len (v |-- b) holds
(v |-- b) /. k = L . (b /. k) by MATRLIN:def 9;
reconsider R = rng b as Basis of W1 + W2 by MATRLIN:def 4;
( rng b1 c= R & rng b2 c= R ) by A2, FINSEQ_1:42, FINSEQ_1:43;
then A14: ( Carrier K1 c= R & Carrier K2 c= R & R is linearly-independent ) by A4, A7, A8, A11, VECTSP_7:def 3, XBOOLE_1:1;
then A15: L = K1 + K2 by A4, A7, A8, A11, A12, A3, MATRLIN:10;
A16: ( len (w1 |-- b1) = len b1 & len (w2 |-- b2) = len b2 & len (v |-- b) = len b & len b1 = dim W1 & len b2 = dim W2 & len b = dim (W1 + W2) & len ((w1 |-- b1) ^ (w2 |-- b2)) = (len (w1 |-- b1)) + (len (w2 |-- b2)) ) by Th21, FINSEQ_1:35, MATRLIN:def 9;
[#] ((0). V1) = {(0. V1)} by VECTSP_4:def 3;
then A17: card ([#] ((0). V1)) = 1 by CARD_1:50;
A18: (dim W1) + (dim W2) = (dim (W1 + W2)) + (dim (W1 /\ W2)) by VECTSP_9:36
.= (dim (W1 + W2)) + 0 by A1, A17, RANKNULL:5 ;
then A19: ( dom b = dom ((w1 |-- b1) ^ (w2 |-- b2)) & dom (w1 |-- b1) = dom b1 & dom (v |-- b) = dom b & dom (w2 |-- b2) = dom b2 ) by A16, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len (v |-- b) implies (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k )
assume A20: ( 1 <= k & k <= len (v |-- b) ) ; :: thesis: (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k
A21: k in dom ((w1 |-- b1) ^ (w2 |-- b2)) by A16, A18, A20, FINSEQ_3:27;

now

per cases ( k in dom (w1 |-- b1) or ex n being Nat st
( n in dom (w2 |-- b2) & k = (len (w1 |-- b1)) + n ) ) by A21, FINSEQ_1:38;

suppose A22: k in dom (w1 |-- b1) ; :: thesis: ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . k

then ( 1 <= k & k <= len (w1 |-- b1) ) by FINSEQ_3:27;
then A23: L1 . (b1 /. k) = (w1 |-- b1) /. k by A5
.= (w1 |-- b1) . k by A22, PARTFUN1:def 8
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A22, FINSEQ_1:def 7 ;
A24: K1 . (b1 /. k) = L1 . (b1 /. k) by A7, FUNCT_1:72;
reconsider b1k = b1 /. k as Vector of (W1 + W2) by A6, VECTSP_4:18;
not b1 /. k in Carrier K2

proof

assume A25: b1 /. k in Carrier K2 ; :: thesis: contradiction
then ( b1 /. k in W2 & b1 /. k in W1 ) by A11, STRUCT_0:def 5;
then b1 /. k in W1 /\ W2 by VECTSP_5:7;
then b1 /. k in the carrier of ((0). V1) by A1, STRUCT_0:def 5;
then b1 /. k in {(0. V1)} by VECTSP_4:def 3;
then b1 /. k = 0. V1 by TARSKI:def 1
.= 0. (W1 + W2) by VECTSP_4:19 ;
hence contradiction by A25, A14, VECTSP_7:3; :: thesis: verum

end;

then K2 . b1k = 0. K ;
then A26: L . b1k = (K1 . b1k) + (0. K) by A15, VECTSP_6:def 11
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A23, A24, RLVECT_1:def 7 ;
b1k = b1 . k by A19, A22, PARTFUN1:def 8
.= b . k by A19, A22, A2, FINSEQ_1:def 7
.= b /. k by A19, A21, PARTFUN1:def 8 ;
hence ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) /. k by A20, A13, A26
.= (v |-- b) . k by A19, A21, PARTFUN1:def 8 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (w2 |-- b2) & k = (len (w1 |-- b1)) + n ) ; :: thesis: ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) . k

then consider n being Nat such that
A27: ( n in dom (w2 |-- b2) & k = (len (w1 |-- b1)) + n ) ;
( 1 <= n & n <= len (w2 |-- b2) ) by A27, FINSEQ_3:27;
then A28: L2 . (b2 /. n) = (w2 |-- b2) /. n by A9
.= (w2 |-- b2) . n by A27, PARTFUN1:def 8
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A27, FINSEQ_1:def 7 ;
A29: K2 . (b2 /. n) = L2 . (b2 /. n) by A11, FUNCT_1:72;
reconsider b2n = b2 /. n as Vector of (W1 + W2) by A10, VECTSP_4:18;
not b2 /. n in Carrier K1

proof

assume A30: b2 /. n in Carrier K1 ; :: thesis: contradiction
then ( b2 /. n in W2 & b2 /. n in W1 ) by A7, STRUCT_0:def 5;
then b2 /. n in W1 /\ W2 by VECTSP_5:7;
then b2 /. n in the carrier of ((0). V1) by A1, STRUCT_0:def 5;
then b2 /. n in {(0. V1)} by VECTSP_4:def 3;
then b2 /. n = 0. V1 by TARSKI:def 1
.= 0. (W1 + W2) by VECTSP_4:19 ;
hence contradiction by A30, A14, VECTSP_7:3; :: thesis: verum

end;

then K1 . b2n = 0. K ;
then A31: L . b2n = (0. K) + (K2 . b2n) by A15, VECTSP_6:def 11
.= ((w1 |-- b1) ^ (w2 |-- b2)) . k by A28, A29, RLVECT_1:def 7 ;
b2n = b2 . n by A19, A27, PARTFUN1:def 8
.= b . k by A16, A19, A27, A2, FINSEQ_1:def 7
.= b /. k by A19, A21, PARTFUN1:def 8 ;
hence ((w1 |-- b1) ^ (w2 |-- b2)) . k = (v |-- b) /. k by A20, A13, A31
.= (v |-- b) . k by A19, A21, PARTFUN1:def 8 ;
:: thesis: verum

end;

end;

end;

hence (v |-- b) . k = ((w1 |-- b1) ^ (w2 |-- b2)) . k ; :: thesis: verum

end;

hence v |-- b = (w1 |-- b1) ^ (w2 |-- b2) by A16, A18, FINSEQ_1:18; :: thesis: verum