reconsider b = rng b1 as Basis of V by defOrdBasis;
let F1, F2 be FinSequence of INT.Ring; :: thesis: ( len F1 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len F1 holds
F1 /. k = KL . (b1 /. k) ) ) & len F2 = len b1 & ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len F2 holds
F2 /. k = KL . (b1 /. k) ) ) implies F1 = F2 )
assume A7: len F1 = len b1 ; :: thesis: ( for KL being Linear_Combination of V holds
( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st
( 1 <= k & k <= len F1 & not F1 /. k = KL . (b1 /. k) ) ) or not len F2 = len b1 or for KL being Linear_Combination of V holds
( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st
( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 )
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: ( not len F2 = len b1 or for KL being Linear_Combination of V holds
( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st
( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 )
assume A10: len F2 = len b1 ; :: thesis: ( for KL being Linear_Combination of V holds
( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st
( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 )
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: F1 = F2
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

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len F1 implies F1 . k = F2 . k )
assume A14: ( 1 <= k & k <= len F1 ) ; :: thesis: F1 . k = F2 . k
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: verum

end;

hence F1 = F2 by A7, A10, FINSEQ_1:14; :: thesis: verum