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, Def12
.= 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 12;
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, Def12;
i <= len M by A1, A2, A12, Def12;
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, Def12;
j <= width M by A1, A2, A15, Def12;
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, Def12;
A20: 1 <= i by A10, Th1;
A21: 1 <= j by A10, Th1;
i <= len M by A1, A2, A12, Def12;
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, Def12
.= (((x . i) * (M * (i9,j9))) * ((y *') . j)) *' by A21, A16, COMPLSP2:def 1
.= (((x . i) * (M * (i,j))) *') * (((y *') . j) *') by COMPLEX1:35
.= (((x . i) * (M * (i9,j9))) *') * (((y *') *') . j) by A3, A21, A16, COMPLSP2:def 1
.= (((x . i) *') * ((M * (i,j)) *')) * (((y *') *') . j) by COMPLEX1:35
.= (((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, Def12 ;
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, Def12 ;
A24: width (QuadraticForm ((x *'),(M *'),(y *'))) = len (y *') by A5, A4, Def12
.= len y by COMPLSP2:def 1 ;
len ((QuadraticForm (x,M,y)) *') = len (QuadraticForm (x,M,y)) by Def1
.= len M by A1, A2, Def12 ;
hence (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *')) by A6, A23, A24, A9, MATRIX_0:21; :: thesis: verum