let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for W1 being Subspace of V1 st W1 = (Omega). V1 holds
for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for W1 being Subspace of V1 st W1 = (Omega). V1 holds
for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let b1 be OrdBasis of V1; :: thesis: for W1 being Subspace of V1 st W1 = (Omega). V1 holds
for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let W1 be Subspace of V1; :: thesis: ( W1 = (Omega). V1 implies for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1 )
assume A1: W1 = (Omega). V1 ; :: thesis: for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let w be Vector of W1; :: thesis: for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let v be Vector of V1; :: thesis: for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1
let w1 be OrdBasis of W1; :: thesis: ( v = w & b1 = w1 implies v |-- b1 = w |-- w1 )
assume that
A2: v = w and
A3: b1 = w1 ; :: thesis: v |-- b1 = w |-- w1
consider KL being Linear_Combination of W1 such that
A4: ( w = Sum KL & Carrier KL c= rng w1 ) and
A5: for k being Nat st 1 <= k & k <= len (w |-- w1) holds
(w |-- w1) /. k = KL . (w1 /. k) by MATRLIN:def 7;
consider K1 being Linear_Combination of V1 such that
A6: ( Carrier K1 = Carrier KL & Sum K1 = Sum KL ) and
A7: K1 | the carrier of W1 = KL by Lm4;
A8: len w1 = len (w |-- w1) by MATRLIN:def 7;

now :: thesis: for k being Nat st 1 <= k & k <= len (w |-- w1) holds
(w |-- w1) /. k = K1 . (b1 /. k)

let k be Nat; :: thesis: ( 1 <= k & k <= len (w |-- w1) implies (w |-- w1) /. k = K1 . (b1 /. k) )
assume A9: ( 1 <= k & k <= len (w |-- w1) ) ; :: thesis: (w |-- w1) /. k = K1 . (b1 /. k)
A10: k in dom w1 by A8, A9, FINSEQ_3:25;
dom K1 = the carrier of W1 by A1, FUNCT_2:def 1;
then KL = K1 by A7;
hence (w |-- w1) /. k = K1 . (w1 /. k) by A5, A9
.= K1 . (w1 . k) by A10, PARTFUN1:def 6
.= K1 . (b1 /. k) by A3, A10, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence v |-- b1 = w |-- w1 by A2, A3, A4, A6, A8, MATRLIN:def 7; :: thesis: verum