reconsider b = rng b1 as Basis of V by Def2;
let F1, F2 be FinSequence of K; :: thesis:
assume A7: len F1 = len b1 ; :: thesis:
given KL1 being Linear_Combination of V such that A8: ( W = Sum KL1 & Carrier KL1 c= rng b1 ) and
A9: for k being Nat st 1 <= k & k <= len F1 holds
F1 /. k = KL1 . (b1 /. k) ; :: thesis:
assume A10: len F2 = len b1 ; :: thesis:
given KL2 being Linear_Combination of V such that A11: ( W = Sum KL2 & Carrier KL2 c= rng b1 ) and
A12: for k being Nat st 1 <= k & k <= len F2 holds
F2 /. k = KL2 . (b1 /. k) ; :: thesis:
A13: b is linearly-independent by VECTSP_7:def 3;
for k being Nat st 1 <= k & k <= len F1 holds
F1 . k = F2 . k

let k be Nat; :: thesis:
assume A14: ( 1 <= k & k <= len F1 ) ; :: thesis:
then A15: k in dom F2 by A7, A10, FINSEQ_3:25;
k in dom F1 by A14, FINSEQ_3:25;
hence F1 . k = F1 /. k by PARTFUN1:def 6
.= KL1 . (b1 /. k) by A9, A14
.= KL2 . (b1 /. k) by A8, A11, A13, Th5
.= F2 /. k by A7, A10, A12, A14
.= F2 . k by A15, PARTFUN1:def 6 ;
:: thesis:

end;