theorem Th1: :: ZMODUL03:1

for V being Z_Module
for u being Vector of V ex l being Linear_Combination of V st
( l . u = 1 & ( for v being Vector of V st v <> u holds
l . v = 0 ) )