let F1, F2 be FinSequence of K; :: 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 and
A9: Carrier KL1 c= rng b1 and
A10: 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 A11: 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 A12: W = Sum KL2 and
A13: Carrier KL2 c= rng b1 and
A14: for k being Nat st 1 <= k & k <= len F2 holds
F2 /. k = KL2 . (b1 /. k) ; :: thesis: F1 = F2
reconsider b = rng b1 as Basis of V by Def4;
A15: 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 A16: ( 1 <= k & k <= len F1 ) ; :: thesis: F1 . k = F2 . k
then A17: k in dom F1 by FINSEQ_3:27;
A18: k in dom F2 by A7, A11, A16, FINSEQ_3:27;
thus F1 . k = F1 /. k by A17, PARTFUN1:def 8
.= KL1 . (b1 /. k) by A10, A16
.= KL2 . (b1 /. k) by A8, A9, A12, A13, A15, Th9
.= F2 /. k by A7, A11, A14, A16
.= F2 . k by A18, PARTFUN1:def 8 ; :: thesis: verum

end;

hence F1 = F2 by A7, A11, FINSEQ_1:18; :: thesis: verum