:: deftheorem Def7 defines |-- MATRLIN:def 7 :
for K being Field
for V being finite-dimensional VectSp of K
for b1 being OrdBasis of V
for W being Element of V
for b₅ being FinSequence of K holds
( b₅ = W |-- b1 iff ( len b₅ = 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 b₅ holds
b₅ /. k = KL . (b1 /. k) ) ) ) );