let x, y be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX 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 COMPLEX; :: 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: width (M @") = width (M @) by Def1
.= len x by A1, A2, A3, MATRIX_0:54 ;
A5: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def12;
then A6: width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, MATRIX_0:54;
len (M @") = len (M @) by Def1;
then A7: len (M @") = width M by MATRIX_0:def 6;
A8: len (x *') = len x by COMPLSP2:def 1;
A9: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_0:def 6;
A10: len (M @") = len (M @) by Def1
.= len y by A2, MATRIX_0:def 6 ;
then A11: width (QuadraticForm (y,(M @"),x)) = len x by A4, Def12;
A12: len ((QuadraticForm (y,(M @"),x)) *') = len (QuadraticForm (y,(M @"),x)) by Def1
.= len y by A10, A4, Def12 ;
A13: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_0:def 6
.= len y by A1, A2, Def12 ;
A14: len (QuadraticForm (y,(M @"),x)) = len y by A10, A4, Def12;
A15: 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) )
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
assume A16: [i,j] in Indices ((QuadraticForm (x,M,y)) @) ; :: thesis: ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
then A17: 1 <= j by Th1;
A18: j <= len (QuadraticForm (x,M,y)) by A6, A16, Th1;
then A19: j <= len M by A1, A2, Def12;
A20: 1 <= i by A16, Th1;
A21: i <= width (QuadraticForm (x,M,y)) by A9, A16, Th1;
then i <= width M by A1, A2, Def12;
then A22: [j,i] in Indices M by A17, A20, A19, Th1;
A23: j <= width (M @") by A1, A2, A4, A18, Def12;
A24: 1 <= i by A16, Th1;
1 <= i by A16, Th1;
then A25: [j,i] in Indices (QuadraticForm (x,M,y)) by A21, A17, A18, Th1;
i <= len (M @") by A1, A2, A7, A21, Def12;
then A26: [i,j] in Indices (M @") by A17, A24, A23, Th1;
A27: j <= len x by A1, A2, A18, Def12;
A28: j <= len x by A1, A2, A18, Def12;
A29: j <= width (QuadraticForm (y,(M @"),x)) by A1, A2, A11, A18, Def12;
A30: 1 <= i by A16, Th1;
i <= len (QuadraticForm (y,(M @"),x)) by A1, A2, A14, A21, Def12;
then [i,j] in Indices (QuadraticForm (y,(M @"),x)) by A17, A30, A29, Th1;
then ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (y,(M @"),x)) * (i,j)) *' by Def1
.= (((y . i) * ((M @") * (i,j))) * ((x . j) *')) *' by A10, A4, A26, Def12
.= (((y . i) * ((M @") * (i9,j9))) * ((x *') . j)) *' by A17, A27, COMPLSP2:def 1
.= (((y . i) * ((M @") * (i,j))) *') * (((x *') . j) *') by COMPLEX1:35
.= (((y . i) * ((M @") * (i9,j9))) *') * (((x *') *') . j) by A8, A17, A28, COMPLSP2:def 1
.= (((y . i) *') * (((M @") * (i,j)) *')) * (((x *') *') . j) by COMPLEX1:35
.= (((y . i) *') * (((M @") *') * (i,j))) * (((x *') *') . j) by A26, Def1
.= (((y . i) *') * (((M @") *') * (i,j))) * (x . j)
.= (((y . i) *') * ((M @) * (i,j))) * (x . j)
.= (((y . i) *') * (M * (j,i))) * (x . j) by A22, MATRIX_0:def 6
.= ((x . j) * (M * (j,i))) * ((y . i) *')
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A22, Def12
.= ((QuadraticForm (x,M,y)) @) * (i,j) by A25, MATRIX_0:def 6 ;
hence ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) ; :: thesis: verum

end;

A31: width ((QuadraticForm (y,(M @"),x)) *') = width (QuadraticForm (y,(M @"),x)) by Def1
.= len x by A10, A4, Def12 ;
width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, A5, MATRIX_0:54
.= len x by A1, A2, Def12 ;
hence (QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *' by A13, A12, A31, A15, MATRIX_0:21; :: thesis: verum