matrixc1.miz

begin

 reserve i,j,n,k for Nat,

a for Element of COMPLEX ,

R1,R2 for Element of (i -tuples_on COMPLEX );

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def1

 func M *' -> Matrix of COMPLEX means

 : Def1: ( len it ) = ( len M) & ( width it ) = ( width M) & for i,j be Nat st [i, j] in ( Indices M) holds (it * (i,j)) = ((M * (i,j)) *' );

 existence

 proof

 deffunc F( Nat, Nat) = ( In (((M * ($1,$2)) *' ), COMPLEX ));

 consider M1 be Matrix of ( len M), ( width M), COMPLEX such that

 A1: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = F(i,j) from MATRIX_0:sch 1;

 take M1;

 thus

 A2: ( len M1) = ( len M) by MATRIX_0:def 2;

 now

 per cases ;

 suppose

 A4: ( len M) = 0 ;

 then ( width M1) = 0 by A2, MATRIX_0:def 3;

 hence ( width M1) = ( width M) by A4, MATRIX_0:def 3;

 end;

 suppose ( len M) > 0 ;

 hence ( width M1) = ( width M) by MATRIX_0: 23;

 end;

 end;



 A5: ( dom M) = ( dom M1) by A2, FINSEQ_3: 29;

 let i,j be Nat;

 assume [i, j] in ( Indices M);

 then [i, j] in ( Indices M1) by A3, A5;

 then (M1 * (i,j)) = F(i,j) by A1;

 hence thesis;

 end;

 uniqueness

 proof

 let M1,M2 be Matrix of COMPLEX ;

 assume that

 A6: ( len M1) = ( len M) and

 A7: ( width M1) = ( width M) and

 A8: for i, j st [i, j] in ( Indices M) holds (M1 * (i,j)) = ((M * (i,j)) *' ) and

 A9: ( len M2) = ( len M) and

 A10: ( width M2) = ( width M) and

 A11: for i, j st [i, j] in ( Indices M) holds (M2 * (i,j)) = ((M * (i,j)) *' );

 now

 let i, j;

 assume

 A12: [i, j] in ( Indices M1);



 A13: ( dom M1) = ( dom M) by A6, FINSEQ_3: 29;



 hence (M1 * (i,j)) = ((M * (i,j)) *' ) by A7, A8, A12

 .= (M2 * (i,j)) by A7, A11, A12, A13;

 end;

 hence thesis by A6, A7, A9, A10, MATRIX_0: 21;

 end;

 involutiveness

 proof

 let N,M be Matrix of COMPLEX ;

 assume that

 A14: ( len N) = ( len M) and

 A15: ( width N) = ( width M) and

 A16: for i,j be Nat st [i, j] in ( Indices M) holds (N * (i,j)) = ((M * (i,j)) *' );

 thus ( len M) = ( len N) by A14;

 thus ( width M) = ( width N) by A15;

 let i,j be Nat such that

 A17: [i, j] in ( Indices N);

 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M) by A14, A15, A17, MATRIX_0: 32;

 then

 A18: [i, j] in ( Indices M) by MATRIX_0: 30;



 thus (M * (i,j)) = (((M * (i,j)) *' ) *' )

 .= ((N * (i,j)) *' ) by A18, A16;

 end;

 end

 theorem :: MATRIXC1:1



 Th1: for M be tabular FinSequence holds [i, j] in ( Indices M) iff 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M)

 proof

 let M be tabular FinSequence;

 thus [i, j] in ( Indices M) implies 1 <= i & i <= ( len M) & 1 <= j & j <= ( width M)

 proof

 assume

 A1: [i, j] in ( Indices M);

 then [i, j] in [:( Seg ( len M)), ( Seg ( width M)):] by FINSEQ_1:def 3;

 then

 A2: i in ( Seg ( len M)) by ZFMISC_1: 87;

 j in ( Seg ( width M)) by A1, ZFMISC_1: 87;

 hence thesis by A2, FINSEQ_1: 1;

 end;

 assume that

 A3: 1 <= i and

 A4: i <= ( len M) and

 A5: 1 <= j and

 A6: j <= ( width M);



 A7: j in ( Seg ( width M)) by A5, A6, FINSEQ_1: 1;

 i in ( dom M) by A3, A4, FINSEQ_3: 25;

 hence thesis by A7, ZFMISC_1: 87;

 end;

 ::$Canceled

 theorem :: MATRIXC1:3



 Th2: for a be Complex, M be Matrix of COMPLEX holds ( len (a * M)) = ( len M) & ( width (a * M)) = ( width M)

 proof

 let a be Complex, M be Matrix of COMPLEX ;

 a in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider ea = a as Element of F_Complex by COMPLFLD:def 1;



 A1: ( width (a * M)) = ( width ( COMPLEX2Field (a * M))) by MATRIX_5: 7

 .= ( width ( COMPLEX2Field ( Field2COMPLEX (ea * ( COMPLEX2Field M))))) by MATRIX_5:def 7

 .= ( width (ea * ( COMPLEX2Field M))) by MATRIX_5: 6

 .= ( width ( COMPLEX2Field M)) by MATRIX_3:def 5

 .= ( width M) by MATRIX_5:def 1;

 ( len (a * M)) = ( len ( COMPLEX2Field (a * M))) by MATRIX_5: 7

 .= ( len ( COMPLEX2Field ( Field2COMPLEX (ea * ( COMPLEX2Field M))))) by MATRIX_5:def 7

 .= ( len (ea * ( COMPLEX2Field M))) by MATRIX_5: 6

 .= ( len ( COMPLEX2Field M)) by MATRIX_3:def 5

 .= ( len M) by MATRIX_5:def 1;

 hence thesis by A1;

 end;

 theorem :: MATRIXC1:4



 Th3: for i,j be Nat, a be Complex, M be Matrix of COMPLEX st [i, j] in ( Indices M) holds ((a * M) * (i,j)) = (a * (M * (i,j)))

 proof

 let i,j be Nat, a be Complex, M be Matrix of COMPLEX ;

 reconsider m1 = ( COMPLEX2Field M) as Matrix of COMPLEX by COMPLFLD:def 1;



 A1: (M * (i,j)) = (m1 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M) * (i,j)) by COMPLFLD:def 1;

 assume [i, j] in ( Indices M);

 then

 A2: [i, j] in ( Indices ( COMPLEX2Field M)) by MATRIX_5:def 1;

 a in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider aa = a as Element of F_Complex by COMPLFLD:def 1;

 reconsider m = ( COMPLEX2Field (a * M)) as Matrix of COMPLEX by COMPLFLD:def 1;



 A3: ( COMPLEX2Field (a * M)) = ( COMPLEX2Field ( Field2COMPLEX (aa * ( COMPLEX2Field M)))) by MATRIX_5:def 7

 .= (aa * ( COMPLEX2Field M)) by MATRIX_5: 6;

 ((a * M) * (i,j)) = (m * (i,j)) by MATRIX_5:def 1

 .= ((aa * ( COMPLEX2Field M)) * (i,j)) by A3, COMPLFLD:def 1

 .= (aa * (( COMPLEX2Field M) * (i,j))) by A2, MATRIX_3:def 5

 .= (a * (( COMPLEX2Field M) * (i,j)));

 hence thesis by A1;

 end;

 theorem :: MATRIXC1:5



 Th4: for a be Complex, M be Matrix of COMPLEX holds ((a * M) *' ) = ((a *' ) * (M *' ))

 proof

 let a be Complex, M be Matrix of COMPLEX ;

 reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;



 A1: ( len (a * M)) = ( len M) by Th2;



 A2: ( width (a * M)) = ( width M) by Th2;



 A3: ( width M) = ( width (M *' )) by Def1;



 A4: ( len ((a * M) *' )) = ( len (a * M)) by Def1;



 A5: ( width ((a * M) *' )) = ( width (a * M)) by Def1;



 A6: ( len M) = ( len (M *' )) by Def1;

 A7:

 now

 let i, j;

 assume

 A8: [i, j] in ( Indices ((a * M) *' ));

 then

 A9: 1 <= i by Th1;



 A10: 1 <= j by A8, Th1;



 A11: j <= ( width (a * M)) by A5, A8, Th1;



 A12: i <= ( len (a * M)) by A4, A8, Th1;

 then

 A13: [i, j] in ( Indices M) by A1, A2, A9, A10, A11, Th1;



 A14: [i, j] in ( Indices (M *' )) by A1, A6, A2, A3, A9, A12, A10, A11, Th1;

 [i, j] in ( Indices (a * M)) by A9, A12, A10, A11, Th1;

 then (((a * M) *' ) * (i,j)) = (((a * M) * (i,j)) *' ) by Def1;



 hence (((a * M) *' ) * (i,j)) = ((aa * (M * (i,j))) *' ) by A13, Th3

 .= ((aa *' ) * ((M * (i,j)) *' )) by COMPLEX1: 35

 .= ((a *' ) * ((M *' ) * (i,j))) by A13, Def1

 .= (((a *' ) * (M *' )) * (i,j)) by A14, Th3;

 end;

 ( len ((a *' ) * (M *' ))) = ( len (M *' )) by Th2;

 then ( len ((a *' ) * (M *' ))) = ( len M) by Def1;

 then

 A15: ( len ((a * M) *' )) = ( len ((a *' ) * (M *' ))) by A4, Th2;

 ( width ((a *' ) * (M *' ))) = ( width (M *' )) by Th2;

 then ( width ((a *' ) * (M *' ))) = ( width M) by Def1;

 hence thesis by A15, A5, A7, Th2, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:6



 Th5: for M1,M2 be Matrix of COMPLEX holds ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M1)

 proof

 let M1,M2 be Matrix of COMPLEX ;



 A1: ( width (M1 + M2)) = ( width ( COMPLEX2Field (M1 + M2))) by MATRIX_5: 7

 .= ( width ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) + ( COMPLEX2Field M2))))) by MATRIX_5:def 3

 .= ( width (( COMPLEX2Field M1) + ( COMPLEX2Field M2))) by MATRIX_5: 6

 .= ( width ( COMPLEX2Field M1)) by MATRIX_3:def 3

 .= ( width M1) by MATRIX_5:def 1;

 ( len (M1 + M2)) = ( len ( COMPLEX2Field (M1 + M2))) by MATRIX_5: 7

 .= ( len ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) + ( COMPLEX2Field M2))))) by MATRIX_5:def 3

 .= ( len (( COMPLEX2Field M1) + ( COMPLEX2Field M2))) by MATRIX_5: 6

 .= ( len ( COMPLEX2Field M1)) by MATRIX_3:def 3

 .= ( len M1) by MATRIX_5:def 1;

 hence thesis by A1;

 end;

 theorem :: MATRIXC1:7



 Th6: for i,j be Nat, M1,M2 be Matrix of COMPLEX st [i, j] in ( Indices M1) holds ((M1 + M2) * (i,j)) = ((M1 * (i,j)) + (M2 * (i,j)))

 proof

 let i,j be Nat, M1,M2 be Matrix of COMPLEX ;



 A1: ( COMPLEX2Field (M1 + M2)) = ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) + ( COMPLEX2Field M2)))) by MATRIX_5:def 3

 .= (( COMPLEX2Field M1) + ( COMPLEX2Field M2)) by MATRIX_5: 6;

 reconsider m1 = ( COMPLEX2Field M1), m2 = ( COMPLEX2Field M2) as Matrix of COMPLEX by COMPLFLD:def 1;

 set m = ( COMPLEX2Field (M1 + M2));

 reconsider m9 = m as Matrix of COMPLEX by COMPLFLD:def 1;



 A2: (M1 * (i,j)) = (m1 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M1) * (i,j)) by COMPLFLD:def 1;

 assume [i, j] in ( Indices M1);

 then

 A3: [i, j] in ( Indices ( COMPLEX2Field M1)) by MATRIX_5:def 1;



 A4: (M2 * (i,j)) = (m2 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M2) * (i,j)) by COMPLFLD:def 1;

 ((M1 + M2) * (i,j)) = (m9 * (i,j)) by MATRIX_5:def 1

 .= (m * (i,j)) by COMPLFLD:def 1

 .= ((( COMPLEX2Field M1) * (i,j)) + (( COMPLEX2Field M2) * (i,j))) by A1, A3, MATRIX_3:def 3;

 hence thesis by A2, A4;

 end;

 theorem :: MATRIXC1:8

 for M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds ((M1 + M2) *' ) = ((M1 *' ) + (M2 *' ))

 proof

 let M1,M2 be Matrix of COMPLEX ;

 assume that

 A1: ( len M1) = ( len M2) and

 A2: ( width M1) = ( width M2);



 A3: ( len (M1 + M2)) = ( len M1) by Th5;



 A4: ( width ((M1 + M2) *' )) = ( width (M1 + M2)) by Def1;



 A5: ( width (M1 + M2)) = ( width M1) by Th5;



 A6: ( len ((M1 + M2) *' )) = ( len (M1 + M2)) by Def1;

 A7:

 now

 let i, j;

 assume

 A8: [i, j] in ( Indices ((M1 + M2) *' ));

 then

 A9: 1 <= j by Th1;



 A10: 1 <= i by A8, Th1;



 A11: j <= ( width (M1 + M2)) by A4, A8, Th1;

 then

 A12: j <= ( width (M1 *' )) by A5, Def1;



 A13: i <= ( len (M1 + M2)) by A6, A8, Th1;

 then i <= ( len (M1 *' )) by A3, Def1;

 then

 A14: [i, j] in ( Indices (M1 *' )) by A9, A10, A12, Th1;



 A15: 1 <= i by A8, Th1;

 then

 A16: [i, j] in ( Indices M1) by A3, A5, A13, A9, A11, Th1;



 A17: [i, j] in ( Indices M2) by A1, A2, A3, A5, A15, A13, A9, A11, Th1;

 [i, j] in ( Indices (M1 + M2)) by A15, A13, A9, A11, Th1;

 then (((M1 + M2) *' ) * (i,j)) = (((M1 + M2) * (i,j)) *' ) by Def1;



 hence (((M1 + M2) *' ) * (i,j)) = (((M1 * (i,j)) + (M2 * (i,j))) *' ) by A16, Th6

 .= (((M1 * (i,j)) *' ) + ((M2 * (i,j)) *' )) by COMPLEX1: 32

 .= (((M1 *' ) * (i,j)) + ((M2 * (i,j)) *' )) by A16, Def1

 .= (((M1 *' ) * (i,j)) + ((M2 *' ) * (i,j))) by A17, Def1

 .= (((M1 *' ) + (M2 *' )) * (i,j)) by A14, Th6;

 end;



 A18: ( width (M1 *' )) = ( width M1) by Def1;



 A19: ( width ((M1 *' ) + (M2 *' ))) = ( width (M1 *' )) by Th5;



 A20: ( len ((M1 *' ) + (M2 *' ))) = ( len (M1 *' )) by Th5;

 ( len (M1 *' )) = ( len M1) by Def1;

 hence thesis by A6, A3, A20, A4, A5, A19, A18, A7, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:9



 Th8: for M be Matrix of COMPLEX holds ( len ( - M)) = ( len M) & ( width ( - M)) = ( width M)

 proof

 let M be Matrix of COMPLEX ;



 A1: ( width ( - M)) = ( width ( COMPLEX2Field ( - M))) by MATRIX_5: 7

 .= ( width ( COMPLEX2Field ( Field2COMPLEX ( - ( COMPLEX2Field M))))) by MATRIX_5:def 4

 .= ( width ( - ( COMPLEX2Field M))) by MATRIX_5: 6

 .= ( width ( COMPLEX2Field M)) by MATRIX_3:def 2

 .= ( width M) by MATRIX_5:def 1;

 ( len ( - M)) = ( len ( COMPLEX2Field ( - M))) by MATRIX_5: 7

 .= ( len ( COMPLEX2Field ( Field2COMPLEX ( - ( COMPLEX2Field M))))) by MATRIX_5:def 4

 .= ( len ( - ( COMPLEX2Field M))) by MATRIX_5: 6

 .= ( len ( COMPLEX2Field M)) by MATRIX_3:def 2

 .= ( len M) by MATRIX_5:def 1;

 hence thesis by A1;

 end;

 theorem :: MATRIXC1:10



 Th9: for i,j be Nat, M be Matrix of COMPLEX st [i, j] in ( Indices M) holds (( - M) * (i,j)) = ( - (M * (i,j)))

 proof

 let i,j be Nat, M be Matrix of COMPLEX ;



 A1: ( COMPLEX2Field ( - M)) = ( COMPLEX2Field ( Field2COMPLEX ( - ( COMPLEX2Field M)))) by MATRIX_5:def 4

 .= ( - ( COMPLEX2Field M)) by MATRIX_5: 6;

 reconsider m = ( COMPLEX2Field ( - M)) as Matrix of COMPLEX by COMPLFLD:def 1;

 reconsider m1 = ( COMPLEX2Field M) as Matrix of COMPLEX by COMPLFLD:def 1;



 A2: (M * (i,j)) = (m1 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M) * (i,j)) by COMPLFLD:def 1;

 assume [i, j] in ( Indices M);

 then

 A3: [i, j] in ( Indices ( COMPLEX2Field M)) by MATRIX_5:def 1;

 (( - M) * (i,j)) = (m * (i,j)) by MATRIX_5:def 1

 .= (( - ( COMPLEX2Field M)) * (i,j)) by A1, COMPLFLD:def 1

 .= ( - (( COMPLEX2Field M) * (i,j))) by A3, MATRIX_3:def 2;

 hence thesis by A2, COMPLFLD: 2;

 end;

 theorem :: MATRIXC1:11



 Th10: for M be Matrix of COMPLEX holds (( - 1) * M) = ( - M)

 proof

 let M be Matrix of COMPLEX ;



 A1: ( width ( - M)) = ( width M) by Th8;



 A2: ( width (( - 1) * M)) = ( width M) by Th2;



 A3: ( len (( - 1) * M)) = ( len M) by Th2;

 A4:

 now

 let i, j;

 assume

 A5: [i, j] in ( Indices (( - 1) * M));

 then

 A6: 1 <= i by Th1;



 A7: 1 <= j by A5, Th1;



 A8: j <= ( width M) by A2, A5, Th1;

 i <= ( len M) by A3, A5, Th1;

 then

 A9: [i, j] in ( Indices M) by A6, A7, A8, Th1;



 hence ((( - 1) * M) * (i,j)) = (( - 1) * (M * (i,j))) by Th3

 .= ( - (M * (i,j)))

 .= (( - M) * (i,j)) by A9, Th9;

 end;

 ( len ( - M)) = ( len M) by Th8;

 hence thesis by A3, A1, A2, A4, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:12

 for M be Matrix of COMPLEX holds (( - M) *' ) = ( - (M *' ))

 proof

 let M be Matrix of COMPLEX ;

 (( - M) *' ) = ((( - 1) * M) *' ) by Th10

 .= ((( - 1r ) *' ) * (M *' )) by Th4, COMPLEX1:def 4

 .= (( - 1) * (M *' )) by COMPLEX1: 30, COMPLEX1: 33, COMPLEX1:def 4

 .= ( - (M *' )) by Th10;

 hence thesis;

 end;

 theorem :: MATRIXC1:13



 Th12: for M1,M2 be Matrix of COMPLEX holds ( len (M1 - M2)) = ( len M1) & ( width (M1 - M2)) = ( width M1)

 proof

 let M1,M2 be Matrix of COMPLEX ;



 A1: ( width (M1 - M2)) = ( width ( COMPLEX2Field (M1 - M2))) by MATRIX_5: 7

 .= ( width ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) - ( COMPLEX2Field M2))))) by MATRIX_5:def 5

 .= ( width (( COMPLEX2Field M1) - ( COMPLEX2Field M2))) by MATRIX_5: 6

 .= ( width (( COMPLEX2Field M1) + ( - ( COMPLEX2Field M2)))) by MATRIX_4:def 1

 .= ( width ( COMPLEX2Field M1)) by MATRIX_3:def 3

 .= ( width M1) by MATRIX_5:def 1;

 ( len (M1 - M2)) = ( len ( COMPLEX2Field (M1 - M2))) by MATRIX_5: 7

 .= ( len ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) - ( COMPLEX2Field M2))))) by MATRIX_5:def 5

 .= ( len (( COMPLEX2Field M1) - ( COMPLEX2Field M2))) by MATRIX_5: 6

 .= ( len (( COMPLEX2Field M1) + ( - ( COMPLEX2Field M2)))) by MATRIX_4:def 1

 .= ( len ( COMPLEX2Field M1)) by MATRIX_3:def 3

 .= ( len M1) by MATRIX_5:def 1;

 hence thesis by A1;

 end;

 theorem :: MATRIXC1:14



 Th13: for i,j be Nat, M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) & [i, j] in ( Indices M1) holds ((M1 - M2) * (i,j)) = ((M1 * (i,j)) - (M2 * (i,j)))

 proof

 let i,j be Nat, M1,M2 be Matrix of COMPLEX ;

 assume that

 A1: ( len M1) = ( len M2) and

 A2: ( width M1) = ( width M2) and

 A3: [i, j] in ( Indices M1);



 A4: j <= ( width M2) by A2, A3, Th1;



 A5: 1 <= j by A3, Th1;



 A6: 1 <= i by A3, Th1;

 i <= ( len M2) by A1, A3, Th1;

 then [i, j] in ( Indices M2) by A6, A5, A4, Th1;

 then

 A7: [i, j] in ( Indices ( COMPLEX2Field M2)) by MATRIX_5:def 1;

 reconsider m2 = ( COMPLEX2Field M2) as Matrix of COMPLEX by COMPLFLD:def 1;

 reconsider m1 = ( COMPLEX2Field M1) as Matrix of COMPLEX by COMPLFLD:def 1;

 set m = ( COMPLEX2Field (M1 - M2));



 A8: ( COMPLEX2Field (M1 - M2)) = ( COMPLEX2Field ( Field2COMPLEX (( COMPLEX2Field M1) - ( COMPLEX2Field M2)))) by MATRIX_5:def 5

 .= (( COMPLEX2Field M1) - ( COMPLEX2Field M2)) by MATRIX_5: 6;

 reconsider m9 = m as Matrix of COMPLEX by COMPLFLD:def 1;



 A9: (M1 * (i,j)) = (m1 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M1) * (i,j)) by COMPLFLD:def 1;



 A10: [i, j] in ( Indices ( COMPLEX2Field M1)) by A3, MATRIX_5:def 1;

 (M2 * (i,j)) = (m2 * (i,j)) by MATRIX_5:def 1

 .= (( COMPLEX2Field M2) * (i,j)) by COMPLFLD:def 1;

 then

 A11: ( - (M2 * (i,j))) = ( - (( COMPLEX2Field M2) * (i,j))) by COMPLFLD: 2;

 ((M1 - M2) * (i,j)) = (m9 * (i,j)) by MATRIX_5:def 1

 .= (m * (i,j)) by COMPLFLD:def 1

 .= ((( COMPLEX2Field M1) + ( - ( COMPLEX2Field M2))) * (i,j)) by A8, MATRIX_4:def 1

 .= ((( COMPLEX2Field M1) * (i,j)) + (( - ( COMPLEX2Field M2)) * (i,j))) by A10, MATRIX_3:def 3

 .= ((( COMPLEX2Field M1) * (i,j)) + ( - (( COMPLEX2Field M2) * (i,j)))) by A7, MATRIX_3:def 2;

 hence thesis by A9, A11;

 end;

 theorem :: MATRIXC1:15

 for M1,M2 be Matrix of COMPLEX st ( len M1) = ( len M2) & ( width M1) = ( width M2) holds ((M1 - M2) *' ) = ((M1 *' ) - (M2 *' ))

 proof

 let M1,M2 be Matrix of COMPLEX ;

 assume that

 A1: ( len M1) = ( len M2) and

 A2: ( width M1) = ( width M2);



 A3: ( len ((M1 - M2) *' )) = ( len (M1 - M2)) by Def1;



 A4: ( width ((M1 - M2) *' )) = ( width (M1 - M2)) by Def1;



 A5: ( width (M1 - M2)) = ( width M1) by Th12;



 A6: ( width (M1 *' )) = ( width M1) by Def1;



 A7: ( len (M1 *' )) = ( len M1) by Def1;



 A8: ( width (M2 *' )) = ( width M2) by Def1;



 A9: ( len (M1 - M2)) = ( len M1) by Th12;



 A10: ( len (M2 *' )) = ( len M2) by Def1;

 A11:

 now

 let i, j;

 assume

 A12: [i, j] in ( Indices ((M1 - M2) *' ));

 then

 A13: 1 <= j by Th1;



 A14: 1 <= i by A12, Th1;



 A15: j <= ( width (M1 - M2)) by A4, A12, Th1;

 then

 A16: j <= ( width (M1 *' )) by A5, Def1;



 A17: i <= ( len (M1 - M2)) by A3, A12, Th1;

 then i <= ( len (M1 *' )) by A9, Def1;

 then

 A18: [i, j] in ( Indices (M1 *' )) by A13, A14, A16, Th1;



 A19: 1 <= i by A12, Th1;

 then

 A20: [i, j] in ( Indices M1) by A9, A5, A17, A13, A15, Th1;



 A21: [i, j] in ( Indices M2) by A1, A2, A9, A5, A19, A17, A13, A15, Th1;

 [i, j] in ( Indices (M1 - M2)) by A19, A17, A13, A15, Th1;

 then (((M1 - M2) *' ) * (i,j)) = (((M1 - M2) * (i,j)) *' ) by Def1;



 hence (((M1 - M2) *' ) * (i,j)) = (((M1 * (i,j)) - (M2 * (i,j))) *' ) by A1, A2, A20, Th13

 .= (((M1 * (i,j)) *' ) - ((M2 * (i,j)) *' )) by COMPLEX1: 34

 .= (((M1 *' ) * (i,j)) - ((M2 * (i,j)) *' )) by A20, Def1

 .= (((M1 *' ) * (i,j)) - ((M2 *' ) * (i,j))) by A21, Def1

 .= (((M1 *' ) - (M2 *' )) * (i,j)) by A1, A2, A7, A10, A6, A8, A18, Th13;

 end;



 A22: ( width (M1 *' )) = ( width M1) by Def1;



 A23: ( width ((M1 *' ) - (M2 *' ))) = ( width (M1 *' )) by Th12;

 ( len ((M1 *' ) - (M2 *' ))) = ( len (M1 *' )) by Th12;

 hence thesis by A3, A7, A9, A4, A5, A23, A22, A11, MATRIX_0: 21;

 end;

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def2

 func M @" -> Matrix of COMPLEX equals ((M @ ) *' );

 coherence ;

 end

 definition

 let x be FinSequence of COMPLEX ;

 assume

 A1: ( len x) > 0 ;

 :: MATRIXC1:def3

 func FinSeq2Matrix x -> Matrix of COMPLEX means ( len it ) = ( len x) & ( width it ) = 1 & for j st j in ( Seg ( len x)) holds (it . j) = <*(x . j)*>;

 existence

 proof

 reconsider n = ( len x) as Element of NAT ;

 deffunc F( Nat) = <*(x . $1)*>;

 consider M3 be FinSequence such that

 A2: ( len M3) = n & for j be Nat st j in ( dom M3) holds (M3 . j) = F(j) from FINSEQ_1:sch 2;

 for y be object st y in ( rng M3) holds ex p be FinSequence of COMPLEX st y = p & ( len p) = 1

 proof

 let y be object;

 assume y in ( rng M3);

 then

 consider z be object such that

 A3: z in ( dom M3) and

 A4: y = (M3 . z) by FUNCT_1:def 3;

 reconsider z as Element of NAT by A3;

 ( len <*(x . z)*>) = 1 by FINSEQ_1: 39;

 hence thesis by A2, A3, A4;

 end;

 then

 reconsider M2 = M3 as Matrix of COMPLEX by MATRIX_0: 9;

 for p be FinSequence of COMPLEX st p in ( rng M2) holds ( len p) = 1

 proof

 let p be FinSequence of COMPLEX ;

 assume p in ( rng M2);

 then

 consider i be Nat such that

 A5: i in ( dom M2) and

 A6: (M2 . i) = p by FINSEQ_2: 10;

 ( len <*(x . i)*>) = 1 by FINSEQ_1: 39;

 hence thesis by A2, A5, A6;

 end;

 then

 reconsider M1 = M2 as Matrix of ( len M2), 1, COMPLEX by MATRIX_0:def 2;

 take M2;



 A7: ( dom M3) = ( Seg n) by A2, FINSEQ_1:def 3;

 ( width M1) = 1 by A1, A2, MATRIX_0: 23;

 hence thesis by A2, A7;

 end;

 uniqueness

 proof

 let M1,M2 be Matrix of COMPLEX ;

 assume that

 A8: ( len M1) = ( len x) and ( width M1) = 1 and

 A9: for k st k in ( Seg ( len x)) holds (M1 . k) = <*(x . k)*> and

 A10: ( len M2) = ( len x) and ( width M2) = 1 and

 A11: for k st k in ( Seg ( len x)) holds (M2 . k) = <*(x . k)*>;



 A12: ( dom M1) = ( Seg ( len x)) by A8, FINSEQ_1:def 3;

 now

 let k be Nat;

 assume

 A13: k in ( dom M1);



 hence (M1 . k) = <*(x . k)*> by A9, A12

 .= (M2 . k) by A11, A12, A13;

 end;

 hence thesis by A8, A10, FINSEQ_2: 9;

 end;

 end

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def4

 func Matrix2FinSeq M -> FinSequence of COMPLEX equals ( Col (M,1));

 coherence ;

 end

 definition

 let F1,F2 be FinSequence of COMPLEX ;

 :: MATRIXC1:def5

 func mlt (F1,F2) -> FinSequence of COMPLEX equals ( multcomplex .: (F1,F2));

 coherence ;

 commutativity

 proof

 let F,F1,F2 be FinSequence of COMPLEX ;



 A1: ( dom multcomplex ) = [: COMPLEX , COMPLEX :] by FUNCT_2:def 1;

 then

 A2: [:( rng F2), ( rng F1):] c= ( dom multcomplex ) by ZFMISC_1: 96;

 [:( rng F1), ( rng F2):] c= ( dom multcomplex ) by A1, ZFMISC_1: 96;



 then

 A3: ( dom ( multcomplex .: (F1,F2))) = (( dom F1) /\ ( dom F2)) by FUNCOP_1: 69

 .= ( dom ( multcomplex .: (F2,F1))) by A2, FUNCOP_1: 69;

 assume

 A4: F = ( multcomplex .: (F1,F2));

 for z be set st z in ( dom ( multcomplex .: (F2,F1))) holds (F . z) = ( multcomplex . ((F2 . z),(F1 . z)))

 proof

 let z be set such that

 A5: z in ( dom ( multcomplex .: (F2,F1)));

 set F1z = (F1 . z), F2z = (F2 . z);



 thus (F . z) = ( multcomplex . ((F1 . z),(F2 . z))) by A4, A3, A5, FUNCOP_1: 22

 .= (F1z * F2z) by BINOP_2:def 5

 .= ( multcomplex . ((F2 . z),(F1 . z))) by BINOP_2:def 5;

 end;

 hence thesis by A4, A3, FUNCOP_1: 21;

 end;

 end

 definition

 let M be Matrix of COMPLEX ;

 let F be FinSequence of COMPLEX ;

 :: MATRIXC1:def6

 func M * F -> FinSequence of COMPLEX means

 : Def6: ( len it ) = ( len M) & for i st i in ( Seg ( len M)) holds (it . i) = ( Sum ( mlt (( Line (M,i)),F)));

 existence

 proof

 deffunc V( Nat) = ( Sum ( mlt (( Line (M,$1)),F)));

 consider z be FinSequence of COMPLEX such that

 A1: ( len z) = ( len M) & for i be Nat st i in ( dom z) holds (z . i) = V(i) from FINSEQ_2:sch 1;

 take z;

 ( dom z) = ( Seg ( len M)) by A1, FINSEQ_1:def 3;

 hence thesis by A1;

 end;

 uniqueness

 proof

 let p1,p2 be FinSequence of COMPLEX ;

 assume that

 A2: ( len p1) = ( len M) and

 A3: for i st i in ( Seg ( len M)) holds (p1 . i) = ( Sum ( mlt (( Line (M,i)),F))) and

 A4: ( len p2) = ( len M) and

 A5: for i st i in ( Seg ( len M)) holds (p2 . i) = ( Sum ( mlt (( Line (M,i)),F)));



 A6: ( dom p1) = ( Seg ( len M)) by A2, FINSEQ_1:def 3;

 now

 let i be Nat;

 assume

 A7: i in ( dom p1);

 then (p1 . i) = ( Sum ( mlt (( Line (M,i)),F))) by A3, A6;

 hence (p1 . i) = (p2 . i) by A5, A6, A7;

 end;

 hence thesis by A2, A4, FINSEQ_2: 9;

 end;

 end



 Lm1: for a be Element of COMPLEX , F be FinSequence of COMPLEX holds (a * F) = (( multcomplex [;] (a,( id COMPLEX ))) * F)

 proof

 let a be Element of COMPLEX , F be FinSequence of COMPLEX ;

 (a multcomplex ) = ( multcomplex [;] (a,( id COMPLEX ))) by SEQ_4:def 4;

 hence thesis by SEQ_4:def 9;

 end;

 theorem :: MATRIXC1:16



 Th15: (a * ( mlt (R1,R2))) = ( mlt ((a * R1),R2))

 proof



 thus (a * ( mlt (R1,R2))) = (( multcomplex [;] (a,( id COMPLEX ))) * ( mlt (R1,R2))) by Lm1

 .= ( multcomplex .: ((( multcomplex [;] (a,( id COMPLEX ))) * R1),R2)) by FINSEQOP: 26

 .= ( mlt ((a * R1),R2)) by Lm1;

 end;

 definition

 let M be Matrix of COMPLEX ;

 let a be Complex;

 :: MATRIXC1:def7

 func M * a -> Matrix of COMPLEX equals (a * M);

 coherence ;

 end

 theorem :: MATRIXC1:17

 for a be Element of COMPLEX , M be Matrix of COMPLEX holds ((M * a) *' ) = ((a *' ) * (M *' )) by Th4;

 theorem :: MATRIXC1:18



 Th17: for F1,F2 be FinSequence of COMPLEX , i be Nat holds i in ( dom ( mlt (F1,F2))) implies (( mlt (F1,F2)) . i) = ((F1 . i) * (F2 . i))

 proof

 let F1,F2 be FinSequence of COMPLEX , i be Nat;

 set r1 = (F1 . i), r2 = (F2 . i);

 assume i in ( dom ( mlt (F1,F2)));

 then (( mlt (F1,F2)) . i) = ( multcomplex . (r1,r2)) by FUNCOP_1: 22;

 hence thesis by BINOP_2:def 5;

 end;

 definition

 let i be Element of NAT , R1,R2 be Element of (i -tuples_on COMPLEX );

 :: original: mlt

 redefine

 func mlt (R1,R2) -> Element of (i -tuples_on COMPLEX ) ;

 coherence by FINSEQ_2: 120;

 end

 theorem :: MATRIXC1:19



 Th18: (( mlt (R1,R2)) . j) = ((R1 . j) * (R2 . j))

 proof

 reconsider i, j1 = j as Element of NAT by ORDINAL1:def 12;

 reconsider R1, R2 as Element of (i -tuples_on COMPLEX );

 per cases ;

 suppose

 A1: not j in ( Seg i);

 then

 A2: not j in ( dom R2) by FINSEQ_2: 124;

 not j in ( dom ( mlt (R1,R2))) by A1, FINSEQ_2: 124;



 then (( mlt (R1,R2)) . j) = ((R1 . j1) * 0 ) by FUNCT_1:def 2

 .= ((R1 . j) * (R2 . j)) by A2, FUNCT_1:def 2;

 hence thesis;

 end;

 suppose j in ( Seg i);

 then j in ( dom ( mlt (R1,R2))) by FINSEQ_2: 124;

 hence thesis by Th17;

 end;

 end;

 ::$Canceled

 theorem :: MATRIXC1:21



 Th19: for F be FinSequence of COMPLEX holds ex G be sequence of COMPLEX st for n be Nat st 1 <= n & n <= ( len F) holds (G . n) = (F . n)

 proof

 let F be FinSequence of COMPLEX ;

 defpred P[ object, object] means ($1 in ( Seg ( len F)) implies $2 = (F . $1)) & ( not $1 in ( Seg ( len F)) implies $2 = 0 );



 A1: for x be object st x in NAT holds ex y be object st y in COMPLEX & P[x, y]

 proof

 let x be object;

 assume x in NAT ;

 per cases ;

 suppose

 A2: x in ( Seg ( len F));

 take (F . x);

 (F . x) in COMPLEX by XCMPLX_0:def 2;

 hence thesis by A2;

 end;

 suppose

 A3: not x in ( Seg ( len F));

 take 0 ;

 0 in COMPLEX by XCMPLX_0:def 2;

 hence thesis by A3;

 end;

 end;

 ex G1 be sequence of COMPLEX st for x be object st x in NAT holds P[x, (G1 . x)] from FUNCT_2:sch 1( A1);

 then

 consider G2 be sequence of COMPLEX such that

 A4: for x be object st x in NAT holds (x in ( Seg ( len F)) implies (G2 . x) = (F . x)) & ( not x in ( Seg ( len F)) implies (G2 . x) = 0 );

 for n be Nat st 1 <= n & n <= ( len F) holds (G2 . n) = (F . n)

 proof

 let n be Nat;

 assume that

 A5: 1 <= n and

 A6: n <= ( len F);

 n in ( Seg ( len F)) by A5, A6, FINSEQ_1: 1;

 hence thesis by A4;

 end;

 hence thesis;

 end;

 theorem :: MATRIXC1:22



 Th20: for F be FinSequence of COMPLEX st ( len (F *' )) >= 1 holds ( addcomplex $$ (F *' )) = (( addcomplex $$ F) *' )

 proof

 let F be FinSequence of COMPLEX ;



 A1: ( len F) = ( len (F *' )) by COMPLSP2:def 1;

 assume

 A2: ( len (F *' )) >= 1;

 then

 consider f22 be sequence of COMPLEX such that

 A3: (f22 . 1) = ((F *' ) . 1) and

 A4: for n be Nat st 0 <> n & n < ( len (F *' )) holds (f22 . (n + 1)) = ( addcomplex . ((f22 . n),((F *' ) . (n + 1)))) and

 A5: ( addcomplex $$ (F *' )) = (f22 . ( len (F *' ))) by FINSOP_1: 1;



 A6: ( len (F *' )) in ( Seg ( len (F *' ))) by A2, FINSEQ_1: 1;

 defpred P[ set, set] means $2 = (f22 . $1);



 A7: for k be Nat st k in ( Seg ( len (F *' ))) holds ex x be Element of COMPLEX st P[k, x];

 ex f2 be FinSequence of COMPLEX st ( dom f2) = ( Seg ( len (F *' ))) & for k be Nat st k in ( Seg ( len (F *' ))) holds P[k, (f2 . k)] from FINSEQ_1:sch 5( A7);

 then

 consider f2 be FinSequence of COMPLEX such that

 A8: ( dom f2) = ( Seg ( len (F *' ))) and

 A9: for k be Nat st k in ( Seg ( len (F *' ))) holds P[k, (f2 . k)];

 consider f9 be sequence of COMPLEX such that

 A10: for n be Nat st 1 <= n & n <= ( len (f2 *' )) holds (f9 . n) = ((f2 *' ) . n) by Th19;



 A11: ( len (f2 *' )) = ( len f2) by COMPLSP2:def 1;

 then 1 <= ( len (f2 *' )) by A2, A8, FINSEQ_1:def 3;

 then

 A12: (f9 . 1) = ((f2 *' ) . 1) by A10;



 A13: ( len f2) = ( len (F *' )) by A8, FINSEQ_1:def 3;



 A14: for n st 0 <> n & n < ( len (F *' )) holds (f2 . (n + 1)) = ( addcomplex . ((f2 . n),((F *' ) . (n + 1))))

 proof

 let n;

 assume that

 A15: 0 <> n and

 A16: n < ( len (F *' ));



 A17: (n + 1) <= ( len (F *' )) by A16, NAT_1: 13;



 A18: ( 0 + 1) <= n by A15, NAT_1: 13;

 then

 A19: n in ( Seg ( len (F *' ))) by A16, FINSEQ_1: 1;

 1 <= (n + 1) by A18, NAT_1: 13;

 then (n + 1) in ( Seg ( len (F *' ))) by A17, FINSEQ_1: 1;



 then (f2 . (n + 1)) = (f22 . (n + 1)) by A9

 .= ( addcomplex . ((f22 . n),((F *' ) . (n + 1)))) by A4, A15, A16

 .= ( addcomplex . ((f2 . n),((F *' ) . (n + 1)))) by A9, A19;

 hence thesis;

 end;



 A20: for n be Nat st 0 <> n & n < ( len F) holds ((f2 *' ) . (n + 1)) = ( addcomplex . (((f2 *' ) . n),(F . (n + 1))))

 proof

 let n be Nat;

 assume that

 A21: 0 <> n and

 A22: n < ( len F);



 A23: n <= ( len f2) by A1, A8, A22, FINSEQ_1:def 3;



 A24: ( 0 + 1) <= n by A21, NAT_1: 13;

 then

 A25: 1 <= (n + 1) by NAT_1: 13;

 reconsider c = ((F . (n + 1)) *' ) as Element of COMPLEX by XCMPLX_0:def 2;



 A26: (n + 1) <= ( len F) by A22, NAT_1: 13;

 then (n + 1) <= ( len f2) by A1, A8, FINSEQ_1:def 3;



 then ((f2 *' ) . (n + 1)) = ((f2 . (n + 1)) *' ) by A25, COMPLSP2:def 1

 .= (( addcomplex . ((f2 . n),((F *' ) . (n + 1)))) *' ) by A1, A14, A21, A22

 .= (( addcomplex . ((f2 . n),c)) *' ) by A25, A26, COMPLSP2:def 1

 .= (((f2 . n) + c) *' ) by BINOP_2:def 3

 .= (((f2 . n) *' ) + (c *' )) by COMPLEX1: 32

 .= ( addcomplex . (((f2 . n) *' ),(F . (n + 1)))) by BINOP_2:def 3;

 hence thesis by A24, A23, COMPLSP2:def 1;

 end;



 A27: for n be Nat st 0 <> n & n < ( len F) holds (f9 . (n + 1)) = ( addcomplex . ((f9 . n),(F . (n + 1))))

 proof

 let n be Nat;

 assume that

 A28: 0 <> n and

 A29: n < ( len F);



 A30: ( 0 + 1) <= n by A28, NAT_1: 13;

 (n + 1) <= ( len (f2 *' )) by A1, A13, A11, A29, NAT_1: 13;

 then

 A31: (f9 . (n + 1)) = ((f2 *' ) . (n + 1)) by A10, NAT_1: 11;

 n <= ( len (f2 *' )) by A1, A13, A29, COMPLSP2:def 1;

 then (f9 . n) = ((f2 *' ) . n) by A10, A30;

 hence thesis by A20, A28, A29, A31;

 end;



 A32: 1 in ( Seg ( len (F *' ))) by A2, FINSEQ_1: 1;

 set d = (( addcomplex $$ (F *' )) *' );



 A33: ( len F) >= 1 by A2, COMPLSP2:def 1;

 ((f2 *' ) . ( len F)) = ((f2 *' ) . ( len (F *' ))) by COMPLSP2:def 1

 .= ((f2 . ( len (F *' ))) *' ) by A2, A13, COMPLSP2:def 1

 .= d by A5, A9, A6;

 then

 A34: d = (f9 . ( len F)) by A2, A1, A13, A10, A11;

 (F . 1) = (((F . 1) *' ) *' )

 .= (((F *' ) . 1) *' ) by A33, COMPLSP2:def 1

 .= ((f2 . 1) *' ) by A3, A9, A32

 .= ((f2 *' ) . 1) by A2, A13, COMPLSP2:def 1;

 then d = ( addcomplex $$ F) by A33, A12, A27, A34, FINSOP_1: 2;

 hence thesis;

 end;

 theorem :: MATRIXC1:23



 Th21: for F be FinSequence of COMPLEX st ( len F) >= 1 holds ( Sum (F *' )) = (( Sum F) *' )

 proof

 let F be FinSequence of COMPLEX ;

 assume ( len F) >= 1;

 then ( len (F *' )) >= 1 by COMPLSP2:def 1;

 hence thesis by Th20;

 end;

 theorem :: MATRIXC1:24



 Th22: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds (( mlt (x,(y *' ))) *' ) = ( mlt (y,(x *' )))

 proof

 let x,y be FinSequence of COMPLEX ;

 assume

 A1: ( len x) = ( len y);

 reconsider x19 = (x *' ) as Element of (( len (x *' )) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider y19 = y as Element of (( len y) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider y9 = (y *' ) as Element of (( len (y *' )) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider x9 = x as Element of (( len x) -tuples_on COMPLEX ) by FINSEQ_2: 92;



 A2: ( len (x *' )) = ( len x) by COMPLSP2:def 1;



 A3: ( len (y *' )) = ( len y) by COMPLSP2:def 1;

 then

 A4: ( len ( mlt (x,(y *' )))) = ( len x) by A1, FINSEQ_2: 72;



 A5: ( len ( mlt (x,(y *' )))) = ( len (y *' )) by A1, A3, FINSEQ_2: 72;

 A6:

 now

 let i be Nat;

 assume that

 A7: 1 <= i and

 A8: i <= ( len (( mlt (x,(y *' ))) *' ));



 A9: i <= ( len ( mlt (x,(y *' )))) by A8, COMPLSP2:def 1;



 hence ((( mlt (x,(y *' ))) *' ) . i) = ((( mlt (x,(y *' ))) . i) *' ) by A7, COMPLSP2:def 1

 .= (((x9 . i) * (y9 . i)) *' ) by A1, A3, Th18

 .= (((x . i) *' ) * (((y *' ) . i) *' )) by COMPLEX1: 35

 .= (((x . i) *' ) * (((y *' ) *' ) . i)) by A5, A7, A9, COMPLSP2:def 1

 .= (((x . i) *' ) * (y . i))

 .= (((x *' ) . i) * (y . i)) by A4, A7, A9, COMPLSP2:def 1

 .= (( mlt (x19,y19)) . i) by A1, A2, Th18

 .= (( mlt (y,(x *' ))) . i);

 end;

 ( len ( mlt (x,(y *' )))) = ( len (( mlt (x,(y *' ))) *' )) by COMPLSP2:def 1;

 then ( len (( mlt (x,(y *' ))) *' )) = ( len ( mlt (y,(x *' )))) by A1, A2, A4, FINSEQ_2: 72;

 hence thesis by A6, FINSEQ_1: 14;

 end;

 theorem :: MATRIXC1:25



 Th23: for x,y be FinSequence of COMPLEX , a be Element of COMPLEX st ( len x) = ( len y) holds ( mlt (x,(a * y))) = (a * ( mlt (x,y)))

 proof

 let x,y be FinSequence of COMPLEX , a be Element of COMPLEX ;

 reconsider x9 = x as Element of (( len x) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider y9 = y as Element of (( len y) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 assume ( len x) = ( len y);



 then ( mlt (x,(a * y))) = (a * ( mlt (x9,y9))) by Th15

 .= (a * ( mlt (x,y)));

 hence thesis;

 end;

 theorem :: MATRIXC1:26



 Th24: for x,y be FinSequence of COMPLEX , a be Element of COMPLEX st ( len x) = ( len y) holds ( mlt ((a * x),y)) = (a * ( mlt (x,y)))

 proof

 let x,y be FinSequence of COMPLEX , a be Element of COMPLEX ;

 reconsider x9 = x as Element of (( len x) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider y9 = y as Element of (( len y) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 assume ( len x) = ( len y);



 then ( mlt ((a * x),y)) = (a * ( mlt (x9,y9))) by Th15

 .= (a * ( mlt (x,y)));

 hence thesis;

 end;

 theorem :: MATRIXC1:27



 Th25: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds (( mlt (x,y)) *' ) = ( mlt ((x *' ),(y *' )))

 proof

 let x,y be FinSequence of COMPLEX ;



 A1: ( len (( mlt (x,y)) *' )) = ( len ( mlt (x,y))) by COMPLSP2:def 1;



 A2: ( len (x *' )) = ( len x) by COMPLSP2:def 1;

 assume

 A3: ( len x) = ( len y);



 A4: for i be Nat st 1 <= i & i <= ( len (( mlt (x,y)) *' )) holds ((( mlt (x,y)) *' ) . i) = (( mlt ((x *' ),(y *' ))) . i)

 proof

 let i be Nat;

 ((( mlt (x,y)) *' ) . i) = ((( mlt (y,((x *' ) *' ))) *' ) . i)

 .= (( mlt ((x *' ),(y *' ))) . i) by A3, A2, Th22;

 hence thesis;

 end;

 ( len (y *' )) = ( len y) by COMPLSP2:def 1;

 then ( len ( mlt ((x *' ),(y *' )))) = ( len (x *' )) by A3, A2, FINSEQ_2: 72;

 then ( len (( mlt (x,y)) *' )) = ( len ( mlt ((x *' ),(y *' )))) by A3, A1, A2, FINSEQ_2: 72;

 hence thesis by A4, FINSEQ_1: 14;

 end;



 Lm2: for a,b be Element of COMPLEX holds (( multcomplex [;] (a,( id COMPLEX ))) . b) = (a * b)

 proof

 let a,b be Element of COMPLEX ;



 thus (( multcomplex [;] (a,( id COMPLEX ))) . b) = ( multcomplex . (a,(( id COMPLEX ) . b))) by FUNCOP_1: 53

 .= ( multcomplex . (a,b))

 .= (a * b) by BINOP_2:def 5;

 end;

 theorem :: MATRIXC1:28



 Th26: for F be FinSequence of COMPLEX , a be Element of COMPLEX holds ( Sum (a * F)) = (a * ( Sum F))

 proof

 let F be FinSequence of COMPLEX , a be Element of COMPLEX ;

 set rM = ( multcomplex [;] (a,( id COMPLEX )));



 thus ( Sum (a * F)) = ( addcomplex $$ (rM * F)) by Lm1

 .= (rM . ( addcomplex $$ F)) by SEQ_4: 51, SEQ_4: 54, SETWOP_2: 30

 .= (a * ( Sum F)) by Lm2;

 end;

 definition

 let x be FinSequence of REAL ;

 :: MATRIXC1:def8

 func FR2FC (x) -> FinSequence of COMPLEX equals x;

 coherence

 proof

 ( rng x) c= COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

 hence thesis by FINSEQ_1:def 4;

 end;

 end

 theorem :: MATRIXC1:29

 for R be FinSequence of REAL , F be FinSequence of COMPLEX st R = F & ( len R) >= 1 holds ( addreal $$ R) = ( addcomplex $$ F)

 proof

 let R be FinSequence of REAL , F be FinSequence of COMPLEX ;

 assume that

 A1: R = F and

 A2: ( len R) >= 1;

 consider f22 be sequence of REAL such that

 A3: (f22 . 1) = (R . 1) and

 A4: for n be Nat st 0 <> n & n < ( len R) holds (f22 . (n + 1)) = ( addreal . ((f22 . n),(R . (n + 1)))) and

 A5: ( addreal $$ R) = (f22 . ( len R)) by A2, FINSOP_1: 1;

 defpred P[ set, set] means $2 = (f22 . $1);



 A6: for k be Nat st k in ( Seg ( len R)) holds ex x be Element of REAL st P[k, x]

 proof

 let k be Nat;

 (f22 . k) in REAL by XREAL_0:def 1;

 hence thesis;

 end;

 ex f2 be FinSequence of REAL st ( dom f2) = ( Seg ( len R)) & for k be Nat st k in ( Seg ( len R)) holds P[k, (f2 . k)] from FINSEQ_1:sch 5( A6);

 then

 consider f2 be FinSequence of REAL such that

 A7: ( dom f2) = ( Seg ( len R)) and

 A8: for k be Nat st k in ( Seg ( len R)) holds P[k, (f2 . k)];

 consider f9 be sequence of COMPLEX such that

 A9: for n be Nat st 1 <= n & n <= ( len ( FR2FC f2)) holds (f9 . n) = (( FR2FC f2) . n) by Th19;



 A10: ( len f2) = ( len R) by A7, FINSEQ_1:def 3;

 then

 A11: (( FR2FC f2) . ( len F)) = (f9 . ( len F)) by A1, A2, A9;



 A12: for n st 0 <> n & n < ( len R) holds (f2 . (n + 1)) = ( addreal . ((f2 . n),(R . (n + 1))))

 proof

 let n;

 assume that

 A13: 0 <> n and

 A14: n < ( len R);



 A15: (n + 1) <= ( len R) by A14, NAT_1: 13;



 A16: ( 0 + 1) <= n by A13, NAT_1: 13;

 then

 A17: n in ( Seg ( len R)) by A14, FINSEQ_1: 1;

 1 <= (n + 1) by A16, NAT_1: 13;

 then (n + 1) in ( Seg ( len R)) by A15, FINSEQ_1: 1;



 then (f2 . (n + 1)) = (f22 . (n + 1)) by A8

 .= ( addreal . ((f22 . n),(R . (n + 1)))) by A4, A13, A14

 .= ( addreal . ((f2 . n),(R . (n + 1)))) by A8, A17;

 hence thesis;

 end;



 A18: for n be Nat st 0 <> n & n < ( len F) holds (f9 . (n + 1)) = ( addcomplex . ((f9 . n),(F . (n + 1))))

 proof

 let n be Nat;

 assume that

 A19: 0 <> n and

 A20: n < ( len F);



 A21: ( 0 + 1) <= n by A19, NAT_1: 13;

 n <= ( len ( FR2FC f2)) by A1, A7, A20, FINSEQ_1:def 3;

 then (f9 . n) = (( FR2FC f2) . n) by A9, A21;

 then

 A22: ( addcomplex . ((f9 . n),(F . (n + 1)))) = ( addreal . ((f2 . n),(R . (n + 1)))) by A1, COMPLSP2: 44;

 (n + 1) <= ( len ( FR2FC f2)) by A1, A10, A20, NAT_1: 13;

 then (f9 . (n + 1)) = (( FR2FC f2) . (n + 1)) by A9, NAT_1: 11;

 hence thesis by A1, A12, A19, A20, A22;

 end;

 set d = ( addreal $$ R);



 A23: 1 in ( Seg ( len R)) by A2, FINSEQ_1: 1;



 A24: (f9 . 1) = (( FR2FC f2) . 1) by A2, A10, A9;

 ( len R) in ( Seg ( len R)) by A2, FINSEQ_1: 1;

 then (( FR2FC f2) . ( len F)) = d by A1, A5, A8;

 hence thesis by A1, A2, A3, A8, A23, A24, A18, A11, FINSOP_1: 2;

 end;

 theorem :: MATRIXC1:30

 for x be FinSequence of REAL , y be FinSequence of COMPLEX st x = y & ( len x) >= 1 holds ( Sum x) = ( Sum y);

 theorem :: MATRIXC1:31



 Th29: for F1,F2 be FinSequence of COMPLEX st ( len F1) = ( len F2) holds ( Sum (F1 - F2)) = (( Sum F1) - ( Sum F2))

 proof

 let F1,F2 be FinSequence of COMPLEX ;

 assume

 A1: ( len F1) = ( len F2);

 reconsider y2 = F2 as Element of (( len F2) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider x2 = F1 as Element of (( len F1) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 ( Sum (F1 - F2)) = ( addcomplex $$ ( diffcomplex .: (F1,F2))) by SEQ_4:def 7

 .= ( diffcomplex . (( addcomplex $$ x2),( addcomplex $$ y2))) by A1, SEQ_4: 51, SEQ_4: 52, SEQ_4:def 3, SETWOP_2: 37

 .= (( Sum F1) - ( Sum F2)) by BINOP_2:def 4;

 hence thesis;

 end;

 theorem :: MATRIXC1:32

 for x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt ((x - y),z)) = (( mlt (x,z)) - ( mlt (y,z)))

 proof

 let x,y,z be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: ( len y) = ( len z);

 reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on COMPLEX ) by A1, A2, FINSEQ_2: 92;



 A3: ( dom ( mlt ((x - y),z))) = ( Seg ( len ( mlt ((x2 - y2),z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) - ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) - ( mlt (y2,z2)))) by FINSEQ_1:def 3;



 A4: ( dom ( mlt (x,z))) = ( Seg ( len ( mlt (x2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) - ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) - ( mlt (y2,z2)))) by FINSEQ_1:def 3;



 A5: ( dom ( mlt (y,z))) = ( Seg ( len ( mlt (y2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) - ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) - ( mlt (y2,z2)))) by FINSEQ_1:def 3;

 for i be Nat st i in ( dom ( mlt ((x - y),z))) holds (( mlt ((x - y),z)) . i) = ((( mlt (x,z)) - ( mlt (y,z))) . i)

 proof

 let i be Nat;

 assume

 A6: i in ( dom ( mlt ((x - y),z)));

 set a = (x . i), b = (y . i), d = ((x - y) . i), e = (z . i);

 ( len (x2 - y2)) = ( len x) by CARD_1:def 7;



 then ( dom (x2 - y2)) = ( Seg ( len x)) by FINSEQ_1:def 3

 .= ( Seg ( len ( mlt (x2,z2)))) by CARD_1:def 7

 .= ( dom ( mlt (x,z))) by FINSEQ_1:def 3;

 then

 A7: d = (a - b) by A3, A4, A6, COMPLSP2: 2;



 thus (( mlt ((x - y),z)) . i) = (d * e) by A6, Th17

 .= ((a * e) - (b * e)) by A7

 .= ((( mlt (x,z)) . i) - (b * e)) by A3, A4, A6, Th17

 .= ((( mlt (x,z)) . i) - (( mlt (y,z)) . i)) by A3, A5, A6, Th17

 .= ((( mlt (x,z)) - ( mlt (y,z))) . i) by A3, A6, COMPLSP2: 2;

 end;

 hence thesis by A3, FINSEQ_1: 13;

 end;

 theorem :: MATRIXC1:33



 Th31: for x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt (x,(y - z))) = (( mlt (x,y)) - ( mlt (x,z)))

 proof

 let x,y,z be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: ( len y) = ( len z);

 reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on COMPLEX ) by A1, A2, FINSEQ_2: 92;



 A3: ( dom ( mlt (x,(y - z)))) = ( Seg ( len ( mlt (x2,(y2 - z2))))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) - ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) - ( mlt (x2,z2)))) by FINSEQ_1:def 3;



 A4: ( dom ( mlt (x,y))) = ( Seg ( len ( mlt (x2,y2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) - ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) - ( mlt (x2,z2)))) by FINSEQ_1:def 3;



 A5: ( dom ( mlt (x,z))) = ( Seg ( len ( mlt (x2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) - ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) - ( mlt (x2,z2)))) by FINSEQ_1:def 3;

 for i be Nat st i in ( dom ( mlt (x,(y - z)))) holds (( mlt (x,(y - z))) . i) = ((( mlt (x,y)) - ( mlt (x,z))) . i)

 proof

 let i be Nat;

 assume

 A6: i in ( dom ( mlt (x,(y - z))));

 set a = (y . i), b = (z . i), d = ((y - z) . i), e = (x . i);

 ( len (y2 - z2)) = ( len x) by CARD_1:def 7;



 then ( dom (y2 - z2)) = ( Seg ( len x)) by FINSEQ_1:def 3

 .= ( Seg ( len ( mlt (x2,y2)))) by CARD_1:def 7

 .= ( dom ( mlt (x,y))) by FINSEQ_1:def 3;

 then

 A7: d = (a - b) by A3, A4, A6, COMPLSP2: 2;



 thus (( mlt (x,(y - z))) . i) = (e * d) by A6, Th17

 .= ((e * a) - (e * b)) by A7

 .= ((( mlt (x,y)) . i) - (e * b)) by A3, A4, A6, Th17

 .= ((( mlt (x,y)) . i) - (( mlt (x,z)) . i)) by A3, A5, A6, Th17

 .= ((( mlt (x,y)) - ( mlt (x,z))) . i) by A3, A6, COMPLSP2: 2;

 end;

 hence thesis by A3, FINSEQ_1: 13;

 end;

 theorem :: MATRIXC1:34

 for x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt (x,(y + z))) = (( mlt (x,y)) + ( mlt (x,z)))

 proof

 let x,y,z be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: ( len y) = ( len z);

 reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on COMPLEX ) by A1, A2, FINSEQ_2: 92;



 A3: ( dom ( mlt (x,(y + z)))) = ( Seg ( len ( mlt (x2,(y2 + z2))))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) + ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) + ( mlt (x2,z2)))) by FINSEQ_1:def 3;



 A4: ( dom ( mlt (x,y))) = ( Seg ( len ( mlt (x2,y2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) + ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) + ( mlt (x2,z2)))) by FINSEQ_1:def 3;



 A5: ( dom ( mlt (x,z))) = ( Seg ( len ( mlt (x2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,y2)) + ( mlt (x2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,y2)) + ( mlt (x2,z2)))) by FINSEQ_1:def 3;

 for i be Nat st i in ( dom ( mlt (x,(y + z)))) holds (( mlt (x,(y + z))) . i) = ((( mlt (x,y)) + ( mlt (x,z))) . i)

 proof

 let i be Nat;

 assume

 A6: i in ( dom ( mlt (x,(y + z))));

 set a = (y . i), b = (z . i), d = ((y + z) . i), e = (x . i);

 ( len (y2 + z2)) = ( len x) by CARD_1:def 7;



 then ( dom (y2 + z2)) = ( Seg ( len x)) by FINSEQ_1:def 3

 .= ( Seg ( len ( mlt (x2,y2)))) by CARD_1:def 7

 .= ( dom ( mlt (x,y))) by FINSEQ_1:def 3;

 then

 A7: d = (a + b) by A3, A4, A6, COMPLSP2: 1;



 thus (( mlt (x,(y + z))) . i) = (e * d) by A6, Th17

 .= ((e * a) + (e * b)) by A7

 .= ((( mlt (x,y)) . i) + (e * b)) by A3, A4, A6, Th17

 .= ((( mlt (x,y)) . i) + (( mlt (x,z)) . i)) by A3, A5, A6, Th17

 .= ((( mlt (x,y)) + ( mlt (x,z))) . i) by A3, A6, COMPLSP2: 1;

 end;

 hence thesis by A3, FINSEQ_1: 13;

 end;

 theorem :: MATRIXC1:35



 Th33: for x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds ( mlt ((x + y),z)) = (( mlt (x,z)) + ( mlt (y,z)))

 proof

 let x,y,z be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: ( len y) = ( len z);

 reconsider x2 = x, y2 = y, z2 = z as Element of (( len x) -tuples_on COMPLEX ) by A1, A2, FINSEQ_2: 92;



 A3: ( dom ( mlt ((x + y),z))) = ( Seg ( len ( mlt ((x2 + y2),z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;



 A4: ( dom ( mlt (x,z))) = ( Seg ( len ( mlt (x2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;



 A5: ( dom ( mlt (y,z))) = ( Seg ( len ( mlt (y2,z2)))) by FINSEQ_1:def 3

 .= ( Seg ( len x)) by CARD_1:def 7

 .= ( Seg ( len (( mlt (x2,z2)) + ( mlt (y2,z2))))) by CARD_1:def 7

 .= ( dom (( mlt (x2,z2)) + ( mlt (y2,z2)))) by FINSEQ_1:def 3;

 for i be Nat st i in ( dom ( mlt ((x + y),z))) holds (( mlt ((x + y),z)) . i) = ((( mlt (x,z)) + ( mlt (y,z))) . i)

 proof

 let i be Nat;

 assume

 A6: i in ( dom ( mlt ((x + y),z)));

 set a = (x . i), b = (y . i), d = ((x + y) . i), e = (z . i);

 ( len (x2 + y2)) = ( len x) by CARD_1:def 7;



 then ( dom (x2 + y2)) = ( Seg ( len x)) by FINSEQ_1:def 3

 .= ( Seg ( len ( mlt (x2,z2)))) by CARD_1:def 7

 .= ( dom ( mlt (x,z))) by FINSEQ_1:def 3;

 then

 A7: d = (a + b) by A3, A4, A6, COMPLSP2: 1;



 thus (( mlt ((x + y),z)) . i) = (d * e) by A6, Th17

 .= ((a * e) + (b * e)) by A7

 .= ((( mlt (x,z)) . i) + (b * e)) by A3, A4, A6, Th17

 .= ((( mlt (x,z)) . i) + (( mlt (y,z)) . i)) by A3, A5, A6, Th17

 .= ((( mlt (x,z)) + ( mlt (y,z))) . i) by A3, A6, COMPLSP2: 1;

 end;

 hence thesis by A3, FINSEQ_1: 13;

 end;

 theorem :: MATRIXC1:36



 Th34: for F1,F2 be FinSequence of COMPLEX st ( len F1) = ( len F2) holds ( Sum (F1 + F2)) = (( Sum F1) + ( Sum F2))

 proof

 let F1,F2 be FinSequence of COMPLEX ;

 assume

 A1: ( len F1) = ( len F2);

 reconsider y2 = F2 as Element of (( len F2) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider x2 = F1 as Element of (( len F1) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 ( Sum (F1 + F2)) = ( addcomplex $$ ( addcomplex .: (F1,F2))) by SEQ_4:def 6

 .= ( addcomplex . (( addcomplex $$ x2),( addcomplex $$ y2))) by A1, SETWOP_2: 35

 .= (( Sum F1) + ( Sum F2)) by BINOP_2:def 3;

 hence thesis;

 end;

 theorem :: MATRIXC1:37



 Th35: for x1,y1 be FinSequence of COMPLEX holds for x2,y2 be FinSequence of REAL st x1 = x2 & y1 = y2 & ( len x1) = ( len y2) holds ( multcomplex .: (x1,y1)) = ( multreal .: (x2,y2))

 proof

 let x1,y1 be FinSequence of COMPLEX ;

 let x2,y2 be FinSequence of REAL ;

 assume that

 A1: x1 = x2 and

 A2: y1 = y2 and

 A3: ( len x1) = ( len y2);

 for i be Element of NAT st i in ( dom x1) holds ( multcomplex . ((x1 . i),(y1 . i))) = ( multreal . ((x2 . i),(y2 . i)))

 proof

 let i be Element of NAT ;

 ((x1 . i) * (y1 . i)) = ( multcomplex . ((x1 . i),(y1 . i))) by BINOP_2:def 5;

 hence thesis by A1, A2, BINOP_2:def 11;

 end;

 hence thesis by A1, A2, A3, COMPLSP2: 45;

 end;

 theorem :: MATRIXC1:38

 for x,y be FinSequence of REAL st ( len x) = ( len y) holds ( FR2FC ( mlt (x,y))) = ( mlt (( FR2FC x),( FR2FC y))) by Th35;

 theorem :: MATRIXC1:39



 Th37: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |(x, y)| = ( Sum ( mlt (x,(y *' ))))

 proof

 let x,y be FinSequence of COMPLEX ;



 A1: ( len ( Im y)) = ( len y) by COMPLSP2: 48;



 A2: ( len (y *' )) = ( len (y *' ));



 A3: (y *' ) = ( - ( - (y *' )))

 .= ((( - 1) * ( - 1)) * (y *' )) by COMPLSP2: 53

 .= (1 * (y *' ));



 A4: ( len (x *' )) = ( len x) by COMPLSP2:def 1;

 then

 A5: ( len (x + (x *' ))) = ( len x) by COMPLSP2: 6;



 A6: ( len ((x *' ) + x)) = ( len x) by A4, COMPLSP2: 6;



 A7: ( len x) = ( len x);



 A8: x = ( - ( - x))

 .= ((( - 1) * ( - 1)) * x) by COMPLSP2: 53

 .= (1 * x);

 set Imx = ( FR2FC ( Im x));

 assume that

 A9: ( len x) = ( len y);



 A10: ( len Imx) = ( len y) by A9, COMPLSP2: 48

 .= ( len (y *' )) by COMPLSP2:def 1;

 set Imy = ( FR2FC ( Im y));

 set Rey = ( FR2FC ( Re y));

 set Rex = ( FR2FC ( Re x));



 A11: ( len ( * Imx)) = ( len Imx) by COMPLSP2: 3

 .= ( len x) by COMPLSP2: 48

 .= ( len Rex) by COMPLSP2: 48;



 A12: ( len Rex) = ( len x) by COMPLSP2: 48;



 A13: ( len ( Im x)) = ( len x) by COMPLSP2: 48;

 then

 A14: ( mlt (( Im x),( Im y))) = ( mlt (( FR2FC ( Im x)),( FR2FC ( Im y)))) by A9, A1, Th35;



 A15: ( len ( Re y)) = ( len y) by COMPLSP2: 48;

 then

 A16: ( mlt (( Im x),( Re y))) = ( mlt (( FR2FC ( Im x)),( FR2FC ( Re y)))) by A9, A13, Th35;



 A17: ( len ( Re x)) = ( len x) by COMPLSP2: 48;

 then

 A18: ( mlt (( Re x),( Re y))) = ( mlt (( FR2FC ( Re x)),( FR2FC ( Re y)))) by A9, A15, Th35;



 A19: ( mlt (( Re x),( Im y))) = ( mlt (( FR2FC ( Re x)),( FR2FC ( Im y)))) by A9, A17, A1, Th35;



 A20: ( len ( * Imx)) = ( len Imx) by COMPLSP2: 3

 .= ( len y) by A9, COMPLSP2: 48

 .= ( len (y *' )) by COMPLSP2:def 1;

 Imx = (( - ((1 / 2) * )) * (x - (x *' ))) by COMPLSP2:def 3;



 then

 A21: ( * Imx) = (( * ( - ((1 / 2) * ))) * (x - (x *' ))) by COMPLSP2: 53

 .= ((1 / 2) * (x - (x *' )));

 Imy = (( - ((1 / 2) * )) * (y - (y *' ))) by COMPLSP2:def 3;



 then

 A22: ( * Imy) = (( * ( - ((1 / 2) * ))) * (y - (y *' ))) by COMPLSP2: 53

 .= ((1 / 2) * (y - (y *' )));



 A23: Rex = ((1 / 2) * (x + (x *' ))) by COMPLSP2:def 2;



 A24: ( len (y *' )) = ( len y) by COMPLSP2:def 1;

 then

 A25: ( len (y + (y *' ))) = ( len y) by COMPLSP2: 6;

 ( len (x - (x *' ))) = ( len x) by A4, COMPLSP2: 7;



 then

 A26: (Rex + ( * Imx)) = ((1 / 2) * ((x + (x *' )) + (x - (x *' )))) by A23, A21, A5, COMPLSP2: 30

 .= ((1 / 2) * ((x + ((x *' ) + x)) - (x *' ))) by A4, A5, COMPLSP2: 37

 .= ((1 / 2) * (x + ((x + (x *' )) - (x *' )))) by A4, A6, COMPLSP2: 37

 .= ((1 / 2) * (x + (x + ((x *' ) - (x *' ))))) by A4, COMPLSP2: 37

 .= ((1 / 2) * (x + (x + ( 0c ( len (x *' )))))) by COMPLSP2: 34

 .= ((1 / 2) * (x + (x + ( 0c ( len x))))) by COMPLSP2:def 1

 .= ((1 / 2) * (x + x)) by COMPLSP2: 33

 .= (((1 / 2) * x) + ((1 / 2) * x)) by A7, COMPLSP2: 30

 .= (((1 / 2) + (1 / 2)) * x) by COMPLSP2: 63

 .= x by A8;



 A27: Rey = ((1 / 2) * (y + (y *' ))) by COMPLSP2:def 2;

 ( len (y - (y *' ))) = ( len y) by A24, COMPLSP2: 7;



 then

 A28: (Rey - ( * Imy)) = ((1 / 2) * ((y + (y *' )) - (y - (y *' )))) by A27, A22, A25, COMPLSP2: 43

 .= ((1 / 2) * ((((y *' ) + y) - y) + (y *' ))) by A24, A25, COMPLSP2: 40

 .= ((1 / 2) * (((y *' ) + (y - y)) + (y *' ))) by A24, COMPLSP2: 37

 .= ((1 / 2) * (((y *' ) + ( 0c ( len y))) + (y *' ))) by COMPLSP2: 34

 .= ((1 / 2) * ((y *' ) + (y *' ))) by A24, COMPLSP2: 33

 .= (((1 / 2) * (y *' )) + ((1 / 2) * (y *' ))) by A2, COMPLSP2: 30

 .= (((1 / 2) + (1 / 2)) * (y *' )) by COMPLSP2: 63

 .= (y *' ) by A3;



 A29: ( len Rey) = ( len y) by COMPLSP2: 48;

 then

 A30: ( len ( mlt (Rex,Rey))) = ( len x) by A9, A12, FINSEQ_2: 72;



 A31: ( len ( * Imy)) = ( len Imy) by COMPLSP2: 3

 .= ( len y) by COMPLSP2: 48;

 then ( len ( mlt (Rex,( * Imy)))) = ( len Rex) by A9, A12, FINSEQ_2: 72;

 then

 A32: ( len (( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy))))) = ( len ( mlt (Rex,Rey))) by A12, A30, COMPLSP2: 7;



 A33: ( len Imx) = ( len x) by COMPLSP2: 48;

 then ( len ( mlt (Imx,Rey))) = ( len x) by A9, A29, FINSEQ_2: 72;

 then

 A34: ( len ( mlt (Imx,Rey))) = ( len ( mlt (Imx,( * Imy)))) by A9, A31, A33, FINSEQ_2: 72;



 A35: ( len Imy) = ( len y) by COMPLSP2: 48;

 then

 A36: ( len ( mlt (Imx,Imy))) = ( len x) by A9, A33, FINSEQ_2: 72;



 A37: ( len ( * ( mlt (Rex,Imy)))) = ( len ( mlt (Rex,Imy))) by COMPLSP2: 3

 .= ( len x) by A9, A12, A35, FINSEQ_2: 72;



 A38: ( len ( * ( mlt (Imx,Rey)))) = ( len ( mlt (Imx,Rey))) by COMPLSP2: 3

 .= ( len x) by A9, A29, A33, FINSEQ_2: 72;

 then

 A39: ( len (( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy))))) = ( len ( * ( mlt (Imx,Rey)))) by A30, A37, COMPLSP2: 7;

 ( len (( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy))))) = ( len ( * ( mlt (Imx,Rey)))) by A30, A37, A38, COMPLSP2: 7;



 then

 A40: ( len ((( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy)))) + ( * ( mlt (Imx,Rey))))) = ( len (( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy))))) by COMPLSP2: 6

 .= ( len ( mlt (Imx,Imy))) by A36, A30, A37, COMPLSP2: 7;

 |(x, y)| = ((( |(( Re x), ( Re y))| - ( * |(( Re x), ( Im y))|)) + ( * |(( Im x), ( Re y))|)) + |(( Im x), ( Im y))|) by COMPLSP2:def 4

 .= (((( Sum ( mlt (( Re x),( Re y)))) - ( * |(( Re x), ( Im y))|)) + ( * |(( Im x), ( Re y))|)) + |(( Im x), ( Im y))|)

 .= (((( Sum ( mlt (( Re x),( Re y)))) - ( * ( Sum ( mlt (( Re x),( Im y)))))) + ( * |(( Im x), ( Re y))|)) + |(( Im x), ( Im y))|)

 .= (((( Sum ( mlt (( Re x),( Re y)))) - ( * ( Sum ( mlt (( Re x),( Im y)))))) + ( * ( Sum ( mlt (( Im x),( Re y)))))) + |(( Im x), ( Im y))|)

 .= (((( Sum ( mlt (Rex,Rey))) - ( * ( Sum ( mlt (Rex,Imy))))) + ( * ( Sum ( mlt (Imx,Rey))))) + ( Sum ( mlt (( Im x),( Im y))))) by A16, A18, A19

 .= (((( Sum ( mlt (Rex,Rey))) - ( Sum ( * ( mlt (Rex,Imy))))) + ( * ( Sum ( mlt (Imx,Rey))))) + ( Sum ( mlt (Imx,Imy)))) by A14, Th26

 .= (((( Sum ( mlt (Rex,Rey))) - ( Sum ( * ( mlt (Rex,Imy))))) + ( Sum ( * ( mlt (Imx,Rey))))) + ( Sum ( mlt (Imx,Imy)))) by Th26

 .= ((( Sum (( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy))))) + ( Sum ( * ( mlt (Imx,Rey))))) + ( Sum ( mlt (Imx,Imy)))) by A30, A37, Th29

 .= (( Sum ((( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy)))) + ( * ( mlt (Imx,Rey))))) + ( Sum ( mlt (Imx,Imy)))) by A39, Th34

 .= ( Sum (((( mlt (Rex,Rey)) - ( * ( mlt (Rex,Imy)))) + ( * ( mlt (Imx,Rey)))) + ( mlt (Imx,Imy)))) by A40, Th34

 .= ( Sum (((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + ( * ( mlt (Imx,Rey)))) + ( mlt (Imx,Imy)))) by A9, A12, A35, Th23

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + (( * ( mlt (Imx,Rey))) + ( - ( - ( mlt (Imx,Imy))))))) by A36, A30, A38, A32, COMPLSP2: 28

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + (( * ( mlt (Imx,Rey))) - (( * ) * ( mlt (Imx,Imy))))))

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + (( * ( mlt (Imx,Rey))) - ( * ( * ( mlt (Imx,Imy))))))) by COMPLSP2: 53

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + (( * ( mlt (Imx,Rey))) - ( * ( mlt (Imx,( * Imy))))))) by A9, A35, A33, Th23

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + ( * (( mlt (Imx,Rey)) - ( mlt (Imx,( * Imy))))))) by A34, COMPLSP2: 43

 .= ( Sum ((( mlt (Rex,Rey)) - ( mlt (Rex,( * Imy)))) + ( * ( mlt (Imx,(y *' )))))) by A9, A31, A29, A33, A28, Th31

 .= ( Sum (( mlt (Rex,(Rey - ( * Imy)))) + ( * ( mlt (Imx,(y *' )))))) by A9, A31, A29, A12, Th31

 .= ( Sum (( mlt (Rex,(y *' ))) + ( mlt (( * Imx),(y *' ))))) by A10, A28, Th24

 .= ( Sum ( mlt (x,(y *' )))) by A11, A20, A26, Th33;

 hence thesis;

 end;

 theorem :: MATRIXC1:40

 for i,j be Nat, M1,M2 be Matrix of COMPLEX st ( width M1) = ( width M2) & j in ( Seg ( len M1)) holds ( Line ((M1 + M2),j)) = (( Line (M1,j)) + ( Line (M2,j)))

 proof

 let i,j be Nat, M1,M2 be Matrix of COMPLEX ;

 assume that

 A1: ( width M1) = ( width M2) and

 A2: j in ( Seg ( len M1));

 ( len ( Line (M2,j))) = ( width M1) by A1, MATRIX_0:def 7

 .= ( len ( Line (M1,j))) by MATRIX_0:def 7;



 then

 A3: ( len (( Line (M1,j)) + ( Line (M2,j)))) = ( len ( Line (M1,j))) by COMPLSP2: 6

 .= ( width M1) by MATRIX_0:def 7;



 A4: ( len ( Line ((M1 + M2),j))) = ( width (M1 + M2)) by MATRIX_0:def 7

 .= ( width M1) by Th5;



 A5: ( width (M1 + M2)) = ( width M1) by Th5;

 now

 let i be Nat;

 assume that

 A6: 1 <= i and

 A7: i <= ( len ( Line ((M1 + M2),j)));



 A8: i in ( Seg ( width M1)) by A4, A6, A7, FINSEQ_1: 1;

 i in ( Seg ( width M1)) by A4, A6, A7, FINSEQ_1: 1;

 then [j, i] in [:( Seg ( len M1)), ( Seg ( width M1)):] by A2, ZFMISC_1: 87;

 then

 A9: [j, i] in ( Indices M1) by FINSEQ_1:def 3;

 i in ( Seg ( len (( Line (M1,j)) + ( Line (M2,j))))) by A3, A4, A6, A7, FINSEQ_1: 1;

 then

 A10: i in ( dom (( Line (M1,j)) + ( Line (M2,j)))) by FINSEQ_1:def 3;



 A11: i in ( Seg ( width M2)) by A1, A4, A6, A7, FINSEQ_1: 1;

 i in ( Seg ( width (M1 + M2))) by A5, A4, A6, A7, FINSEQ_1: 1;



 hence (( Line ((M1 + M2),j)) . i) = ((M1 + M2) * (j,i)) by MATRIX_0:def 7

 .= ((M1 * (j,i)) + (M2 * (j,i))) by A9, Th6

 .= ((M1 * (j,i)) + (( Line (M2,j)) . i)) by A11, MATRIX_0:def 7

 .= ((( Line (M1,j)) . i) + (( Line (M2,j)) . i)) by A8, MATRIX_0:def 7

 .= ((( Line (M1,j)) + ( Line (M2,j))) . i) by A10, COMPLSP2: 1;

 end;

 hence thesis by A3, A4, FINSEQ_1: 14;

 end;

 theorem :: MATRIXC1:41



 Th39: for M be Matrix of COMPLEX st i in ( Seg ( len M)) holds ( Line (M,i)) = (( Line ((M *' ),i)) *' )

 proof

 let M be Matrix of COMPLEX ;

 assume

 A1: i in ( Seg ( len M));



 A2: ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7;



 A3: ( len (( Line ((M *' ),i)) *' )) = ( len ( Line ((M *' ),i))) by COMPLSP2:def 1

 .= ( width (M *' )) by MATRIX_0:def 7

 .= ( width M) by Def1;

 for j be Nat st 1 <= j & j <= ( len ( Line (M,i))) holds (( Line (M,i)) . j) = ((( Line ((M *' ),i)) *' ) . j)

 proof



 A4: i <= ( len M) by A1, FINSEQ_1: 1;



 A5: 1 <= i by A1, FINSEQ_1: 1;

 let j be Nat;

 assume that

 A6: 1 <= j and

 A7: j <= ( len ( Line (M,i)));



 A8: j in ( Seg ( width M)) by A2, A6, A7, FINSEQ_1: 1;

 then

 A9: j in ( Seg ( width (M *' ))) by Def1;

 j <= ( len (( Line ((M *' ),i)) *' )) by A3, A7, MATRIX_0:def 7;

 then

 A10: j <= ( len ( Line ((M *' ),i))) by COMPLSP2:def 1;

 j <= ( width M) by A7, MATRIX_0:def 7;

 then

 A11: [i, j] in ( Indices M) by A6, A5, A4, Th1;

 (( Line (M,i)) . j) = (((M * (i,j)) *' ) *' ) by A8, MATRIX_0:def 7

 .= (((M *' ) * (i,j)) *' ) by A11, Def1

 .= ((( Line ((M *' ),i)) . j) *' ) by A9, MATRIX_0:def 7

 .= ((( Line ((M *' ),i)) *' ) . j) by A6, A10, COMPLSP2:def 1;

 hence thesis;

 end;

 hence thesis by A2, A3, FINSEQ_1: 14;

 end;

 theorem :: MATRIXC1:42



 Th40: for F be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len F) = ( width M) holds ( mlt (F,(( Line ((M *' ),i)) *' ))) = (( mlt (( Line ((M *' ),i)),(F *' ))) *' )

 proof

 let F be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume

 A1: ( len F) = ( width M);

 ( len ( Line ((M *' ),i))) = ( width (M *' )) by MATRIX_0:def 7

 .= ( width M) by Def1;

 hence thesis by A1, Th22;

 end;

 theorem :: MATRIXC1:43



 Th41: for F be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len F) = ( width M) & ( len F) >= 1 holds ((M * F) *' ) = ((M *' ) * (F *' ))

 proof

 let F be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len F) = ( width M) and

 A2: ( len F) >= 1;



 A3: ( len (F *' )) = ( len F) by COMPLSP2:def 1;



 A4: ( width (M *' )) = ( width M) by Def1;



 A5: ( len ((M * F) *' )) = ( len (M * F)) by COMPLSP2:def 1

 .= ( len M) by Def6;



 A6: ( len (M *' )) = ( len M) by Def1;

 A7:

 now

 let i be Nat;

 assume that

 A8: 1 <= i and

 A9: i <= ( len ((M * F) *' ));



 A10: i in ( Seg ( len M)) by A5, A8, A9, FINSEQ_1: 1;

 ( len ( Line ((M *' ),i))) = ( len (F *' )) by A1, A3, A4, MATRIX_0:def 7;

 then

 A11: ( len ( mlt (( Line ((M *' ),i)),(F *' )))) >= 1 by A2, A3, FINSEQ_2: 72;



 A12: i in ( Seg ( len (M *' ))) by A5, A6, A8, A9, FINSEQ_1: 1;

 i <= ( len (M * F)) by A9, COMPLSP2:def 1;



 hence (((M * F) *' ) . i) = (((M * F) . i) *' ) by A8, COMPLSP2:def 1

 .= (( Sum ( mlt (F,( Line (M,i))))) *' ) by A10, Def6

 .= (( Sum ( mlt (F,(( Line ((M *' ),i)) *' )))) *' ) by A10, Th39

 .= (( Sum (( mlt (( Line ((M *' ),i)),(F *' ))) *' )) *' ) by A1, Th40

 .= ((( Sum ( mlt (( Line ((M *' ),i)),(F *' )))) *' ) *' ) by A11, Th21

 .= (((M *' ) * (F *' )) . i) by A12, Def6;

 end;

 ( len ((M *' ) * (F *' ))) = ( len (M *' )) by Def6

 .= ( len M) by Def1;

 hence thesis by A5, A7, FINSEQ_1: 14;

 end;

 theorem :: MATRIXC1:44

 for F1,F2,F3 be FinSequence of COMPLEX st ( len F1) = ( len F2) & ( len F2) = ( len F3) holds ( mlt (F1,( mlt (F2,F3)))) = ( mlt (( mlt (F1,F2)),F3))

 proof

 let F1,F2,F3 be FinSequence of COMPLEX ;

 assume that

 A1: ( len F1) = ( len F2) and

 A2: ( len F2) = ( len F3);

 reconsider f3 = F3 as Element of (( len F3) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider f2 = F2 as Element of (( len F2) -tuples_on COMPLEX ) by FINSEQ_2: 92;

 reconsider f1 = F1 as Element of (( len F1) -tuples_on COMPLEX ) by FINSEQ_2: 92;



 thus ( mlt (F1,( mlt (F2,F3)))) = ( multcomplex .: (( multcomplex .: (f1,f2)),f3)) by A1, A2, FINSEQOP: 28

 .= ( mlt (( mlt (F1,F2)),F3));

 end;

 theorem :: MATRIXC1:45

 for F be FinSequence of COMPLEX holds ( Sum ( - F)) = ( - ( Sum F))

 proof

 let F be FinSequence of COMPLEX ;



 thus ( Sum ( - F)) = ( addcomplex $$ ( compcomplex * F)) by SEQ_4:def 8

 .= ( compcomplex . ( addcomplex $$ F)) by SEQ_4: 51, SEQ_4: 52, SETWOP_2: 31

 .= ( - ( Sum F)) by BINOP_2:def 1;

 end;

 theorem :: MATRIXC1:46



 Th44: for F1,F2 be FinSequence of COMPLEX holds ( Sum (F1 ^ F2)) = (( Sum F1) + ( Sum F2))

 proof

 let F1,F2 be FinSequence of COMPLEX ;



 thus ( Sum (F1 ^ F2)) = ( addcomplex . (( addcomplex $$ F1),( addcomplex $$ F2))) by FINSOP_1: 5

 .= (( Sum F1) + ( Sum F2)) by BINOP_2:def 3;

 end;

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def9

 func LineSum M -> FinSequence of COMPLEX means

 : Def9: ( len it ) = ( len M) & for i be Nat st i in ( Seg ( len M)) holds (it . i) = ( Sum ( Line (M,i)));

 existence

 proof

 deffunc F( Nat) = ( Sum ( Line (M,$1)));

 consider z be FinSequence of COMPLEX such that

 A1: ( len z) = ( len M) and

 A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

 take z;

 thus ( len z) = ( len M) by A1;

 let j be Nat;

 ( dom z) = ( Seg ( len M)) by A1, FINSEQ_1:def 3;

 hence thesis by A2;

 end;

 uniqueness

 proof

 let p1,p2 be FinSequence of COMPLEX ;

 assume that

 A3: ( len p1) = ( len M) and

 A4: for j st j in ( Seg ( len M)) holds (p1 . j) = ( Sum ( Line (M,j))) and

 A5: ( len p2) = ( len M) and

 A6: for j st j in ( Seg ( len M)) holds (p2 . j) = ( Sum ( Line (M,j)));



 A7: ( dom p1) = ( Seg ( len M)) by A3, FINSEQ_1:def 3;

 for j be Nat st j in ( dom p1) holds (p1 . j) = (p2 . j)

 proof

 let j be Nat;

 assume

 A8: j in ( dom p1);

 then (p1 . j) = ( Sum ( Line (M,j))) by A4, A7;

 hence thesis by A6, A7, A8;

 end;

 hence thesis by A3, A5, FINSEQ_2: 9;

 end;

 end

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def10

 func ColSum M -> FinSequence of COMPLEX means

 : Def10: ( len it ) = ( width M) & for j be Nat st j in ( Seg ( width M)) holds (it . j) = ( Sum ( Col (M,j)));

 existence

 proof

 deffunc F( Nat) = ( Sum ( Col (M,$1)));

 consider f be FinSequence of COMPLEX such that

 A1: ( len f) = ( width M) and

 A2: for j be Nat st j in ( dom f) holds (f . j) = F(j) from FINSEQ_2:sch 1;

 take f;

 thus ( len f) = ( width M) by A1;

 let j be Nat;

 ( dom f) = ( Seg ( width M)) by A1, FINSEQ_1:def 3;

 hence thesis by A2;

 end;

 uniqueness

 proof

 let p1,p2 be FinSequence of COMPLEX ;

 assume that

 A3: ( len p1) = ( width M) and

 A4: for j st j in ( Seg ( width M)) holds (p1 . j) = ( Sum ( Col (M,j))) and

 A5: ( len p2) = ( width M) and

 A6: for j st j in ( Seg ( width M)) holds (p2 . j) = ( Sum ( Col (M,j)));



 A7: ( dom p1) = ( Seg ( width M)) by A3, FINSEQ_1:def 3;

 for j be Nat st j in ( dom p1) holds (p1 . j) = (p2 . j)

 proof

 let j be Nat;

 assume

 A8: j in ( dom p1);

 then (p1 . j) = ( Sum ( Col (M,j))) by A4, A7;

 hence thesis by A6, A7, A8;

 end;

 hence thesis by A3, A5, FINSEQ_2: 9;

 end;

 end

 theorem :: MATRIXC1:47



 Th45: for F be FinSequence of COMPLEX holds ( len F) = 1 implies ( Sum F) = (F . 1)

 proof

 let F be FinSequence of COMPLEX ;

 assume ( len F) = 1;

 then F = <*(F . 1)*> by FINSEQ_1: 40;

 hence thesis by FINSOP_1: 11;

 end;

 theorem :: MATRIXC1:48



 Th46: for f,g be FinSequence of COMPLEX , n be Nat st ( len f) = (n + 1) & g = (f | n) holds ( Sum f) = (( Sum g) + (f /. ( len f)))

 proof

 let f,g be FinSequence of COMPLEX , n be Nat;

 assume that

 A1: ( len f) = (n + 1) and

 A2: g = (f | n);



 A3: ( dom f) = ( Seg (n + 1)) by A1, FINSEQ_1:def 3;

 set q = <*(f /. ( len f))*>;

 set p = (g ^ q);



 A4: ( len q) = 1 by FINSEQ_1: 39;

 set n9 = ( Seg n);



 A5: g = (f | n9) by A2, FINSEQ_1:def 15;



 A6: n <= ( len f) by A1, NAT_1: 11;

 A7:

 now

 let u be object;

 assume

 A8: u in ( dom f);

 then u in { k where k be Nat : 1 <= k & k <= (n + 1) } by A3, FINSEQ_1:def 1;

 then

 consider i be Nat such that

 A9: u = i and

 A10: 1 <= i and

 A11: i <= (n + 1);

 now

 per cases ;

 case

 A12: i = (n + 1);

 then

 A13: (( len g) + 1) <= i by A1, A2, FINSEQ_1: 59, NAT_1: 11;

 i <= (( len g) + ( len q)) by A1, A2, A4, A12, FINSEQ_1: 59, NAT_1: 11;



 hence (p . i) = (q . (i - ( len g))) by A13, FINSEQ_1: 23

 .= (q . ((n + 1) - n)) by A1, A2, A12, FINSEQ_1: 59, NAT_1: 11

 .= (f /. (n + 1)) by A1, FINSEQ_1: 40

 .= (f . i) by A8, A9, A12, PARTFUN1:def 6;

 end;

 case i <> (n + 1);

 then i < (n + 1) by A11, XXREAL_0: 1;

 then i <= n by NAT_1: 13;

 then i in { k where k be Nat : 1 <= k & k <= n } by A10;

 then i in ( Seg n) by FINSEQ_1:def 1;

 then

 A14: i in ( dom g) by A5, A6, FINSEQ_1: 17;

 then (p . i) = (g . i) by FINSEQ_1:def 7;

 hence (p . i) = (f . i) by A5, A14, FUNCT_1: 47;

 end;

 end;

 hence (f . u) = (p . u) by A9;

 end;

 ( len (g ^ q)) = (( len g) + ( len q)) by FINSEQ_1: 22

 .= (( len g) + 1) by FINSEQ_1: 40

 .= ( len f) by A1, A2, FINSEQ_1: 59, NAT_1: 11;



 then ( dom f) = ( Seg ( len (g ^ q))) by FINSEQ_1:def 3

 .= ( dom (g ^ q)) by FINSEQ_1:def 3;

 then f = (g ^ <*(f /. ( len f))*>) by A7, FUNCT_1: 2;



 hence ( Sum f) = (( Sum g) + ( Sum <*(f /. ( len f))*>)) by Th44

 .= (( Sum g) + (f /. ( len f))) by FINSOP_1: 11;

 end;

 theorem :: MATRIXC1:49



 Th47: for M be Matrix of COMPLEX st ( len M) > 0 holds ( Sum ( LineSum M)) = ( Sum ( ColSum M))

 proof

 defpred P[ Nat] means for N be Matrix of COMPLEX st ($1 + 1) = ( len N) holds ( Sum ( LineSum N)) = ( Sum ( ColSum N));

 let M be Matrix of COMPLEX ;

 assume ( len M) > 0 ;

 then ( 0 + 1) <= ( len M) by NAT_1: 8;

 then (( 0 + 1) - 1) <= (( len M) - 1) by XREAL_1: 9;

 then

 A1: (( len M) -' 1) = (( len M) - 1) by XREAL_0:def 2;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat;

 assume

 A3: P[k];

 for N be Matrix of COMPLEX st ((k + 1) + 1) = ( len N) holds ( Sum ( LineSum N)) = ( Sum ( ColSum N))

 proof

 reconsider k1 = (k + 1) as Element of NAT ;

 let N be Matrix of COMPLEX ;

 consider n such that

 A4: for x be object st x in ( rng N) holds ex p be FinSequence of COMPLEX st x = p & ( len p) = n by MATRIX_0: 9;



 A5: ( rng (N | k1)) c= ( rng N) by FINSEQ_5: 19;

 then for x be object st x in ( rng (N | k1)) holds ex p be FinSequence of COMPLEX st x = p & ( len p) = n by A4;

 then

 reconsider N2 = (N | k1) as Matrix of COMPLEX by MATRIX_0: 9;

 set g1 = ( LineSum N2);

 consider n3 be Nat such that

 A6: for x2 be object st x2 in ( rng N) holds ex s be FinSequence st s = x2 & ( len s) = n3 by MATRIX_0:def 1;

 set f3 = ( LineSum N);



 A7: ( len ( Line (N,((k + 1) + 1)))) = ( width N) by MATRIX_0:def 7;

 assume

 A8: ((k + 1) + 1) = ( len N);

 then

 A9: ( len N2) = (k + 1) by FINSEQ_1: 59, NAT_1: 11;



 A10: ( len g1) = ( len N2) by Def9

 .= k1 by A8, FINSEQ_1: 59, NAT_1: 11;

 (1 + k) >= 1 by NAT_1: 11;

 then

 A11: ( len N2) >= 1 by A8, FINSEQ_1: 59, NAT_1: 11;

 then

 A12: ( len N2) > 0 ;

 1 in ( Seg ( len N2)) by A11, FINSEQ_1: 1;

 then 1 in ( dom N2) by FINSEQ_1:def 3;

 then

 A13: (N2 . 1) in ( rng N2) by FUNCT_1: 3;

 then ex s3 be FinSequence st s3 = (N2 . 1) & ( len s3) = n3 by A5, A6;

 then

 A14: ( width N2) = n3 by A13, A12, MATRIX_0:def 3;



 A15: ( len N) >= 1 by A8, NAT_1: 11;

 then

 A16: ( len N) > 0 ;

 1 in ( Seg ( len N)) by A15, FINSEQ_1: 1;

 then

 A17: 1 in ( dom N) by FINSEQ_1:def 3;

 then

 A18: (N . 1) in ( rng N) by FUNCT_1: 3;



 A19: ex s2 be FinSequence st s2 = (N . 1) & ( len s2) = n3 by A6, A17, FUNCT_1: 3;

 then

 A20: ( width N2) = ( width N) by A18, A14, A16, MATRIX_0:def 3;

 ( len f3) = (k1 + 1) by A8, Def9;

 then

 A21: ( len (f3 | k1)) = ( len g1) by A10, FINSEQ_1: 59, NAT_1: 11;



 A22: for n be Nat st 1 <= n & n <= ( len (f3 | k1)) holds ((f3 | k1) . n) = (g1 . n)

 proof

 let n be Nat;

 assume that

 A23: 1 <= n and

 A24: n <= ( len (f3 | k1));



 A25: n <= (k1 + 1) by A10, A21, A24, NAT_1: 13;

 then

 A26: n in ( Seg ( len N)) by A8, A23, FINSEQ_1: 1;



 A27: for n1 be Nat st 1 <= n1 & n1 <= ( len ( Line (N,n))) holds (( Line (N,n)) . n1) = (( Line (N2,n)) . n1)

 proof



 A28: (N2 . n) = (N . n) by A10, A21, A24, FINSEQ_3: 112;



 A29: n <= ( len N2) by A21, A24, Def9;

 let n1 be Nat;

 assume that

 A30: 1 <= n1 and

 A31: n1 <= ( len ( Line (N,n)));



 A32: n1 in ( Seg ( len ( Line (N,n)))) by A30, A31, FINSEQ_1: 1;

 then

 A33: n1 in ( Seg ( width N2)) by A20, MATRIX_0:def 7;



 A34: n1 in ( Seg ( width N)) by A32, MATRIX_0:def 7;

 then n1 <= ( width N) by FINSEQ_1: 1;

 then [n, n1] in ( Indices N) by A8, A23, A25, A30, Th1;

 then

 A35: ex pn be FinSequence of COMPLEX st pn = (N . n) & (N * (n,n1)) = (pn . n1) by MATRIX_0:def 5;

 n1 <= ( width N) by A34, FINSEQ_1: 1;

 then n1 <= ( width N2) by A8, A18, A19, A14, MATRIX_0:def 3;

 then

 A36: [n, n1] in ( Indices N2) by A23, A30, A29, Th1;

 n1 in ( Seg ( width N)) by A32, MATRIX_0:def 7;



 then (( Line (N,n)) . n1) = (N * (n,n1)) by MATRIX_0:def 7

 .= (N2 * (n,n1)) by A36, A35, A28, MATRIX_0:def 5

 .= (( Line (N2,n)) . n1) by A33, MATRIX_0:def 7;

 hence thesis;

 end;

 ( len ( Line (N,n))) = ( width N) by MATRIX_0:def 7

 .= ( width N2) by A8, A18, A19, A14, MATRIX_0:def 3

 .= ( len ( Line (N2,n))) by MATRIX_0:def 7;

 then

 A37: ( Line (N,n)) = ( Line (N2,n)) by A27, FINSEQ_1: 14;

 n in ( Seg ( len (f3 | k1))) by A23, A24, FINSEQ_1: 1;

 then n in ( dom (f3 | k1)) by FINSEQ_1:def 3;

 then

 A38: n in ( dom (f3 | ( Seg k1))) by FINSEQ_1:def 15;

 n in ( Seg k1) by A10, A21, A23, A24, FINSEQ_1: 1;

 then

 A39: n in ( Seg ( len N2)) by A8, FINSEQ_1: 59, NAT_1: 11;

 ((f3 | k1) . n) = ((f3 | ( Seg k1)) . n) by FINSEQ_1:def 15

 .= (( LineSum N) . n) by A38, FUNCT_1: 47

 .= ( Sum ( Line (N2,n))) by A26, A37, Def9

 .= (g1 . n) by A39, Def9;

 hence thesis;

 end;

 ( len ( ColSum N2)) = ( width N2) by Def10;



 then

 A40: ( len (( ColSum N2) + ( Line (N,((k + 1) + 1))))) = ( width N) by A20, A7, COMPLSP2: 6

 .= ( len ( ColSum N)) by Def10;



 A41: ( len ( ColSum N2)) = ( width N2) by Def10

 .= ( width N) by A8, A18, A19, A14, MATRIX_0:def 3

 .= ( len ( Line (N,((k + 1) + 1)))) by MATRIX_0:def 7;



 A42: ((k + 1) + 1) in ( Seg ( len N)) by A8, FINSEQ_1: 3;

 then ((k + 1) + 1) in ( Seg ( len ( LineSum N))) by Def9;

 then

 A43: ((k + 1) + 1) in ( dom ( LineSum N)) by FINSEQ_1:def 3;



 A44: ( len N) >= (k + 1) by A8, NAT_1: 11;



 A45: for j st 1 <= j & j <= ( width N) holds ((( ColSum N2) . j) + (N * (((k + 1) + 1),j))) = (( ColSum N) . j)

 proof

 let j;

 assume that

 A46: 1 <= j and

 A47: j <= ( width N);

 set g = ( Col (N2,j));

 set f = ( Col (N,j));



 A48: k1 <= ( len f) by A44, MATRIX_0:def 8;



 A49: for n be Nat st 1 <= n & n <= ( len (f | k1)) holds ((f | k1) . n) = (g . n)

 proof

 let n be Nat;

 assume that

 A50: 1 <= n and

 A51: n <= ( len (f | k1));



 A52: n <= k1 by A48, A51, FINSEQ_1: 59;

 then

 A53: (N2 . n) = (N . n) by FINSEQ_3: 112;

 n <= (k1 + 1) by A52, NAT_1: 13;

 then n in ( Seg ( len N)) by A8, A50, FINSEQ_1: 1;

 then

 A54: n in ( dom N) by FINSEQ_1:def 3;

 n <= ( len N) by A8, A52, NAT_1: 13;

 then [n, j] in ( Indices N) by A46, A47, A50, Th1;

 then

 A55: ex pn be FinSequence of COMPLEX st pn = (N . n) & (N * (n,j)) = (pn . j) by MATRIX_0:def 5;



 A56: j <= ( width N2) by A8, A18, A19, A14, A47, MATRIX_0:def 3;

 n in ( Seg k1) by A50, A52, FINSEQ_1: 1;

 then

 A57: n in ( dom N2) by A9, FINSEQ_1:def 3;

 n in ( Seg ( len (f | k1))) by A50, A51, FINSEQ_1: 1;

 then n in ( dom (f | k1)) by FINSEQ_1:def 3;

 then

 A58: n in ( dom (f | ( Seg k1))) by FINSEQ_1:def 15;

 n <= ( len N2) by A9, A48, A51, FINSEQ_1: 59;

 then

 A59: [n, j] in ( Indices N2) by A46, A50, A56, Th1;

 ((f | k1) . n) = ((f | ( Seg k1)) . n) by FINSEQ_1:def 15

 .= (( Col (N,j)) . n) by A58, FUNCT_1: 47

 .= (N * (n,j)) by A54, MATRIX_0:def 8

 .= (N2 * (n,j)) by A59, A55, A53, MATRIX_0:def 5

 .= (g . n) by A57, MATRIX_0:def 8;

 hence thesis;

 end;



 A60: ((k + 1) + 1) in ( Seg ( len N)) by A8, FINSEQ_1: 4;

 then

 A61: ((k + 1) + 1) in ( dom N) by FINSEQ_1:def 3;

 ( len g) = ( len N2) by MATRIX_0:def 8

 .= k1 by A8, FINSEQ_1: 59, NAT_1: 11;

 then

 A62: g = (f | k1) by A48, A49, FINSEQ_1: 14, FINSEQ_1: 59;



 A63: ( len ( Col (N,j))) = ( len N) by MATRIX_0:def 8;

 ((k + 1) + 1) in ( Seg ( len ( Col (N,j)))) by A60, MATRIX_0:def 8;

 then

 A64: ((k + 1) + 1) in ( dom ( Col (N,j))) by FINSEQ_1:def 3;



 A65: j in ( Seg ( width N)) by A46, A47, FINSEQ_1: 1;



 then ((( ColSum N2) . j) + (N * (((k + 1) + 1),j))) = (( Sum ( Col (N2,j))) + (N * (((k + 1) + 1),j))) by A20, Def10

 .= (( Sum ( Col (N2,j))) + (( Col (N,j)) . ((k + 1) + 1))) by A61, MATRIX_0:def 8

 .= (( Sum ( Col (N2,j))) + (( Col (N,j)) /. ((k + 1) + 1))) by A64, PARTFUN1:def 6

 .= ( Sum ( Col (N,j))) by A8, A63, A62, Th46

 .= (( ColSum N) . j) by A65, Def10;

 hence thesis;

 end;



 A66: for j be Nat st 1 <= j & j <= ( len ( ColSum N)) holds ((( ColSum N2) + ( Line (N,((k + 1) + 1)))) . j) = (( ColSum N) . j)

 proof

 let j be Nat;

 assume that

 A67: 1 <= j and

 A68: j <= ( len ( ColSum N));

 j in ( Seg ( len ( ColSum N))) by A67, A68, FINSEQ_1: 1;

 then

 A69: j in ( Seg ( width N2)) by A20, Def10;

 then

 A70: j <= ( width N) by A20, FINSEQ_1: 1;

 j in ( Seg ( len (( ColSum N2) + ( Line (N,((k + 1) + 1)))))) by A40, A67, A68, FINSEQ_1: 1;

 then j in ( dom (( ColSum N2) + ( Line (N,((k + 1) + 1))))) by FINSEQ_1:def 3;



 then ((( ColSum N2) + ( Line (N,((k + 1) + 1)))) . j) = ((( ColSum N2) . j) + (( Line (N,((k + 1) + 1))) . j)) by COMPLSP2: 1

 .= ((( ColSum N2) . j) + (N * (((k + 1) + 1),j))) by A20, A69, MATRIX_0:def 7

 .= (( ColSum N) . j) by A45, A67, A70;

 hence thesis;

 end;

 ( len ( LineSum N)) = ( len N) by Def9;



 then ( Sum ( LineSum N)) = (( Sum ( LineSum N2)) + (( LineSum N) /. ((k + 1) + 1))) by A8, A21, A22, Th46, FINSEQ_1: 14

 .= (( Sum ( LineSum N2)) + (( LineSum N) . ((k + 1) + 1))) by A43, PARTFUN1:def 6

 .= (( Sum ( ColSum N2)) + (( LineSum N) . ((k + 1) + 1))) by A3, A9

 .= (( Sum ( ColSum N2)) + ( Sum ( Line (N,((k + 1) + 1))))) by A42, Def9

 .= ( Sum (( ColSum N2) + ( Line (N,((k + 1) + 1))))) by A41, Th34

 .= ( Sum ( ColSum N)) by A40, A66, FINSEQ_1: 14;

 hence thesis;

 end;

 hence thesis;

 end;

 for N be Matrix of COMPLEX st ( 0 + 1) = ( len N) holds ( Sum ( LineSum N)) = ( Sum ( ColSum N))

 proof

 let N be Matrix of COMPLEX ;



 A71: ( len ( Line (N,1))) = ( width N) by MATRIX_0:def 7;

 assume

 A72: ( 0 + 1) = ( len N);

 then

 A73: 1 in ( Seg ( len N)) by FINSEQ_1: 3;



 A74: 1 in ( Seg 1) by FINSEQ_1: 3;



 A75: for j be Nat st 1 <= j & j <= ( width N) holds (( ColSum N) . j) = (( Line (N,1)) . j)

 proof



 A76: 1 in ( dom N) by A72, A74, FINSEQ_1:def 3;

 let j be Nat;

 assume that

 A77: 1 <= j and

 A78: j <= ( width N);



 A79: ( len ( Col (N,j))) = 1 by A72, MATRIX_0:def 8;



 A80: j in ( Seg ( width N)) by A77, A78, FINSEQ_1: 1;



 then (( ColSum N) . j) = ( Sum ( Col (N,j))) by Def10

 .= (( Col (N,j)) . 1) by A79, Th45

 .= (N * (1,j)) by A76, MATRIX_0:def 8

 .= (( Line (N,1)) . j) by A80, MATRIX_0:def 7;

 hence thesis;

 end;



 A81: ( len ( LineSum N)) = 1 by A72, Def9;

 ( len ( ColSum N)) = ( width N) by Def10;



 then ( Sum ( ColSum N)) = ( Sum ( Line (N,1))) by A71, A75, FINSEQ_1: 14

 .= (( LineSum N) . 1) by A73, Def9

 .= ( Sum ( LineSum N)) by A81, Th45;

 hence thesis;

 end;

 then

 A82: P[ 0 ];

 for i holds P[i] from NAT_1:sch 2( A82, A2);

 then ((( len M) -' 1) + 1) = ( len M) implies ( Sum ( LineSum M)) = ( Sum ( ColSum M));

 hence thesis by A1;

 end;

 definition

 let M be Matrix of COMPLEX ;

 :: MATRIXC1:def11

 func SumAll M -> Element of COMPLEX equals ( Sum ( LineSum M));

 coherence ;

 end

 theorem :: MATRIXC1:50



 Th48: for M be Matrix of COMPLEX holds ( ColSum M) = ( LineSum (M @ ))

 proof

 let M be Matrix of COMPLEX ;



 A1: ( len ( ColSum M)) = ( width M) by Def10;



 A2: ( len ( LineSum (M @ ))) = ( len (M @ )) by Def9;

 A3:

 now

 let i be Nat;

 assume that

 A4: 1 <= i and

 A5: i <= ( len ( ColSum M));

 i <= ( len ( LineSum (M @ ))) by A2, A1, A5, MATRIX_0:def 6;

 then i in ( Seg ( len ( LineSum (M @ )))) by A4, FINSEQ_1: 1;

 then

 A6: i in ( Seg ( len (M @ ))) by Def9;



 A7: i in ( Seg ( width M)) by A1, A4, A5, FINSEQ_1: 1;



 hence (( ColSum M) . i) = ( Sum ( Col (M,i))) by Def10

 .= ( Sum ( Line ((M @ ),i))) by A7, MATRIX_0: 59

 .= (( LineSum (M @ )) . i) by A6, Def9;

 end;

 ( len ( ColSum M)) = ( len ( LineSum (M @ ))) by A2, A1, MATRIX_0:def 6;

 hence thesis by A3, FINSEQ_1: 14;

 end;

 theorem :: MATRIXC1:51



 Th49: for M be Matrix of COMPLEX st ( len M) > 0 holds ( SumAll M) = ( SumAll (M @ ))

 proof

 let M be Matrix of COMPLEX ;

 assume ( len M) > 0 ;



 then ( SumAll M) = ( Sum ( ColSum M)) by Th47

 .= ( SumAll (M @ )) by Th48;

 hence thesis;

 end;

 definition

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( len M) and

 A2: ( len y) = ( width M);

 :: MATRIXC1:def12

 func QuadraticForm (x,M,y) -> Matrix of COMPLEX means

 : Def12: ( len it ) = ( len x) & ( width it ) = ( len y) & for i,j be Nat st [i, j] in ( Indices M) holds (it * (i,j)) = (((x . i) * (M * (i,j))) * ((y . j) *' ));

 existence

 proof

 deffunc F( Nat, Nat) = ( In ((((x . $1) * (M * ($1,$2))) * ((y . $2) *' )), COMPLEX ));

 consider M1 be Matrix of ( len M), ( width M), COMPLEX such that

 A3: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = F(i,j) from MATRIX_0:sch 1;

 take M1;

 thus

 A4: ( len M1) = ( len x) by A1, MATRIX_0:def 2;

 now

 per cases ;

 suppose

 A6: ( len M) = 0 ;

 then ( width M1) = 0 by A1, A4, MATRIX_0:def 3;

 hence ( width M1) = ( len y) by A2, A6, MATRIX_0:def 3;

 end;

 suppose ( len M) > 0 ;

 hence ( width M1) = ( len y) by A2, MATRIX_0: 23;

 end;

 end;



 A7: ( dom M) = ( dom M1) by A1, A4, FINSEQ_3: 29;

 let i,j be Nat;

 assume [i, j] in ( Indices M);

 then [i, j] in ( Indices M1) by A7, A5, A2;

 then (M1 * (i,j)) = F(i,j) by A3;

 hence thesis;

 end;

 uniqueness

 proof

 let M1,M2 be Matrix of COMPLEX ;

 assume that

 A8: ( len M1) = ( len x) and

 A9: ( width M1) = ( len y) and

 A10: for i, j st [i, j] in ( Indices M) holds (M1 * (i,j)) = (((x . i) * (M * (i,j))) * ((y . j) *' )) and

 A11: ( len M2) = ( len x) and

 A12: ( width M2) = ( len y) and

 A13: for i, j st [i, j] in ( Indices M) holds (M2 * (i,j)) = (((x . i) * (M * (i,j))) * ((y . j) *' ));

 now

 let i, j;

 assume

 A14: [i, j] in ( Indices M1);



 A15: ( dom M1) = ( dom M) by A1, A8, FINSEQ_3: 29;



 hence (M1 * (i,j)) = (((x . i) * (M * (i,j))) * ((y . j) *' )) by A2, A9, A10, A14

 .= (M2 * (i,j)) by A2, A9, A13, A14, A15;

 end;

 hence thesis by A8, A9, A11, A12, MATRIX_0: 21;

 end;

 end

 theorem :: MATRIXC1:52



 Th50: for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len x) = ( len M) & ( len y) = ( width M) & ( len y) > 0 holds (( QuadraticForm (x,M,y)) @ ) = (( QuadraticForm (y,(M @" ),x)) *' )

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( len M) and

 A2: ( len y) = ( width M) and

 A3: ( len y) > 0 ;



 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 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;

 reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A16: [i, j] in ( Indices (( QuadraticForm (x,M,y)) @ ));

 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 thesis;

 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 thesis by A13, A12, A31, A15, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:53



 Th51: for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len x) = ( len M) & ( len y) = ( width M) holds (( QuadraticForm (x,M,y)) *' ) = ( QuadraticForm ((x *' ),(M *' ),(y *' )))

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( len M) and

 A2: ( len y) = ( width M);



 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 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;

 reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

 assume

 A10: [i, j] in ( Indices (( QuadraticForm (x,M,y)) *' ));

 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 thesis;

 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 thesis by A6, A23, A24, A9, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:54



 Th52: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) & 0 < ( len y) holds |(x, y)| = ( |(y, x)| *' )

 proof

 let x,y be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: 0 < ( len y);



 A3: ( 0 + 1) <= ( len x) by A1, A2, NAT_1: 8;

 ( len (x *' )) = ( len x) by COMPLSP2:def 1;

 then

 A4: ( len ( mlt (y,(x *' )))) = ( len y) by A1, FINSEQ_2: 72;

 ( |(y, x)| *' ) = (( Sum ( mlt (y,(x *' )))) *' ) by A1, Th37

 .= ( Sum (( mlt (y,(x *' ))) *' )) by A1, A3, A4, Th21

 .= ( Sum ( mlt (x,(y *' )))) by A1, Th22

 .= |(x, y)| by A1, Th37;

 hence thesis;

 end;

 theorem :: MATRIXC1:55



 Th53: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) & 0 < ( len y) holds ( |(x, y)| *' ) = |((x *' ), (y *' ))|

 proof

 let x,y be FinSequence of COMPLEX ;

 assume that

 A1: ( len x) = ( len y) and

 A2: 0 < ( len y);



 A3: ( 0 + 1) <= ( len x) by A1, A2, NAT_1: 8;



 A4: ( len (y *' )) = ( len y) by COMPLSP2:def 1;

 then

 A5: ( len ( mlt (x,(y *' )))) = ( len x) by A1, FINSEQ_2: 72;

 ( len (x *' )) = ( len x) by COMPLSP2:def 1;



 then |((x *' ), (y *' ))| = ( Sum ( mlt ((x *' ),((y *' ) *' )))) by A1, A4, Th37

 .= ( Sum (( mlt (x,(y *' ))) *' )) by A1, A4, Th25

 .= (( Sum ( mlt (x,(y *' )))) *' ) by A3, A5, Th21

 .= ( |(x, y)| *' ) by A1, Th37;

 hence thesis;

 end;

 theorem :: MATRIXC1:56

 for M be Matrix of COMPLEX st ( width M) > 0 holds ((M @ ) *' ) = ((M *' ) @ )

 proof

 let M be Matrix of COMPLEX ;

 assume

 A1: ( width M) > 0 ;

 ( width (M *' )) = ( width M) by Def1;



 then

 A2: ( width ((M *' ) @ )) = ( len (M *' )) by A1, MATRIX_0: 54

 .= ( len M) by Def1;



 A3: ( width ((M @ ) *' )) = ( width (M @ )) by Def1;



 A4: ( len ((M @ ) *' )) = ( len (M @ )) by Def1

 .= ( width M) by MATRIX_0:def 6;



 A5: ( width ((M @ ) *' )) = ( width (M @ )) by Def1

 .= ( len M) by A1, MATRIX_0: 54;



 A6: ( len ((M @ ) *' )) = ( len (M @ )) by Def1;



 A7: for i, j st [i, j] in ( Indices ((M @ ) *' )) holds (((M @ ) *' ) * (i,j)) = (((M *' ) @ ) * (i,j))

 proof

 let i, j;

 assume

 A8: [i, j] in ( Indices ((M @ ) *' ));

 then

 A9: 1 <= i by Th1;



 A10: 1 <= j by A8, Th1;



 A11: j <= ( width (M @ )) by A3, A8, Th1;

 i <= ( len (M @ )) by A6, A8, Th1;

 then

 A12: [i, j] in ( Indices (M @ )) by A9, A10, A11, Th1;

 then

 A13: [j, i] in ( Indices M) by MATRIX_0:def 6;

 j <= ( width ((M @ ) *' )) by A8, Th1;

 then

 A14: j <= ( len (M *' )) by A5, Def1;

 i <= ( len ((M @ ) *' )) by A8, Th1;

 then

 A15: i <= ( width (M *' )) by A4, Def1;



 A16: 1 <= i by A8, Th1;

 1 <= j by A8, Th1;

 then

 A17: [j, i] in ( Indices (M *' )) by A14, A16, A15, Th1;

 (((M @ ) *' ) * (i,j)) = (((M @ ) * (i,j)) *' ) by A12, Def1

 .= ((M * (j,i)) *' ) by A13, MATRIX_0:def 6

 .= ((M *' ) * (j,i)) by A13, Def1

 .= (((M *' ) @ ) * (i,j)) by A17, MATRIX_0:def 6;

 hence thesis;

 end;

 ( len ((M *' ) @ )) = ( width (M *' )) by MATRIX_0:def 6

 .= ( width M) by Def1;

 hence thesis by A4, A5, A2, A7, MATRIX_0: 21;

 end;

 theorem :: MATRIXC1:57



 Th55: for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len x) = ( width M) & ( len y) = ( len M) & ( len x) > 0 & ( len y) > 0 holds |(x, ((M @" ) * y))| = ( SumAll ( QuadraticForm (x,(M @ ),y)))

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( width M) and

 A2: ( len y) = ( len M) and

 A3: ( len x) > 0 and

 A4: ( len y) > 0 ;



 A5: ( width (M @ )) = ( len y) by A1, A2, A3, MATRIX_0: 54;

 then

 A6: ( width ((M @ ) *' )) = ( len y) by Def1;



 A7: ( dom ( LineSum ( QuadraticForm (x,(M @ ),y)))) = ( Seg ( len ( LineSum ( QuadraticForm (x,(M @ ),y))))) by FINSEQ_1:def 3

 .= ( Seg ( len ( QuadraticForm (x,(M @ ),y)))) by Def9;



 A8: ( len (M @ )) = ( len x) by A1, MATRIX_0:def 6;



 A9: ( len ( LineSum ( QuadraticForm (x,(M @ ),y)))) = ( len ( QuadraticForm (x,(M @ ),y))) by Def9

 .= ( len x) by A8, A5, Def12;



 A10: ( len (M @" )) = ( len (M @ )) by Def1

 .= ( len x) by A1, MATRIX_0:def 6;

 then

 A11: ( len ((M @" ) * y)) = ( len x) by Def6;

 then ( len (((M @" ) * y) *' )) = ( len x) by COMPLSP2:def 1;

 then

 A12: ( len ( LineSum ( QuadraticForm (x,(M @ ),y)))) = ( len ( mlt (x,(((M @" ) * y) *' )))) by A9, FINSEQ_2: 72;



 A13: ( 0 + 1) <= ( len y) by A4, NAT_1: 13;

 for i be Nat st 1 <= i & i <= ( len ( LineSum ( QuadraticForm (x,(M @ ),y)))) holds (( LineSum ( QuadraticForm (x,(M @ ),y))) . i) = (( mlt (x,(((M @" ) * y) *' ))) . i)

 proof

 let i be Nat;

 assume that

 A14: 1 <= i and

 A15: i <= ( len ( LineSum ( QuadraticForm (x,(M @ ),y))));



 A16: ( len y) = ( width ( QuadraticForm (x,(M @ ),y))) by A8, A5, Def12

 .= ( len ( Line (( QuadraticForm (x,(M @ ),y)),i))) by MATRIX_0:def 7;



 A17: ( len ( Line ((M @" ),i))) = ( len y) by A6, MATRIX_0:def 7;

 then

 A18: ( len ( mlt (( Line ((M @" ),i)),y))) >= 1 by A13, FINSEQ_2: 72;

 ( len (M @ )) = ( len ( QuadraticForm (x,(M @ ),y))) by A8, A5, Def12;

 then

 A19: ( len (M @ )) = ( len ( LineSum ( QuadraticForm (x,(M @ ),y)))) by Def9;

 then

 A20: i in ( Seg ( len (M @" ))) by A8, A10, A14, A15, FINSEQ_1: 1;



 A21: for j be Nat st 1 <= j & j <= ( len ( Line (( QuadraticForm (x,(M @ ),y)),i))) holds (((x . i) * (( mlt (( Line ((M @" ),i)),y)) *' )) . j) = (( Line (( QuadraticForm (x,(M @ ),y)),i)) . j)

 proof



 A22: ( len ( Line ((M @ ),i))) = ( width (M @ )) by MATRIX_0:def 7

 .= ( len y) by A1, A2, A3, MATRIX_0: 54

 .= ( len (y *' )) by COMPLSP2:def 1;

 let j be Nat;

 assume that

 A23: 1 <= j and

 A24: j <= ( len ( Line (( QuadraticForm (x,(M @ ),y)),i)));



 A25: j in ( Seg ( width (M @ ))) by A5, A16, A23, A24, FINSEQ_1: 1;

 j in ( Seg ( len y)) by A16, A23, A24, FINSEQ_1: 1;

 then j in ( Seg ( len (y *' ))) by COMPLSP2:def 1;

 then j in ( Seg ( len ( mlt (( Line ((M @ ),i)),(y *' ))))) by A22, FINSEQ_2: 72;

 then

 A26: j in ( dom ( mlt (( Line ((M @ ),i)),(y *' )))) by FINSEQ_1:def 3;

 j in ( Seg ( len ( Line (( QuadraticForm (x,(M @ ),y)),i)))) by A23, A24, FINSEQ_1: 1;

 then

 A27: j in ( Seg ( width ( QuadraticForm (x,(M @ ),y)))) by MATRIX_0:def 7;

 j <= ( width (M @ )) by A1, A2, A3, A16, A24, MATRIX_0: 54;

 then

 A28: [i, j] in ( Indices (M @ )) by A14, A15, A19, A23, Th1;

 (((x . i) * (( mlt (( Line ((M @" ),i)),y)) *' )) . j) = ((x . i) * ((( mlt (( Line ((M @" ),i)),y)) *' ) . j)) by COMPLSP2: 16

 .= ((x . i) * (( mlt ((( Line ((M @" ),i)) *' ),(y *' ))) . j)) by A17, Th25

 .= ((x . i) * (( mlt (( Line ((M @ ),i)),(y *' ))) . j)) by A8, A10, A20, Th39

 .= ((x . i) * ((( Line ((M @ ),i)) . j) * ((y *' ) . j))) by A26, Th17

 .= ((x . i) * ((( Line ((M @ ),i)) . j) * ((y . j) *' ))) by A16, A23, A24, COMPLSP2:def 1

 .= (((x . i) * (( Line ((M @ ),i)) . j)) * ((y . j) *' ))

 .= (((x . i) * ((M @ ) * (i,j))) * ((y . j) *' )) by A25, MATRIX_0:def 7

 .= (( QuadraticForm (x,(M @ ),y)) * (i,j)) by A8, A5, A28, Def12;

 hence thesis by A27, MATRIX_0:def 7;

 end;

 i in ( Seg ( len ( LineSum ( QuadraticForm (x,(M @ ),y))))) by A14, A15, FINSEQ_1: 1;

 then

 A29: i in ( dom ( LineSum ( QuadraticForm (x,(M @ ),y)))) by FINSEQ_1:def 3;



 A30: ( len ( Line ((M @" ),i))) = ( len y) by A6, MATRIX_0:def 7;



 A31: ( len ((x . i) * (( mlt (( Line ((M @" ),i)),y)) *' ))) = ( len (( mlt (( Line ((M @" ),i)),y)) *' )) by COMPLSP2: 3

 .= ( len ( mlt (( Line ((M @" ),i)),y))) by COMPLSP2:def 1

 .= ( len ( Line (( QuadraticForm (x,(M @ ),y)),i))) by A16, A30, FINSEQ_2: 72;

 i in ( Seg ( len ( mlt (x,(((M @" ) * y) *' ))))) by A12, A14, A15, FINSEQ_1: 1;

 then i in ( dom ( mlt (x,(((M @" ) * y) *' )))) by FINSEQ_1:def 3;



 then (( mlt (x,(((M @" ) * y) *' ))) . i) = ((x . i) * ((((M @" ) * y) *' ) . i)) by Th17

 .= ((x . i) * ((((M @" ) * y) . i) *' )) by A11, A9, A14, A15, COMPLSP2:def 1;



 then (( mlt (x,(((M @" ) * y) *' ))) . i) = ((x . i) * (( Sum ( mlt (( Line ((M @" ),i)),y))) *' )) by A20, Def6

 .= ((x . i) * ( Sum (( mlt (( Line ((M @" ),i)),y)) *' ))) by A18, Th21

 .= ( Sum ((x . i) * (( mlt (( Line ((M @" ),i)),y)) *' ))) by Th26;

 then (( mlt (x,(((M @" ) * y) *' ))) . i) = ( Sum ( Line (( QuadraticForm (x,(M @ ),y)),i))) by A31, A21, FINSEQ_1: 14;

 hence thesis by A7, A29, Def9;

 end;

 then ( Sum ( LineSum ( QuadraticForm (x,(M @ ),y)))) = ( Sum ( mlt (x,(((M @" ) * y) *' )))) by A12, FINSEQ_1: 14;

 hence thesis by A11, Th37;

 end;

 theorem :: MATRIXC1:58



 Th56: for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len y) = ( len M) & ( len x) = ( width M) & ( len x) > 0 & ( len y) > 0 holds |((M * x), y)| = ( SumAll ( QuadraticForm (x,(M @ ),y)))

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len y) = ( len M) and

 A2: ( len x) = ( width M) and

 A3: ( len x) > 0 and

 A4: ( len y) > 0 ;



 A5: ((M @ ) @" ) = (M *' ) by A1, A2, A3, A4, MATRIX_0: 57;



 A6: ( width (M @ )) = ( len M) by A2, A3, MATRIX_0: 54;



 A7: ( len (x *' )) = ( width M) by A2, COMPLSP2:def 1;

 ( len (y *' )) = ( len M) by A1, COMPLSP2:def 1;

 then

 A8: ( len ( QuadraticForm ((y *' ),M,(x *' )))) = ( len M) by A7, Def12;



 A9: ( len (x *' )) = ( len x) by COMPLSP2:def 1;



 A10: ( 0 + 1) <= ( len x) by A3, NAT_1: 13;



 A11: ( len (y *' )) = ( len y) by COMPLSP2:def 1;



 A12: ( len (M @ )) = ( width M) by MATRIX_0:def 6;



 A13: ( len (M * x)) = ( len M) by Def6;



 hence |((M * x), y)| = ( |(y, (M * x))| *' ) by A1, A4, Th52

 .= |((y *' ), ((M * x) *' ))| by A1, A4, A13, Th53

 .= |((y *' ), ((M *' ) * (x *' )))| by A2, A10, Th41

 .= ( SumAll ( QuadraticForm ((y *' ),((M @ ) @ ),(x *' )))) by A1, A2, A3, A4, A9, A11, A12, A6, A5, Th55

 .= ( SumAll ( QuadraticForm ((y *' ),M,(x *' )))) by A1, A2, A3, A4, MATRIX_0: 57

 .= ( SumAll (( QuadraticForm ((y *' ),M,(x *' ))) @ )) by A1, A4, A8, Th49

 .= ( SumAll (( QuadraticForm ((x *' ),(M @" ),(y *' ))) *' )) by A1, A2, A3, A9, A11, Th50

 .= ( SumAll ((( QuadraticForm (x,(M @ ),y)) *' ) *' )) by A1, A2, A12, A6, Th51

 .= ( SumAll ( QuadraticForm (x,(M @ ),y)));

 end;

 theorem :: MATRIXC1:59



 Th57: for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len x) = ( width M) & ( len y) = ( len M) & ( width M) > 0 & ( len M) > 0 holds |((M * x), y)| = |(x, ((M @" ) * y))|

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( width M) and

 A2: ( len y) = ( len M) and

 A3: ( width M) > 0 and

 A4: ( len M) > 0 ;

 |(x, ((M @" ) * y))| = ( SumAll ( QuadraticForm (x,(M @ ),y))) by A1, A2, A3, A4, Th55;

 hence thesis by A1, A2, A3, A4, Th56;

 end;

 theorem :: MATRIXC1:60

 for x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX st ( len x) = ( len M) & ( len y) = ( width M) & ( width M) > 0 & ( len M) > 0 holds |(x, (M * y))| = |(((M @" ) * x), y)|

 proof

 let x,y be FinSequence of COMPLEX , M be Matrix of COMPLEX ;

 assume that

 A1: ( len x) = ( len M) and

 A2: ( len y) = ( width M) and

 A3: ( width M) > 0 and

 A4: ( len M) > 0 ;



 A5: ( len ((M @" ) * x)) = ( len (M @" )) by Def6

 .= ( len (M @ )) by Def1

 .= ( width M) by MATRIX_0:def 6;

 ( len (M * y)) = ( len x) by A1, Def6;



 hence |(x, (M * y))| = ( |((M * y), x)| *' ) by A1, A4, Th52

 .= ( |(y, ((M @" ) * x))| *' ) by A1, A2, A3, A4, Th57

 .= |(((M @" ) * x), y)| by A2, A3, A5, Th52;

 end;