theorem Th34: :: BKMODEL1:39

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
|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|