reconsider b = rng b1 as Basis of V by Def2;

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 & 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

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 & 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

hence
F1 = F2
by A7, A10, FINSEQ_1:14; :: thesis: verum
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;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