theorem Th35: :: BKMODEL1:40

for a, b being Element of F_Real
for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3 holds
SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))