let a, b be 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)))
let p be 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)))
let M be Matrix of 3,REAL; ( len p = 3 implies SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p))) )
assume A1:
len p = 3
; SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))
A2:
( len M = 3 & width M = 3 )
by MATRIX_0:23;
then A3:
len (a * p) = len M
by A1, RVSUM_1:117;
( len (b * p) = width M & len (b * p) > 0 )
by A1, A2, RVSUM_1:117;
then A4:
SumAll (QuadraticForm ((a * p),M,(b * p))) = |((a * p),(M * (b * p)))|
by A3, MATRPROB:44;
( len p = len M & len p = width M & len p > 0 )
by A1, MATRIX_0:23;
then
SumAll (QuadraticForm (p,M,p)) = |(p,(M * p))|
by MATRPROB:44;
hence
SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))
by A4, A1, Th34; verum