theorem LmND1: :: ZMODUL08:15

for V being non trivial free Z_Module
for v being non zero Vector of V
for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )