:: deftheorem defCoord defines Coordinate ZMATRLIN:def 11 :
for V being free Z_Module
for B being Basis of V
for u being Vector of V
for b₄ being Function of V,INT.Ring holds
( b₄ = Coordinate (u,B) iff ( ( for v being Vector of V ex Lu being Linear_Combination of B st
( v = Sum Lu & b₄ . v = Lu . u ) ) & ( for v being Vector of V
for Lv being Linear_Combination of B st v = Sum Lv holds
b₄ . v = Lv . u ) & ( for v1, v2 being Vector of V holds b₄ . (v1 + v2) = (b₄ . v1) + (b₄ . v2) ) & ( for v being Vector of V
for r being Element of INT.Ring holds b₄ . (r * v) = r * (b₄ . v) ) ) );