let a, b be Element of F_Real; :: thesis: 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 ; :: thesis: 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; :: thesis: ( len p = 3 implies SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p))) )
assume A1: len p = 3 ; :: thesis: 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; :: thesis: verum