:: deftheorem Def7 defines |-- ZMATRLIN:def 7 :
for V being free finite-rank Z_Module
for b1 being OrdBasis of V
for W being Element of V
for b₄ being FinSequence of INT.Ring 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) ) ) ) );