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_2:12 ;
A5: width (QuadraticForm x,M,y) = len y by A1, A2, Def13;
then A6: width ((QuadraticForm x,M,y) @ ) = len (QuadraticForm x,M,y) by A3, MATRIX_2:12;
len (M @" ) = len (M @ ) by Def1;
then A7: len (M @" ) = width M by MATRIX_1:def 7;
A8: len (x *' ) = len x by COMPLSP2:def 1;
A9: len ((QuadraticForm x,M,y) @ ) = width (QuadraticForm x,M,y) by MATRIX_1:def 7;
A10: len (M @" ) = len (M @ ) by Def1
.= len y by A2, MATRIX_1:def 7 ;
then A11: width (QuadraticForm y,(M @" ),x) = len x by A4, Def13;
A12: len ((QuadraticForm y,(M @" ),x) *' ) = len (QuadraticForm y,(M @" ),x) by Def1
.= len y by A10, A4, Def13 ;
A13: len ((QuadraticForm x,M,y) @ ) = width (QuadraticForm x,M,y) by MATRIX_1:def 7
.= len y by A1, A2, Def13 ;
A14: len (QuadraticForm y,(M @" ),x) = len y by A10, A4, Def13;
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 13;
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, Def13;
A20: 1 <= i by A16, Th1;
A21: i <= width (QuadraticForm x,M,y) by A9, A16, Th1;
then i <= width M by A1, A2, Def13;
then A22: [j,i] in Indices M by A17, A20, A19, Th1;
A23: j <= width (M @" ) by A1, A2, A4, A18, Def13;
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, Def13;
then A26: [i,j] in Indices (M @" ) by A17, A24, A23, Th1;
A27: j <= len x by A1, A2, A18, Def13;
A28: j <= len x by A1, A2, A18, Def13;
A29: j <= width (QuadraticForm y,(M @" ),x) by A1, A2, A11, A18, Def13;
A30: 1 <= i by A16, Th1;
i <= len (QuadraticForm y,(M @" ),x) by A1, A2, A14, A21, Def13;
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, Def13
.= (((y . i) * ((M @" ) * i9,j9)) * ((x *' ) . j)) *' by A17, A27, COMPLSP2:def 1
.= (((y . i) * ((M @" ) * i,j)) *' ) * (((x *' ) . j) *' ) by COMPLEX1:121
.= (((y . i) * ((M @" ) * i9,j9)) *' ) * (((x *' ) *' ) . j) by A8, A17, A28, COMPLSP2:def 1
.= (((y . i) *' ) * (((M @" ) * i,j) *' )) * (((x *' ) *' ) . j) by COMPLEX1:121
.= (((y . i) *' ) * (((M @" ) *' ) * i,j)) * (((x *' ) *' ) . j) by A26, Def1
.= (((y . i) *' ) * (((M @" ) *' ) * i,j)) * (x . j) by COMPLSP2:22
.= (((y . i) *' ) * ((M @ ) * i,j)) * (x . j) by Th2
.= (((y . i) *' ) * (M * j,i)) * (x . j) by A22, MATRIX_1:def 7
.= ((x . j) * (M * j,i)) * ((y . i) *' )
.= (QuadraticForm x,M,y) * j,i by A1, A2, A22, Def13
.= ((QuadraticForm x,M,y) @ ) * i,j by A25, MATRIX_1:def 7 ;
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, Def13 ;
width ((QuadraticForm x,M,y) @ ) = len (QuadraticForm x,M,y) by A3, A5, MATRIX_2:12
.= len x by A1, A2, Def13 ;
hence (QuadraticForm x,M,y) @ = (QuadraticForm y,(M @" ),x) *' by A13, A12, A31, A15, MATRIX_1:21; :: thesis: verum