let x, y be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len x = len M & len y = width M holds
(QuadraticForm x,M,y) *' = QuadraticForm (x *' ),(M *' ),(y *' )
let M be Matrix of COMPLEX ; :: thesis: ( len x = len M & len y = width M implies (QuadraticForm x,M,y) *' = QuadraticForm (x *' ),(M *' ),(y *' ) )
assume that
A1: len x = len M and
A2: len y = width M ; :: thesis: (QuadraticForm x,M,y) *' = QuadraticForm (x *' ),(M *' ),(y *' )
A3: len (y *' ) = len y by COMPLSP2:def 1;
then A4: len (y *' ) = width (M *' ) by A2, Def1;
len (M *' ) = len M by Def1;
then A5: len (x *' ) = len (M *' ) by A1, COMPLSP2:def 1;
then A6: len (QuadraticForm (x *' ),(M *' ),(y *' )) = len (x *' ) by A4, Def13
.= len M by A1, COMPLSP2:def 1 ;
A7: width ((QuadraticForm x,M,y) *' ) = width (QuadraticForm x,M,y) by Def1;
A8: len ((QuadraticForm x,M,y) *' ) = len (QuadraticForm x,M,y) by Def1;
A9: for i, j being Nat st [i,j] in Indices ((QuadraticForm x,M,y) *' ) holds
((QuadraticForm x,M,y) *' ) * 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 x,M,y) *' ) * i,j = (QuadraticForm (x *' ),(M *' ),(y *' )) * i,j )
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
assume A10: [i,j] in Indices ((QuadraticForm x,M,y) *' ) ; :: thesis: ((QuadraticForm x,M,y) *' ) * i,j = (QuadraticForm (x *' ),(M *' ),(y *' )) * i,j
then A11: 1 <= i by Th1;
A12: i <= len (QuadraticForm x,M,y) by A8, A10, Th1;
then A13: i <= len x by A1, A2, Def13;
i <= len M by A1, A2, A12, Def13;
then A14: i <= len (M *' ) by Def1;
A15: j <= width (QuadraticForm x,M,y) by A7, A10, Th1;
then A16: j <= len y by A1, A2, Def13;
j <= width M by A1, A2, A15, Def13;
then A17: j <= width (M *' ) by Def1;
1 <= j by A10, Th1;
then A18: [i,j] in Indices (M *' ) by A11, A14, A17, Th1;
A19: j <= width M by A1, A2, A15, Def13;
A20: 1 <= i by A10, Th1;
A21: 1 <= j by A10, Th1;
i <= len M by A1, A2, A12, Def13;
then A22: [i,j] in Indices M by A21, A20, A19, Th1;
[i,j] in Indices (QuadraticForm x,M,y) by A11, A12, A21, A15, Th1;
then ((QuadraticForm x,M,y) *' ) * i,j = ((QuadraticForm x,M,y) * i,j) *' by Def1
.= (((x . i) * (M * i,j)) * ((y . j) *' )) *' by A1, A2, A22, Def13
.= (((x . i) * (M * i9,j9)) * ((y *' ) . j)) *' by A21, A16, COMPLSP2:def 1
.= (((x . i) * (M * i,j)) *' ) * (((y *' ) . j) *' ) by COMPLEX1:121
.= (((x . i) * (M * i9,j9)) *' ) * (((y *' ) *' ) . j) by A3, A21, A16, COMPLSP2:def 1
.= (((x . i) *' ) * ((M * i,j) *' )) * (((y *' ) *' ) . j) by COMPLEX1:121
.= (((x . i) *' ) * ((M *' ) * i,j)) * (((y *' ) *' ) . j) by A22, Def1
.= (((x . i) *' ) * ((M *' ) * i9,j9)) * (((y *' ) . j) *' ) by A3, A21, A16, COMPLSP2:def 1
.= (((x *' ) . i) * ((M *' ) * i9,j9)) * (((y *' ) . j) *' ) by A11, A13, COMPLSP2:def 1
.= (QuadraticForm (x *' ),(M *' ),(y *' )) * i,j by A5, A4, A18, Def13 ;
hence ((QuadraticForm x,M,y) *' ) * i,j = (QuadraticForm (x *' ),(M *' ),(y *' )) * i,j ; :: thesis: verum

end;

A23: width ((QuadraticForm x,M,y) *' ) = width (QuadraticForm x,M,y) by Def1
.= len y by A1, A2, Def13 ;
A24: width (QuadraticForm (x *' ),(M *' ),(y *' )) = len (y *' ) by A5, A4, Def13
.= len y by COMPLSP2:def 1 ;
len ((QuadraticForm x,M,y) *' ) = len (QuadraticForm x,M,y) by Def1
.= len M by A1, A2, Def13 ;
hence (QuadraticForm x,M,y) *' = QuadraticForm (x *' ),(M *' ),(y *' ) by A6, A23, A24, A9, MATRIX_1:21; :: thesis: verum