theorem Th80: :: ANPROJ_8:99

for uf being FinSequence of F_Real st len uf = 3 holds
<*uf*> @ = (1. (F_Real,3)) * (<*uf*> @)