let x, y be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
let M be Matrix of REAL; :: thesis: ( len x = len M & len y = width M & len y > 0 implies (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x) )
assume that
A1: len x = len M and
A2: len y = width M and
A3: len y > 0 ; :: thesis: (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
A4: len (M @) = len y by A2, MATRIX_0:def 6;
A5: width (M @) = len x by A1, A2, A3, MATRIX_0:54;
then A6: ( len (QuadraticForm (y,(M @),x)) = len y & width (QuadraticForm (y,(M @),x)) = len x ) by A4, Def4;
A7: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_0:def 6;
A8: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def4;
then A9: width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, MATRIX_0:54;
A10: for i, j being Nat st [i,j] in Indices ((QuadraticForm (x,M,y)) @) holds
(QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((QuadraticForm (x,M,y)) @) implies (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) )
assume A11: [i,j] in Indices ((QuadraticForm (x,M,y)) @) ; :: thesis: (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
reconsider i = i, j = j as Nat ;
A12: 1 <= j by A11, MATRIXC1:1;
A13: j <= len (QuadraticForm (x,M,y)) by A9, A11, MATRIXC1:1;
then A14: j <= len M by A1, A2, Def4;
A15: 1 <= i by A11, MATRIXC1:1;
A16: i <= width (QuadraticForm (x,M,y)) by A7, A11, MATRIXC1:1;
then i <= width M by A1, A2, Def4;
then A17: [j,i] in Indices M by A12, A15, A14, MATRIXC1:1;
A18: j <= width (M @) by A1, A2, A5, A13, Def4;
A19: 1 <= i by A11, MATRIXC1:1;
1 <= i by A11, MATRIXC1:1;
then A20: [j,i] in Indices (QuadraticForm (x,M,y)) by A16, A12, A13, MATRIXC1:1;
i <= len (M @) by A1, A2, A4, A16, Def4;
then [i,j] in Indices (M @) by A12, A19, A18, MATRIXC1:1;
then (QuadraticForm (y,(M @),x)) * (i,j) = ((y . i) * ((M @) * (i,j))) * (x . j) by A4, A5, Def4
.= ((y . i) * (M * (j,i))) * (x . j) by A17, MATRIX_0:def 6
.= ((x . j) * (M * (j,i))) * (y . i)
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A17, Def4
.= ((QuadraticForm (x,M,y)) @) * (i,j) by A20, MATRIX_0:def 6 ;
hence (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) ; :: thesis: verum

end;

A21: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_0:def 6
.= len y by A1, A2, Def4 ;
width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, A8, MATRIX_0:54
.= len x by A1, A2, Def4 ;
hence (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x) by A21, A6, A10, MATRIX_0:21; :: thesis: verum