theorem Th3: :: MATRTOP3:3

for r being Real
for f being real-valued FinSequence
for i being Nat st i in dom f holds
Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)