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_1:def 7;
A5: width (M @ ) = len x by A1, A2, A3, MATRIX_2:12;
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_1:def 7;
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_2:12;
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 Element of NAT by ORDINAL1:def 13;
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_1:def 7
.= ((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_1:def 7 ;
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_1:def 7
.= len y by A1, A2, Def4 ;
width ((QuadraticForm x,M,y) @ ) = len (QuadraticForm x,M,y) by A3, A8, MATRIX_2:12
.= len x by A1, A2, Def4 ;
hence (QuadraticForm x,M,y) @ = QuadraticForm y,(M @ ),x by A21, A6, A10, MATRIX_1:21; :: thesis: verum