theorem LMThGM21: :: ZMODLAT2:65

for L being non trivial positive-definite RATional Z_Lattice
for v being Element of L
for b being FinSequence of L
for sbv being FinSequence of F_Rat st len b = len sbv & ( for n being Nat st n in dom sbv holds
sbv . n = <;(b /. n),v;> ) holds
<;(Sum b),v;> = Sum sbv