complsp2.miz

begin

 reserve i,j for Element of NAT ,

x,y,z for FinSequence of COMPLEX ,

c for Element of COMPLEX ,

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

 definition

 let z be FinSequence of COMPLEX ;

 :: original: *'

 redefine

 :: COMPLSP2:def1

 func z *' -> FinSequence of COMPLEX means

 : Def1: ( len it ) = ( len z) & for i be Nat st 1 <= i & i <= ( len z) holds (it . i) = ((z . i) *' );

 coherence

 proof

 set f = (z *' );



 A1: ( dom f) = ( dom z) by COMSEQ_2:def 1;

 ex n be Nat st ( dom z) = ( Seg n) by FINSEQ_1:def 2;

 then

 A2: f is FinSequence by A1, FINSEQ_1:def 2;

 ( rng f) c= COMPLEX

 proof

 let y be object;

 thus thesis by XCMPLX_0:def 2;

 end;

 hence thesis by A2, FINSEQ_1:def 4;

 end;

 compatibility

 proof

 let IT be FinSequence of COMPLEX ;

 thus IT = (z *' ) implies ( len IT) = ( len z) & for i be Nat st 1 <= i & i <= ( len z) holds (IT . i) = ((z . i) *' )

 proof

 assume

 A3: IT = (z *' );

 then ( dom IT) = ( dom z) by COMSEQ_2:def 1;

 hence thesis by A3, COMSEQ_2:def 1, FINSEQ_3: 25, FINSEQ_3: 29;

 end;

 assume that

 A4: ( len IT) = ( len z) and

 A5: for i be Nat st 1 <= i & i <= ( len z) holds (IT . i) = ((z . i) *' );



 A6: ( dom IT) = ( dom z) by A4, FINSEQ_3: 29;

 now

 let i be set;

 assume

 A7: i in ( dom IT);

 then

 reconsider j = i as Nat;

 1 <= j & j <= ( len z) by A4, A7, FINSEQ_3: 25;

 hence (IT . i) = ((z . i) *' ) by A5;

 end;

 hence IT = (z *' ) by A6, COMSEQ_2:def 1;

 end;

 end



 Lm1: (c * x) = (( multcomplex [;] (c,( id COMPLEX ))) * x)

 proof

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

 hence thesis by SEQ_4:def 9;

 end;

 theorem :: COMPLSP2:1

 i in ( dom (x + y)) implies ((x + y) . i) = ((x . i) + (y . i)) by VALUED_1:def 1;

 theorem :: COMPLSP2:2

 i in ( dom (x - y)) implies ((x - y) . i) = ((x . i) - (y . i)) by VALUED_1: 13;

 definition

 let i, R1, R2;

 :: original: -

 redefine

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

 coherence

 proof

 (R1 - R2) = ( diffcomplex .: (R1,R2)) by SEQ_4:def 7;

 hence thesis by FINSEQ_2: 120;

 end;

 end

 definition

 let i, R1, R2;

 :: original: +

 redefine

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

 coherence

 proof

 (R1 + R2) = ( addcomplex .: (R1,R2)) by SEQ_4:def 6;

 hence thesis by FINSEQ_2: 120;

 end;

 end

 definition

 let i, R;

 let r be Complex;

 :: original: *

 redefine

 func r * R -> Element of (i -tuples_on COMPLEX ) ;

 coherence

 proof

 reconsider q = r as Element of COMPLEX by XCMPLX_0:def 2;

 (q * R) = (( multcomplex [;] (q,( id COMPLEX ))) * R) by Lm1;

 hence thesis by FINSEQ_2: 113;

 end;

 end



 Lm2: for F be complex-valued FinSequence holds F is FinSequence of COMPLEX

 proof

 let F be complex-valued FinSequence;

 ( rng F) c= COMPLEX by VALUED_0:def 1;

 hence thesis by FINSEQ_1:def 4;

 end;

 theorem :: COMPLSP2:3



 Th3: for a be Complex, x be complex-valued FinSequence holds ( len (a (#) x)) = ( len x)

 proof

 let a be Complex, x be complex-valued FinSequence;

 set n = ( len x);

 x is FinSequence of COMPLEX by Lm2;

 then

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

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

 ( len (a9 * z)) = n by CARD_1:def 7;

 hence thesis;

 end;

 theorem :: COMPLSP2:4

 for x be complex-valued FinSequence holds ( dom x) = ( dom ( - x)) by VALUED_1: 8;

 theorem :: COMPLSP2:5



 Th5: for x be complex-valued FinSequence holds ( len ( - x)) = ( len x)

 proof

 let x be complex-valued FinSequence;

 ( dom ( - x)) = ( dom x) by VALUED_1: 8;

 hence thesis by FINSEQ_3: 29;

 end;

 theorem :: COMPLSP2:6



 Th6: for x1,x2 be complex-valued FinSequence st ( len x1) = ( len x2) holds ( len (x1 + x2)) = ( len x1)

 proof

 let x1,x2 be complex-valued FinSequence;

 set n = ( len x1);



 A1: x2 is FinSequence of COMPLEX by Lm2;

 x1 is FinSequence of COMPLEX by Lm2;

 then

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

 assume ( len x1) = ( len x2);

 then

 reconsider z2 = x2 as Element of (n -tuples_on COMPLEX ) by A1, FINSEQ_2: 92;

 ( dom (z1 + z2)) = ( Seg n) by FINSEQ_2: 124;

 hence thesis by FINSEQ_1:def 3;

 end;

 theorem :: COMPLSP2:7



 Th7: for x1,x2 be complex-valued FinSequence st ( len x1) = ( len x2) holds ( len (x1 - x2)) = ( len x1)

 proof

 let x1,x2 be complex-valued FinSequence;

 set n = ( len x1);



 A1: x2 is FinSequence of COMPLEX by Lm2;

 x1 is FinSequence of COMPLEX by Lm2;

 then

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

 assume ( len x1) = ( len x2);

 then

 reconsider z2 = x2 as Element of (n -tuples_on COMPLEX ) by A1, FINSEQ_2: 92;

 ( dom (z1 - z2)) = ( Seg n) by FINSEQ_2: 124;

 hence thesis by FINSEQ_1:def 3;

 end;

 theorem :: COMPLSP2:8

 for f be complex-valued FinSequence holds f is Element of ( COMPLEX ( len f))

 proof

 let f be complex-valued FinSequence;

 f is FinSequence of COMPLEX by Lm2;

 then f is Element of ( COMPLEX * ) by FINSEQ_1:def 11;

 then f in { s where s be Element of ( COMPLEX * ) : ( len s) = ( len f) };

 then f in (( len f) -tuples_on COMPLEX ) by FINSEQ_2:def 4;

 hence thesis by SEQ_4:def 11;

 end;

 ::$Canceled

 theorem :: COMPLSP2:13



 Th9: for x be FinSequence of COMPLEX holds (( - x) . i) = ( - (x . i))

 proof

 let x be FinSequence of COMPLEX ;

 per cases ;

 suppose

 A1: not i in ( dom ( - x));

 then

 A2: not i in ( dom x) by VALUED_1: 8;



 thus (( - x) . i) = ( - 0 ) by A1, FUNCT_1:def 2

 .= ( - (x . i)) by A2, FUNCT_1:def 2;

 end;

 suppose

 A3: i in ( dom ( - x));

 set r = (x . i);

 ( - x) = ( compcomplex * x) by SEQ_4:def 8;

 then (( - x) . i) = ( compcomplex . r) by A3, FUNCT_1: 12;

 hence thesis by BINOP_2:def 1;

 end;

 end;

 definition

 let i, R;

 :: original: -

 redefine

 func - R -> Element of (i -tuples_on COMPLEX ) ;

 coherence

 proof

 ( - R) = ( compcomplex * R) by SEQ_4:def 8;

 hence thesis by FINSEQ_2: 113;

 end;

 end

 theorem :: COMPLSP2:14

 c = (R . j) implies (( - R) . j) = ( - c) by Th9;

 theorem :: COMPLSP2:15



 Th11: for a be Complex holds ( dom (a * x)) = ( dom x)

 proof

 let a be Complex;

 ( dom (a multcomplex )) = COMPLEX by FUNCT_2:def 1;

 then ( rng x) c= ( dom (a multcomplex )) by FINSEQ_1:def 4;



 hence ( dom x) = ( dom ((a multcomplex ) * x)) by RELAT_1: 27

 .= ( dom (a * x)) by SEQ_4:def 9;

 end;

 theorem :: COMPLSP2:16



 Th12: for i be Nat, a be Complex holds ((a * x) . i) = (a * (x . i))

 proof

 let i be Nat, a be Complex;

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

 per cases ;

 suppose

 A1: not i in ( dom (a * x));

 then

 A2: not i in ( dom x) by Th11;



 thus ((a * x) . i) = (a * 0 ) by A1, FUNCT_1:def 2

 .= (a * (x . i)) by A2, FUNCT_1:def 2;

 end;

 suppose

 A3: i in ( dom (a * x));

 set a9 = (x . i);



 A4: (a * x) = (( multcomplex [;] (aa,( id COMPLEX ))) * x) by Lm1;

 then

 A5: a9 in ( dom ( multcomplex [;] (aa,( id COMPLEX )))) by A3, FUNCT_1: 11;



 thus ((a * x) . i) = (( multcomplex [;] (aa,( id COMPLEX ))) . a9) by A3, A4, FUNCT_1: 12

 .= ( multcomplex . (a,(( id COMPLEX ) . a9))) by A5, FUNCOP_1: 32

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

 end;

 end;

 theorem :: COMPLSP2:17



 Th13: for a be Complex holds ((a * x) *' ) = ((a *' ) * (x *' ))

 proof

 let a be Complex;

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

 ( len ((a *' ) * (x *' ))) = ( len (x *' )) by Th3;

 then

 A1: ( len ((a *' ) * (x *' ))) = ( len x) by Def1;



 A2: ( len (a * x)) = ( len x) by Th3;

 A3:

 now

 let i be Nat;

 assume that

 A4: 1 <= i and

 A5: i <= ( len ((a * x) *' ));



 A6: i <= ( len (a * x)) by A5, Def1;



 hence (((a * x) *' ) . i) = (((a * x) . i) *' ) by A4, Def1

 .= ((aa * (x . i)) *' ) by Th12

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

 .= ((a *' ) * ((x *' ) . i)) by A2, A4, A6, Def1

 .= (((a *' ) * (x *' )) . i) by Th12;

 end;

 ( len ((a * x) *' )) = ( len (a * x)) by Def1;

 hence thesis by A1, A3, Th3;

 end;

 theorem :: COMPLSP2:18



 Th14: ((R1 + R2) . j) = ((R1 . j) + (R2 . j))

 proof

 per cases ;

 suppose

 A1: not j in ( Seg i);

 then

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



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

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



 hence ((R1 + R2) . j) = ( 0 + 0 ) by FUNCT_1:def 2

 .= ((R1 . j) + 0 ) by A3, FUNCT_1:def 2

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

 end;

 suppose j in ( Seg i);

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

 hence thesis by VALUED_1:def 1;

 end;

 end;

 theorem :: COMPLSP2:19



 Th15: for x1,x2 be FinSequence of COMPLEX st ( len x1) = ( len x2) holds ((x1 + x2) *' ) = ((x1 *' ) + (x2 *' ))

 proof

 let x1,x2 be FinSequence of COMPLEX ;

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

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

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

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

 assume

 A1: ( len x1) = ( len x2);

 then

 A2: ( len (x1 + x2)) = ( len x1) by Th6;



 A3: ( len x1) = ( len (x1 *' )) & ( len x2) = ( len (x2 *' )) by Def1;

 A4:

 now

 let i be Nat;



 A5: i in NAT by ORDINAL1:def 12;

 assume that

 A6: 1 <= i and

 A7: i <= ( len ((x1 + x2) *' ));



 A8: i <= ( len (x1 + x2)) by A7, Def1;



 hence (((x1 + x2) *' ) . i) = (((x1 + x2) . i) *' ) by A6, Def1

 .= (((x9 . i) + (y9 . i)) *' ) by A1, A5, Th14

 .= (((x1 . i) *' ) + ((x2 . i) *' )) by COMPLEX1: 32

 .= (((x1 *' ) . i) + ((x2 . i) *' )) by A2, A6, A8, Def1

 .= (((x1 *' ) . i) + ((x2 *' ) . i)) by A1, A2, A6, A8, Def1

 .= ((x3 + x4) . i) by A1, A3, A5, Th14;

 end;

 ( len ((x1 *' ) + (x2 *' ))) = ( len x1) by A1, A3, Th6;

 hence thesis by A4, A2, Def1;

 end;

 theorem :: COMPLSP2:20



 Th16: ((R1 - R2) . j) = ((R1 . j) - (R2 . j))

 proof

 per cases ;

 suppose

 A1: not j in ( Seg i);

 then

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



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

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



 hence ((R1 - R2) . j) = ( 0 - 0 ) by FUNCT_1:def 2

 .= ((R1 . j) - 0 ) by A3, FUNCT_1:def 2

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

 end;

 suppose j in ( Seg i);

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

 hence thesis by VALUED_1: 13;

 end;

 end;

 theorem :: COMPLSP2:21



 Th17: for x1,x2 be FinSequence of COMPLEX st ( len x1) = ( len x2) holds ((x1 - x2) *' ) = ((x1 *' ) - (x2 *' ))

 proof

 let x1,x2 be FinSequence of COMPLEX ;

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

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

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

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

 assume

 A1: ( len x1) = ( len x2);

 then

 A2: ( len (x1 - x2)) = ( len x1) by Th7;



 A3: ( len x1) = ( len (x1 *' )) & ( len x2) = ( len (x2 *' )) by Def1;

 A4:

 now

 let i be Nat;



 A5: i in NAT by ORDINAL1:def 12;

 assume that

 A6: 1 <= i and

 A7: i <= ( len ((x1 - x2) *' ));



 A8: i <= ( len (x1 - x2)) by A7, Def1;



 hence (((x1 - x2) *' ) . i) = (((x1 - x2) . i) *' ) by A6, Def1

 .= (((x9 . i) - (y9 . i)) *' ) by A1, A5, Th16

 .= (((x1 . i) *' ) - ((x2 . i) *' )) by COMPLEX1: 34

 .= (((x1 *' ) . i) - ((x2 . i) *' )) by A2, A6, A8, Def1

 .= (((x1 *' ) . i) - ((x2 *' ) . i)) by A1, A2, A6, A8, Def1

 .= ((x3 - x4) . i) by A1, A3, A5, Th16;

 end;

 ( len ((x1 *' ) - (x2 *' ))) = ( len x1) by A1, A3, Th7;

 hence thesis by A4, A2, Def1;

 end;

 theorem :: COMPLSP2:22

 for z be FinSequence of COMPLEX holds ((z *' ) *' ) = z;

 theorem :: COMPLSP2:23

 for z be FinSequence of COMPLEX holds (( - z) *' ) = ( - (z *' ))

 proof

 let z be FinSequence of COMPLEX ;



 thus (( - z) *' ) = ((( - 1r ) *' ) * (z *' )) by Th13, COMPLEX1:def 4

 .= ( - (z *' )) by COMPLEX1: 30, COMPLEX1: 33, COMPLEX1:def 4;

 end;

 theorem :: COMPLSP2:24



 Th20: for z be Complex holds (z + (z *' )) = (2 * ( Re z))

 proof

 let z be Complex;

 (z + (z *' )) = ((( Re z) + ( Re (z *' ))) + ((( Im z) + ( Im (z *' ))) * )) by COMPLEX1: 81

 .= ((( Re z) + ( Re (z *' ))) + ((( Im z) + ( - ( Im z))) * )) by COMPLEX1: 27

 .= (( Re z) + ( Re z)) by COMPLEX1: 27

 .= (2 * ( Re z));

 hence thesis;

 end;

 theorem :: COMPLSP2:25



 Th21: for x,y be complex-valued FinSequence st ( len x) = ( len y) holds ((x - y) . i) = ((x . i) - (y . i))

 proof

 let x,y be complex-valued FinSequence;



 A1: x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2;

 then

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

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

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

 assume

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

 then

 A3: ( len (x - y)) = ( len x) by Th7;

 per cases ;

 suppose

 A4: not i in ( Seg ( len x));

 then

 A5: not i in ( dom x2) by FINSEQ_2: 124;



 A6: not i in ( dom y2) by A2, A4, FINSEQ_2: 124;

 not i in ( dom y29) by A3, A4, FINSEQ_2: 124;



 then ((x2 - y2) . i) = ( 0 - 0 ) by FUNCT_1:def 2

 .= ((x2 . i) - 0 ) by A5, FUNCT_1:def 2

 .= ((x2 . i) - (y2 . i)) by A6, FUNCT_1:def 2;

 hence thesis;

 end;

 suppose i in ( Seg ( len x));

 then i in ( dom y29) by A3, FINSEQ_2: 124;

 hence thesis by VALUED_1: 13;

 end;

 end;

 theorem :: COMPLSP2:26



 Th22: for x,y be complex-valued FinSequence st ( len x) = ( len y) holds ((x + y) . i) = ((x . i) + (y . i))

 proof

 let x,y be complex-valued FinSequence;



 A1: x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2;

 then

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

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

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

 assume

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

 then

 A3: ( len (x + y)) = ( len x) by Th6;

 per cases ;

 suppose

 A4: not i in ( Seg ( len x));

 then

 A5: not i in ( dom x2) by FINSEQ_2: 124;



 A6: not i in ( dom y2) by A2, A4, FINSEQ_2: 124;

 not i in ( dom y29) by A3, A4, FINSEQ_2: 124;



 then ((x2 + y2) . i) = ( 0 + 0 ) by FUNCT_1:def 2

 .= ((x2 . i) + 0 ) by A5, FUNCT_1:def 2

 .= ((x2 . i) + (y2 . i)) by A6, FUNCT_1:def 2;

 hence thesis;

 end;

 suppose i in ( Seg ( len x));

 then i in ( dom y29) by A3, FINSEQ_2: 124;

 hence thesis by VALUED_1:def 1;

 end;

 end;

 definition

 let z be FinSequence of COMPLEX ;

 :: COMPLSP2:def2

 func Re z -> FinSequence of REAL equals ((1 / 2) * (z + (z *' )));

 coherence

 proof



 A1: ( len z) = ( len (z *' )) by Def1;



 A2: ( len ((1 / 2) * (z + (z *' )))) = ( len (z + (z *' ))) by Th3

 .= ( len z) by A1, Th6;

 ( rng ((1 / 2) * (z + (z *' )))) c= REAL

 proof

 let w be object;

 assume w in ( rng ((1 / 2) * (z + (z *' ))));

 then

 consider x be object such that

 A3: x in ( dom ((1 / 2) * (z + (z *' )))) and

 A4: w = (((1 / 2) * (z + (z *' ))) . x) by FUNCT_1:def 3;

 reconsider i = x as Element of NAT by A3;

 x in ( Seg ( len ((1 / 2) * (z + (z *' ))))) by A3, FINSEQ_1:def 3;

 then

 A5: 1 <= i & i <= ( len z) by A2, FINSEQ_1: 1;

 (((1 / 2) * (z + (z *' ))) . i) = ((1 / 2) * ((z + (z *' )) . i)) by Th12

 .= ((1 / 2) * ((z . i) + ((z *' ) . i))) by A1, Th22

 .= ((1 / 2) * ((z . i) + ((z . i) *' ))) by A5, Def1

 .= ((1 / 2) * (2 * ( Re (z . i)))) by Th20;

 hence thesis by A4;

 end;

 hence thesis by FINSEQ_1:def 4;

 end;

 end

 theorem :: COMPLSP2:27



 Th23: for z be Complex holds (z - (z *' )) = ((2 * ( Im z)) * )

 proof

 let z be Complex;

 (z - (z *' )) = ((( Re z) - ( Re (z *' ))) + ((( Im z) - ( Im (z *' ))) * )) by COMPLEX1: 84

 .= ((( Re z) - ( Re (z *' ))) + ((( Im z) - ( - ( Im z))) * )) by COMPLEX1: 27

 .= ((( Re z) - ( Re z)) + ((( Im z) - ( - ( Im z))) * )) by COMPLEX1: 27

 .= ((2 * ( Im z)) * );

 hence thesis;

 end;

 definition

 let z be FinSequence of COMPLEX ;

 :: COMPLSP2:def3

 func Im z -> FinSequence of REAL equals (( - ((1 / 2) * )) * (z - (z *' )));

 coherence

 proof



 A1: ( len z) = ( len (z *' )) by Def1;



 A2: ( len (( - ((1 / 2) * )) * (z - (z *' )))) = ( len (z - (z *' ))) by Th3

 .= ( len z) by A1, Th7;

 ( rng (( - ((1 / 2) * )) * (z - (z *' )))) c= REAL

 proof

 let w be object;

 assume w in ( rng (( - ((1 / 2) * )) * (z - (z *' ))));

 then

 consider x be object such that

 A3: x in ( dom (( - ((1 / 2) * )) * (z - (z *' )))) and

 A4: w = ((( - ((1 / 2) * )) * (z - (z *' ))) . x) by FUNCT_1:def 3;

 reconsider i = x as Element of NAT by A3;

 x in ( Seg ( len (( - ((1 / 2) * )) * (z - (z *' ))))) by A3, FINSEQ_1:def 3;

 then

 A5: 1 <= i & i <= ( len z) by A2, FINSEQ_1: 1;

 ((( - ((1 / 2) * )) * (z - (z *' ))) . i) = (( - ((1 / 2) * )) * ((z - (z *' )) . i)) by Th12

 .= (( - ((1 / 2) * )) * ((z . i) - ((z *' ) . i))) by A1, Th21

 .= (( - ((1 / 2) * )) * ((z . i) - ((z . i) *' ))) by A5, Def1

 .= (( - ((1 / 2) * )) * ((2 * ( Im (z . i))) * )) by Th23;

 hence thesis by A4;

 end;

 hence thesis by FINSEQ_1:def 4;

 end;

 end

 definition

 let x,y be FinSequence of COMPLEX ;

 :: COMPLSP2:def4

 func |(x,y)| -> Element of COMPLEX equals ((( |(( Re x), ( Re y))| - ( * |(( Re x), ( Im y))|)) + ( * |(( Im x), ( Re y))|)) + |(( Im x), ( Im y))|);

 coherence by XCMPLX_0:def 2;

 end

 theorem :: COMPLSP2:28



 Th24: for x,y,z be complex-valued FinSequence st ( len x) = ( len y) & ( len y) = ( len z) holds (x + (y + z)) = ((x + y) + z)

 proof

 let x,y,z be complex-valued FinSequence;

 reconsider x1 = x, y1 = y, z1 = z as FinSequence of COMPLEX by Lm2;

 assume

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

 reconsider z9 = z1 as Element of (( len z) -tuples_on COMPLEX ) by FINSEQ_2: 92;

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

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

 (x + (y + z)) = ( addcomplex .: (x1,(y1 + z1))) by SEQ_4:def 6

 .= ( addcomplex .: (x1,( addcomplex .: (y1,z1)))) by SEQ_4:def 6

 .= ( addcomplex .: (( addcomplex .: (x9,y9)),z9)) by A1, FINSEQOP: 28

 .= ( addcomplex .: ((x1 + y1),z1)) by SEQ_4:def 6

 .= ((x + y) + z) by SEQ_4:def 6;

 hence thesis;

 end;

 ::$Canceled

 theorem :: COMPLSP2:30



 Th25: for c be Complex, x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds (c * (x + y)) = ((c * x) + (c * y))

 proof

 let c be Complex, x,y be FinSequence of COMPLEX ;

 assume

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

 set cM = (c multcomplex );

 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: c is Element of COMPLEX by XCMPLX_0:def 2;

 (c * (x + y)) = (cM * (x + y)) by SEQ_4:def 9

 .= (cM * ( addcomplex .: (x,y))) by SEQ_4:def 6

 .= ( addcomplex .: ((cM * x9),(cM * y9))) by A1, A2, FINSEQOP: 51, SEQ_4: 56

 .= ((cM * x) + (cM * y)) by SEQ_4:def 6

 .= ((c * x) + (cM * y)) by SEQ_4:def 9

 .= ((c * x) + (c * y)) by SEQ_4:def 9;

 hence thesis;

 end;

 ::$Canceled

 theorem :: COMPLSP2:32



 Th26: for x,y be complex-valued FinSequence st ( len x) = ( len y) & (x + y) = ( 0c ( len x)) holds x = ( - y) & y = ( - x)

 proof

 let x,y be complex-valued FinSequence;

 assume that

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

 A2: (x + y) = ( 0c ( len x));

 reconsider x1 = x, y1 = y as FinSequence of COMPLEX by Lm2;

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

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



 A3: (x + y) = ( addcomplex .: (x1,y1)) & ( - y) = ( compcomplex * y1) by SEQ_4:def 6, SEQ_4:def 8;

 (x + y) = (( len x) |-> 0c ) by A2, SEQ_4:def 12;

 then x9 = ( - y9) by A1, A3, BINOP_2: 1, FINSEQOP: 74, SEQ_4: 51, SEQ_4: 52;

 hence thesis;

 end;

 theorem :: COMPLSP2:33



 Th27: for x be complex-valued FinSequence holds (x + ( 0c ( len x))) = x

 proof

 let x be complex-valued FinSequence;



 A1: x is FinSequence of COMPLEX by Lm2;

 then

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

 (x + ( 0c ( len x))) = (x + (( len x) |-> 0c )) by SEQ_4:def 12

 .= ( addcomplex .: (x,(( len x) |-> 0c ))) by A1, SEQ_4:def 6

 .= x9 by BINOP_2: 1, FINSEQOP: 56;

 hence thesis;

 end;

 theorem :: COMPLSP2:34



 Th28: for x be complex-valued FinSequence holds (x + ( - x)) = ( 0c ( len x))

 proof

 let x be complex-valued FinSequence;



 A1: x is FinSequence of COMPLEX & ( - x) is FinSequence of COMPLEX by Lm2;

 then

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

 (x + ( - x)) = ( addcomplex .: (x,( - x))) by A1, SEQ_4:def 6

 .= ( addcomplex .: (x,( compcomplex * x))) by A1, SEQ_4:def 8

 .= (( len x9) |-> 0c ) by BINOP_2: 1, FINSEQOP: 73, SEQ_4: 51, SEQ_4: 52

 .= ( 0c ( len x9)) by SEQ_4:def 12;

 hence thesis;

 end;

 theorem :: COMPLSP2:35



 Th29: for x,y be complex-valued FinSequence st ( len x) = ( len y) holds ( - (x + y)) = (( - x) + ( - y))

 proof

 let x,y be complex-valued FinSequence;

 assume

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



 A2: ( len ( - y)) = ( len y) by Th5;

 then

 A3: ( len (( - x) + ( - y))) = ( len ( - x)) by A1, Th5, Th6;



 A4: ( len ( - x)) = ( len x) by Th5;



 A5: ( len (x + y)) = ( len x) by A1, Th6;



 then ((x + y) + (( - x) + ( - y))) = (((y + x) + ( - x)) + ( - y)) by A1, A2, A4, Th24

 .= ((y + (x + ( - x))) + ( - y)) by A1, A4, Th24

 .= ((y + ( 0c ( len x))) + ( - y)) by Th28

 .= (y + ( - y)) by A1, Th27

 .= ( 0c ( len y)) by Th28;

 hence thesis by A1, A4, A5, A3, Th26;

 end;

 theorem :: COMPLSP2:36



 Th30: for x,y,z be complex-valued FinSequence st ( len x) = ( len y) & ( len y) = ( len z) holds ((x - y) - z) = (x - (y + z))

 proof

 let x,y,z be complex-valued FinSequence;

 assume that

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

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

 ( len ( - y)) = ( len y) & ( len ( - z)) = ( len z) by Th5;



 then ((x - y) - z) = (x + (( - y) + ( - z))) by A1, A2, Th24

 .= (x - (y + z)) by A2, Th29;

 hence thesis;

 end;

 theorem :: COMPLSP2:37



 Th31: for x,y,z be complex-valued FinSequence st ( len x) = ( len y) & ( len y) = ( len z) holds (x + (y - z)) = ((x + y) - z)

 proof

 let x,y,z be complex-valued FinSequence;

 assume

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

 ( len ( - z)) = ( len z) by Th5;

 hence thesis by A1, Th24;

 end;

 ::$Canceled

 theorem :: COMPLSP2:39



 Th32: for x,y be complex-valued FinSequence st ( len x) = ( len y) holds ( - (x - y)) = (( - x) + y)

 proof

 let x,y be complex-valued FinSequence;

 assume

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

 ( len ( - y)) = ( len y) by Th5;



 then ( - (x - y)) = (( - x) + ( - ( - y))) by A1, Th29

 .= (( - x) + y);

 hence thesis;

 end;

 theorem :: COMPLSP2:40



 Th33: for x,y,z be complex-valued FinSequence st ( len x) = ( len y) & ( len y) = ( len z) holds (x - (y - z)) = ((x - y) + z)

 proof

 let x,y,z be complex-valued FinSequence;

 assume that

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

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



 A3: ( len ( - y)) = ( len y) by Th5;

 (x - (y - z)) = (x + (( - y) + z)) by A2, Th32

 .= ((x - y) + z) by A1, A2, A3, Th24;

 hence thesis;

 end;

 theorem :: COMPLSP2:41



 Th34: for c be Complex holds (c * ( 0c ( len x))) = ( 0c ( len x))

 proof

 let c be Complex;

 reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;



 A1: ( rng ( 0c ( len x))) c= COMPLEX by FINSEQ_1:def 4;

 (c * ( 0c ( len x))) = (( multcomplex [;] (cc,( id COMPLEX ))) * ( 0c ( len x))) by Lm1

 .= ( multcomplex [;] (cc,(( id COMPLEX ) * ( 0c ( len x))))) by FUNCOP_1: 34

 .= ( multcomplex [;] (cc,( 0c ( len x)))) by A1, RELAT_1: 53

 .= ( multcomplex [;] (cc,(( len x) |-> 0c ))) by SEQ_4:def 12

 .= (( len x) |-> ( multcomplex . (cc, 0c ))) by FINSEQOP: 18

 .= (( len x) |-> (cc * 0c )) by BINOP_2:def 5

 .= ( 0c ( len x)) by SEQ_4:def 12;

 hence thesis;

 end;

 theorem :: COMPLSP2:42



 Th35: for c be Complex holds ( - (c * x)) = (c * ( - x))

 proof

 let c be Complex;



 A1: ( len (c * ( - x))) = ( len ( - x)) & ( len (c * x)) = ( len x) by Th3;



 A2: ( len x) = ( len ( - x)) by Th5;



 then ((c * ( - x)) + (c * x)) = (c * (x + ( - x))) by Th25

 .= (c * ( 0c ( len x))) by Th28

 .= ( 0c ( len x)) by Th34;

 hence thesis by A2, A1, Th26;

 end;

 theorem :: COMPLSP2:43



 Th36: for c be Complex, x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds (c * (x - y)) = ((c * x) - (c * y))

 proof

 let c be Complex, x,y be FinSequence of COMPLEX ;

 assume

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

 reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;

 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;

 set cM = (cc multcomplex );

 (c * (x - y)) = (cM * (x + ( - y))) by SEQ_4:def 9

 .= (cM * ( addcomplex .: (x,( - y)))) by SEQ_4:def 6

 .= ( addcomplex .: ((cM * x9),(cM * ( - y9)))) by A1, FINSEQOP: 51, SEQ_4: 56

 .= ((cM * x) + (cM * ( - y))) by SEQ_4:def 6

 .= ((c * x) + (cM * ( - y))) by SEQ_4:def 9

 .= ((c * x) + (c * ( - y))) by SEQ_4:def 9

 .= ((c * x) - (c * y)) by Th35;

 hence thesis;

 end;

 theorem :: COMPLSP2:44

 for x1,y1 be Element of COMPLEX holds for x2,y2 be Real st x1 = x2 & y1 = y2 holds ( addcomplex . (x1,y1)) = ( addreal . (x2,y2))

 proof

 let x1,y1 be Element of COMPLEX ;

 let x2,y2 be Real;



 A1: ( addcomplex . (x1,y1)) = (x1 + y1) by BINOP_2:def 3;

 assume x1 = x2 & y1 = y2;

 hence thesis by A1, BINOP_2:def 9;

 end;

 reserve C for Function of [: COMPLEX , COMPLEX :], COMPLEX ;

 reserve G for Function of [: REAL , REAL :], REAL ;

 theorem :: COMPLSP2:45



 Th38: for x1,y1 be FinSequence of COMPLEX holds for x2,y2 be FinSequence of REAL st x1 = x2 & y1 = y2 & ( len x1) = ( len y2) & (for i st i in ( dom x1) holds (C . ((x1 . i),(y1 . i))) = (G . ((x2 . i),(y2 . i)))) holds (C .: (x1,y1)) = (G .: (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) and

 A4: for i st i in ( dom x1) holds (C . ((x1 . i),(y1 . i))) = (G . ((x2 . i),(y2 . i)));



 A5: ( len (G .: (x2,y2))) = ( len x1) by A1, A3, FINSEQ_2: 72;

 now

 let i be Nat;

 assume that

 A6: 1 <= i and

 A7: i <= ( len (C .: (x1,y1)));



 A8: i <= ( len x1) by A2, A3, A7, FINSEQ_2: 72;

 then

 A9: i in ( dom x1) by A6, FINSEQ_3: 25;



 A10: i in ( dom (G .: (x2,y2))) by A5, A6, A8, FINSEQ_3: 25;

 i in ( dom (C .: (x1,y1))) by A6, A7, FINSEQ_3: 25;



 hence ((C .: (x1,y1)) . i) = (C . ((x1 . i),(y1 . i))) by FUNCOP_1: 22

 .= (G . ((x2 . i),(y2 . i))) by A4, A9

 .= ((G .: (x2,y2)) . i) by A10, FUNCOP_1: 22;

 end;

 hence thesis by A5, A2, A3, FINSEQ_2: 72;

 end;

 theorem :: COMPLSP2:46

 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 ( addcomplex .: (x1,y1)) = ( addreal .: (x2,y2))

 proof

 let x1,y1 be FinSequence of COMPLEX ;

 let x2,y2 be FinSequence of REAL ;

 assume that

 A1: x1 = x2 & y1 = y2 and

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

 for i st i in ( dom x1) holds ( addcomplex . ((x1 . i),(y1 . i))) = ( addreal . ((x2 . i),(y2 . i)))

 proof

 let i;

 ((x1 . i) + (y1 . i)) = ( addcomplex . ((x1 . i),(y1 . i))) by BINOP_2:def 3;

 hence thesis by A1, BINOP_2:def 9;

 end;

 hence thesis by A1, A2, Th38;

 end;

 ::$Canceled

 theorem :: COMPLSP2:48



 Th40: for x be FinSequence of COMPLEX holds ( len ( Re x)) = ( len x) & ( len ( Im x)) = ( len x)

 proof

 let x be FinSequence of COMPLEX ;



 A1: ( len x) = ( len (x *' )) by Def1;



 A2: ( len ( Im x)) = ( len (x - (x *' ))) by Th3

 .= ( len x) by A1, Th7;

 ( len ( Re x)) = ( len (x + (x *' ))) by Th3

 .= ( len x) by A1, Th6;

 hence thesis by A2;

 end;

 theorem :: COMPLSP2:49



 Th41: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds ( Re (x + y)) = (( Re x) + ( Re y)) & ( Im (x + y)) = (( Im x) + ( Im y))

 proof

 let x,y be FinSequence of COMPLEX ;



 A1: ( len ( - (x *' ))) = ( len (x *' )) by Th5;

 assume

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

 then

 A3: ( len (x + y)) = ( len x) by Th6;



 A4: ( len y) = ( len (y *' )) by Def1;

 then

 A5: ( len (y + (y *' ))) = ( len y) by Th6;



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

 then

 A7: ( len (x + (x *' ))) = ( len x) by Th6;



 A8: ( len (x - (x *' ))) = ( len x) by A6, Th7;



 A9: ( len (y - (y *' ))) = ( len y) by A4, Th7;



 thus ( Re (x + y)) = ((1 / 2) * ((x + y) + ((x *' ) + (y *' )))) by A2, Th15

 .= ((1 / 2) * (((x + y) + (x *' )) + (y *' ))) by A2, A4, A6, A3, Th24

 .= ((1 / 2) * (((x + (x *' )) + y) + (y *' ))) by A2, A6, Th24

 .= ((1 / 2) * ((x + (x *' )) + (y + (y *' )))) by A2, A4, A7, Th24

 .= (( Re x) + ( Re y)) by A2, A7, A5, Th25;



 thus ( Im (x + y)) = (( - ((1 / 2) * )) * ((x + y) - ((x *' ) + (y *' )))) by A2, Th15

 .= (( - ((1 / 2) * )) * (((x + y) - (x *' )) - (y *' ))) by A2, A4, A6, A3, Th30

 .= (( - ((1 / 2) * )) * (((x + ( - (x *' ))) + y) - (y *' ))) by A2, A6, A1, Th24

 .= (( - ((1 / 2) * )) * ((x - (x *' )) + (y - (y *' )))) by A2, A4, A8, Th31

 .= (( Im x) + ( Im y)) by A2, A8, A9, Th25;

 end;

 theorem :: COMPLSP2:50

 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 ( diffcomplex .: (x1,y1)) = ( diffreal .: (x2,y2))

 proof

 let x1,y1 be FinSequence of COMPLEX , x2,y2 be FinSequence of REAL ;

 assume that

 A1: x1 = x2 & y1 = y2 and

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

 for i st i in ( dom x1) holds ( diffcomplex . ((x1 . i),(y1 . i))) = ( diffreal . ((x2 . i),(y2 . i)))

 proof

 let i;

 ((x1 . i) - (y1 . i)) = ( diffcomplex . ((x1 . i),(y1 . i))) by BINOP_2:def 4;

 hence thesis by A1, BINOP_2:def 10;

 end;

 hence thesis by A1, A2, Th38;

 end;

 ::$Canceled

 theorem :: COMPLSP2:52



 Th43: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds ( Re (x - y)) = (( Re x) - ( Re y)) & ( Im (x - y)) = (( Im x) - ( Im y))

 proof

 let x,y be FinSequence of COMPLEX ;

 assume

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

 then

 A2: ( len (x - y)) = ( len x) by Th7;



 A3: ( len x) = ( len (x *' )) by Def1;

 then

 A4: ( len (x + (x *' ))) = ( len x) by Th6;



 A5: ( len y) = ( len (y *' )) by Def1;

 then

 A6: ( len (y + (y *' ))) = ( len y) by Th6;



 thus ( Re (x - y)) = ((1 / 2) * ((x - y) + ((x *' ) - (y *' )))) by A1, Th17

 .= ((1 / 2) * (((x *' ) + (x - y)) - (y *' ))) by A1, A5, A3, A2, Th31

 .= ((1 / 2) * ((x *' ) + ((x - y) - (y *' )))) by A1, A5, A3, A2, Th31

 .= ((1 / 2) * ((x *' ) + (x - (y + (y *' ))))) by A1, A5, Th30

 .= ((1 / 2) * ((x + (x *' )) - (y + (y *' )))) by A1, A3, A6, Th31

 .= (( Re x) - ( Re y)) by A1, A4, A6, Th36;



 A7: ( len (x - (x *' ))) = ( len x) by A3, Th7;



 A8: ( len (y - (y *' ))) = ( len y) by A5, Th7;



 thus ( Im (x - y)) = (( - ((1 / 2) * )) * ((x - y) - ((x *' ) - (y *' )))) by A1, Th17

 .= (( - ((1 / 2) * )) * (((x - y) - (x *' )) + (y *' ))) by A1, A5, A3, A2, Th33

 .= (( - ((1 / 2) * )) * ((x - ((x *' ) + y)) + (y *' ))) by A1, A3, Th30

 .= (( - ((1 / 2) * )) * (((x - (x *' )) - y) + (y *' ))) by A1, A3, Th30

 .= (( - ((1 / 2) * )) * ((x - (x *' )) - (y - (y *' )))) by A1, A5, A7, Th33

 .= (( Im x) - ( Im y)) by A1, A7, A8, Th36;

 end;

 theorem :: COMPLSP2:53



 Th44: for a,b be Complex holds (a * (b * z)) = ((a * b) * z)

 proof

 let a,b be Complex;

 reconsider aa = a, bb = b, ab = (a * b) as Element of COMPLEX by XCMPLX_0:def 2;



 thus ((a * b) * z) = (( multcomplex [;] (ab,( id COMPLEX ))) * z) by Lm1

 .= (( multcomplex [;] (( multcomplex . (aa,bb)),( id COMPLEX ))) * z) by BINOP_2:def 5

 .= (( multcomplex [;] (aa,( multcomplex [;] (bb,( id COMPLEX ))))) * z) by FUNCOP_1: 62

 .= ((( multcomplex [;] (aa,( id COMPLEX ))) * ( multcomplex [;] (bb,( id COMPLEX )))) * z) by FUNCOP_1: 55

 .= (( multcomplex [;] (aa,( id COMPLEX ))) * (( multcomplex [;] (bb,( id COMPLEX ))) * z)) by RELAT_1: 36

 .= (( multcomplex [;] (aa,( id COMPLEX ))) * (b * z)) by Lm1

 .= (a * (b * z)) by Lm1;

 end;



 Lm3: ( - ( 0c ( len x))) = ( 0c ( len x))

 proof

 ( - ( 0c ( len x))) = ( - (( len x) |-> 0c )) by SEQ_4:def 12

 .= ( compcomplex * (( len x) |-> 0c )) by SEQ_4:def 8

 .= (( len x) |-> ( compcomplex . 0c )) by FINSEQOP: 16

 .= (( len x) |-> ( - 0c )) by BINOP_2:def 1

 .= ( 0c ( len x)) by SEQ_4:def 12;

 hence thesis;

 end;

 theorem :: COMPLSP2:54



 Th45: for c be Complex holds (( - c) * x) = ( - (c * x))

 proof

 let c be Complex;



 A1: ( len (( - c) * x)) = ( len x) by Th3;



 A2: ( len (c * x)) = ( len x) by Th3;

 ((( - c) * x) + (c * x)) = (((( - 1) * c) * x) + (c * x))

 .= (( - (c * x)) + (c * x)) by Th44

 .= ( - ((c * x) - (c * x))) by A2, Th32

 .= ( - ( 0c ( len x))) by A2, Th28

 .= ( 0c ( len x)) by Lm3;

 hence thesis by A1, A2, Th26;

 end;

 reserve h for Function of COMPLEX , COMPLEX ,

g for Function of REAL , REAL ;

 theorem :: COMPLSP2:55



 Th46: for y1 be FinSequence of COMPLEX holds for y2 be FinSequence of REAL st ( len y1) = ( len y2) & (for i st i in ( dom y1) holds (h . (y1 . i)) = (g . (y2 . i))) holds (h * y1) = (g * y2)

 proof

 let y1 be FinSequence of COMPLEX ;

 let y2 be FinSequence of REAL ;

 assume that

 A1: ( len y1) = ( len y2) and

 A2: for i st i in ( dom y1) holds (h . (y1 . i)) = (g . (y2 . i));



 A3: ( len (g * y2)) = ( len y1) by A1, FINSEQ_2: 33;

 now

 let i be Nat;

 assume that

 A4: 1 <= i and

 A5: i <= ( len (h * y1));



 A6: i <= ( len y1) by A5, FINSEQ_2: 33;

 then

 A7: i in ( dom y1) by A4, FINSEQ_3: 25;



 A8: i in ( dom (g * y2)) by A3, A4, A6, FINSEQ_3: 25;

 i in ( dom (h * y1)) by A4, A5, FINSEQ_3: 25;



 hence ((h * y1) . i) = (h . (y1 . i)) by FUNCT_1: 12

 .= (g . (y2 . i)) by A2, A7

 .= ((g * y2) . i) by A8, FUNCT_1: 12;

 end;

 hence thesis by A3, FINSEQ_2: 33;

 end;

 theorem :: COMPLSP2:56

 for y1 be FinSequence of COMPLEX holds for y2 be FinSequence of REAL st y1 = y2 & ( len y1) = ( len y2) holds ( compcomplex * y1) = ( compreal * y2)

 proof

 let y1 be FinSequence of COMPLEX ;

 let y2 be FinSequence of REAL ;

 assume that

 A1: y1 = y2 and

 A2: ( len y1) = ( len y2);

 for i st i in ( dom y1) holds ( compcomplex . (y1 . i)) = ( compreal . (y2 . i))

 proof

 let i;

 assume i in ( dom y1);

 ( - (y1 . i)) = ( compcomplex . (y1 . i)) by BINOP_2:def 1;

 hence thesis by A1, BINOP_2:def 7;

 end;

 hence thesis by A2, Th46;

 end;

 ::$Canceled

 theorem :: COMPLSP2:58



 Th48: for x be FinSequence of COMPLEX holds ( Re ( * x)) = ( - ( Im x)) & ( Im ( * x)) = ( Re x)

 proof

 let x be FinSequence of COMPLEX ;



 A1: ( len (x *' )) = ( len x) by Def1;



 A2: ( Im ( * x)) = ((( - (1 / 2)) * ) * (( * x) - (( - ) * (x *' )))) by Th13, COMPLEX1: 31

 .= ((( - (1 / 2)) * ) * (( * x) + ( - ( - ( * (x *' )))))) by Th45

 .= ((( - (1 / 2)) * ) * ( * (x + (x *' )))) by A1, Th25

 .= (((( - (1 / 2)) * ) * ) * (x + (x *' ))) by Th44

 .= ( Re x);

 ( Re ( * x)) = ((1 / 2) * (( * x) + (( - ) * (x *' )))) by Th13, COMPLEX1: 31

 .= ((1 / 2) * (( * x) - ( * (x *' )))) by Th45

 .= ((1 / 2) * ( * (x - (x *' )))) by A1, Th36

 .= (((1 / 2) * ) * (x - (x *' ))) by Th44

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

 .= ( - ( Im x)) by Th44;

 hence thesis by A2;

 end;

 theorem :: COMPLSP2:59



 Th49: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |(( * x), y)| = ( * |(x, y)|)

 proof

 let x,y be FinSequence of COMPLEX ;

 assume

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



 A2: ( len ( Im y)) = ( len y) by Th40;



 A3: ( len ( Re y)) = ( len y) by Th40;



 A4: ( len ( Im x)) = ( len x) by Th40;

 |(( * x), y)| = ((( |(( - ( Im x)), ( Re y))| - ( * |(( Re ( * x)), ( Im y))|)) + ( * |(( Im ( * x)), ( Re y))|)) + |(( Im ( * x)), ( Im y))|) by Th48

 .= ((( |(( - ( Im x)), ( Re y))| - ( * |(( - ( Im x)), ( Im y))|)) + ( * |(( Im ( * x)), ( Re y))|)) + |(( Im ( * x)), ( Im y))|) by Th48

 .= ((( |(( - ( Im x)), ( Re y))| - ( * |(( - ( Im x)), ( Im y))|)) + ( * |(( Re x), ( Re y))|)) + |(( Im ( * x)), ( Im y))|) by Th48

 .= ((( |(( - ( Im x)), ( Re y))| - ( * |(( - ( Im x)), ( Im y))|)) + ( * |(( Re x), ( Re y))|)) + |(( Re x), ( Im y))|) by Th48

 .= (((( - |(( Im x), ( Re y))|) - ( * |(( - ( Im x)), ( Im y))|)) + ( * |(( Re x), ( Re y))|)) + |(( Re x), ( Im y))|) by A1, A3, A4, RVSUM_1: 122

 .= (((( - |(( Im x), ( Re y))|) - ( * ( - |(( Im x), ( Im y))|))) + ( * |(( Re x), ( Re y))|)) + |(( Re x), ( Im y))|) by A1, A4, A2, RVSUM_1: 122

 .= ( * |(x, y)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:60



 Th50: for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |(x, ( * y))| = ( - ( * |(x, y)|))

 proof

 let x,y be FinSequence of COMPLEX ;

 assume

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



 A2: ( len ( Im x)) = ( len x) by Th40;



 A3: ( len ( Re x)) = ( len x) by Th40;



 A4: ( len ( Im y)) = ( len y) by Th40;

 |(x, ( * y))| = ((( |(( Re x), ( - ( Im y)))| - ( * |(( Re x), ( Im ( * y)))|)) + ( * |(( Im x), ( Re ( * y)))|)) + |(( Im x), ( Im ( * y)))|) by Th48

 .= ((( |(( Re x), ( - ( Im y)))| - ( * |(( Re x), ( Re y))|)) + ( * |(( Im x), ( Re ( * y)))|)) + |(( Im x), ( Im ( * y)))|) by Th48

 .= ((( |(( Re x), ( - ( Im y)))| - ( * |(( Re x), ( Re y))|)) + ( * |(( Im x), ( - ( Im y)))|)) + |(( Im x), ( Im ( * y)))|) by Th48

 .= ((( |(( Re x), ( - ( Im y)))| - ( * |(( Re x), ( Re y))|)) + ( * |(( Im x), ( - ( Im y)))|)) + |(( Im x), ( Re y))|) by Th48

 .= (((( - |(( Re x), ( Im y))|) - ( * |(( Re x), ( Re y))|)) + ( * |(( Im x), ( - ( Im y)))|)) + |(( Im x), ( Re y))|) by A1, A3, A4, RVSUM_1: 122

 .= (((( - |(( Re x), ( Im y))|) - ( * |(( Re x), ( Re y))|)) + ( * ( - |(( Im x), ( Im y))|))) + |(( Im x), ( Re y))|) by A1, A2, A4, RVSUM_1: 122

 .= ( - ( * |(x, y)|));

 hence thesis;

 end;

 theorem :: COMPLSP2:61

 for a1 be Element of COMPLEX , y1 be FinSequence of COMPLEX holds for a2 be Element of REAL , y2 be FinSequence of REAL st a1 = a2 & y1 = y2 & ( len y1) = ( len y2) holds ((a1 multcomplex ) * y1) = ((a2 multreal ) * y2)

 proof

 let a1 be Element of COMPLEX , y1 be FinSequence of COMPLEX ;

 let a2 be Element of REAL , y2 be FinSequence of REAL ;

 assume that

 A1: a1 = a2 & y1 = y2 and

 A2: ( len y1) = ( len y2);

 for i st i in ( dom y1) holds ((a1 multcomplex ) . (y1 . i)) = ((a2 multreal ) . (y2 . i))

 proof

 let i;

 reconsider y2i = (y2 . i) as Element of REAL by XREAL_0:def 1;

 assume i in ( dom y1);



 A3: ((a2 * y2) . i) = (a2 * (y2 . i)) by RVSUM_1: 44

 .= ( multreal . (a2,(( id REAL ) . y2i))) by BINOP_2:def 11

 .= (( multreal [;] (a2,( id REAL ))) . y2i) by FUNCOP_1: 53

 .= ((a2 multreal ) . (y2 . i)) by RVSUM_1:def 3;

 ((a1 * y1) . i) = (a1 * (y1 . i)) by Th12

 .= ( multcomplex . (a1,(( id COMPLEX ) . (y1 . i)))) by BINOP_2:def 5

 .= (( multcomplex [;] (a1,( id COMPLEX ))) . (y1 . i)) by FUNCOP_1: 53

 .= ((a1 multcomplex ) . (y1 . i)) by SEQ_4:def 4;

 hence thesis by A1, A3;

 end;

 hence thesis by A2, Th46;

 end;

 ::$Canceled

 theorem :: COMPLSP2:63



 Th52: for a,b be Complex holds ((a + b) * z) = ((a * z) + (b * z))

 proof

 let a,b be Complex;

 reconsider aa = a, bb = b, ab = (a + b) as Element of COMPLEX by XCMPLX_0:def 2;

 set c1M = ( multcomplex [;] (aa,( id COMPLEX ))), c2M = ( multcomplex [;] (bb,( id COMPLEX )));



 thus ((a + b) * z) = (( multcomplex [;] (ab,( id COMPLEX ))) * z) by Lm1

 .= (( multcomplex [;] (( addcomplex . (aa,bb)),( id COMPLEX ))) * z) by BINOP_2:def 3

 .= (( addcomplex .: (c1M,c2M)) * z) by FINSEQOP: 35, SEQ_4: 54

 .= ( addcomplex .: ((c1M * z),(c2M * z))) by FUNCOP_1: 25

 .= ((c1M * z) + (c2M * z)) by SEQ_4:def 6

 .= ((a * z) + (c2M * z)) by Lm1

 .= ((a * z) + (b * z)) by Lm1;

 end;

 theorem :: COMPLSP2:64



 Th53: for a,b be Complex holds ((a - b) * z) = ((a * z) - (b * z))

 proof

 let a,b be Complex;

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

 ((a - b) * z) = ((a + ( - b)) * z)

 .= ((aa * z) + (( - bb) * z)) by Th52

 .= ((a * z) - (b * z)) by Th45;

 hence thesis;

 end;

 theorem :: COMPLSP2:65



 Th54: for a be Element of COMPLEX , x be FinSequence of COMPLEX holds ( Re (a * x)) = ((( Re a) * ( Re x)) - (( Im a) * ( Im x))) & ( Im (a * x)) = ((( Im a) * ( Re x)) + (( Re a) * ( Im x)))

 proof

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

 reconsider z5 = ( Re a), z6 = ( Im a) as Element of COMPLEX by XCMPLX_0:def 2;



 A1: ( len (x *' )) = ( len x) by Def1;

 ( len (((1 / 2) * z5) * x)) = ( len x) by Th3;

 then

 A2: ( len (((((1 / 2) * ) * z6) * x) + (((1 / 2) * z5) * x))) = ( len ((((1 / 2) * ) * z6) * x)) by Th3, Th6;



 A3: ( len (((1 / 2) * z5) * x)) = ( len x) by Th3;



 A4: ( len (z5 * x)) = ( len x) & ( len (( * z6) * x)) = ( len x) by Th3;



 A5: (( Re a) * ( Re x)) = ((z5 * (1 / 2)) * (x + (x *' ))) by Th44

 .= ((((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *' ))) by A1, Th25;



 A6: ( len ( Re x)) = ( len x) & ( len (( Re a) * ( Re x))) = ( len ( Re x)) by Th40, RVSUM_1: 117;



 A7: ( len ((z5 - (z6 * )) * (x *' ))) = ( len (x *' )) & ( len ((z5 + ( * z6)) * x)) = ( len x) by Th3;



 A8: ( len ((( - ((1 / 2) * )) * z6) * (x *' ))) = ( len (x *' )) by Th3;



 A9: (( Im a) * ( Im x)) = ((z6 * ( - ((1 / 2) * ))) * (x - (x *' ))) by Th44

 .= (((( - ((1 / 2) * )) * z6) * x) - ((( - ((1 / 2) * )) * z6) * (x *' ))) by A1, Th36;



 A10: ( len ((( - ((1 / 2) * )) * z6) * x)) = ( len x) by Th3;



 A11: ( len (z5 * (x *' ))) = ( len (x *' )) & ( len ((z6 * ) * (x *' ))) = ( len (x *' )) by Th3;



 A12: ( len (((1 / 2) * z5) * (x *' ))) = ( len (x *' )) & ( len ((((1 / 2) * ) * z6) * x)) = ( len x) by Th3;



 A13: ( Re (a * x)) = ((1 / 2) * (((a *' ) * (x *' )) + (a * x))) by Th13

 .= ((1 / 2) * (((a *' ) * (x *' )) + ((z5 + ( * z6)) * x))) by COMPLEX1: 13

 .= ((1 / 2) * (((z5 - (z6 * )) * (x *' )) + ((z5 + ( * z6)) * x))) by COMPLEX1:def 11

 .= (((1 / 2) * ((z5 - (z6 * )) * (x *' ))) + ((1 / 2) * ((z5 + ( * z6)) * x))) by A7, Th25, Def1

 .= (((1 / 2) * ((z5 - (z6 * )) * (x *' ))) + ((1 / 2) * ((z5 * x) + (( * z6) * x)))) by Th52

 .= (((1 / 2) * ((z5 * (x *' )) - ((z6 * ) * (x *' )))) + ((1 / 2) * ((z5 * x) + (( * z6) * x)))) by Th53

 .= (((1 / 2) * ((z5 * (x *' )) - ((z6 * ) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * (( * z6) * x)))) by A4, Th25

 .= ((((1 / 2) * (z5 * (x *' ))) - ((1 / 2) * ((z6 * ) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * (( * z6) * x)))) by A11, Th36

 .= ((((1 / 2) * (z5 * (x *' ))) - ((1 / 2) * (( * z6) * (x *' )))) + (((1 / 2) * (z5 * x)) + (((1 / 2) * ( * z6)) * x))) by Th44

 .= ((((1 / 2) * (z5 * (x *' ))) + ( - ((((1 / 2) * ) * z6) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * ) * z6) * x))) by Th44

 .= ((((1 / 2) * (z5 * (x *' ))) + (( - (((1 / 2) * ) * z6)) * (x *' ))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * ) * z6) * x))) by Th45

 .= (((((1 / 2) * z5) * (x *' )) + ((( - ((1 / 2) * )) * z6) * (x *' ))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * ) * z6) * x))) by Th44

 .= (((((1 / 2) * z5) * x) + ((((1 / 2) * ) * z6) * x)) + ((((1 / 2) * z5) * (x *' )) + ((( - ((1 / 2) * )) * z6) * (x *' )))) by Th44

 .= (((((((1 / 2) * ) * z6) * x) + (((1 / 2) * z5) * x)) + (((1 / 2) * z5) * (x *' ))) + ((( - ((1 / 2) * )) * z6) * (x *' ))) by A1, A8, A12, A2, Th24

 .= ((((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *' ))) + (( - (( - ((1 / 2) * )) * z6)) * x)) + ((( - ((1 / 2) * )) * z6) * (x *' ))) by A1, A3, A12, Th24

 .= ((((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *' ))) - ((( - ((1 / 2) * )) * z6) * x)) + ((( - ((1 / 2) * )) * z6) * (x *' ))) by Th45

 .= ((( Re a) * ( Re x)) - (( Im a) * ( Im x))) by A1, A5, A9, A6, A10, A8, Th33;



 A14: ( len ((((1 / 2) * ) * z5) * (x *' ))) = ( len (x *' )) by Th3;



 A15: (( Im a) * ( Re x)) = ((z6 * (1 / 2)) * (x + (x *' ))) by Th44

 .= ((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *' ))) by A1, Th25;



 A16: ( len (( * z6) * (x *' ))) = ( len (x *' )) & ( len (( - z5) * (x *' ))) = ( len (x *' )) by Th3;



 A17: ( len ((1 / 2) * (z6 * x))) = ( len (z6 * x)) by Th3;



 A18: ( len (z6 * (x *' ))) = ( len (x *' )) & ( len ((1 / 2) * (z6 * (x *' )))) = ( len (z6 * (x *' ))) by Th3;

 then

 A19: ( len (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' ))))) = ( len ((1 / 2) * (z6 * x))) by A1, A17, Th3, Th6;



 A20: ( len ((( - ((1 / 2) * )) * z5) * x)) = ( len x) by Th3;

 then

 A21: ( len (((1 / 2) * (z6 * x)) + ((( - ((1 / 2) * )) * z5) * x))) = ( len ((1 / 2) * (z6 * x))) by A17, Th3, Th6;



 A22: (( Re a) * ( Im x)) = ((z5 * ( - ((1 / 2) * ))) * (x - (x *' ))) by Th44

 .= (((( - ((1 / 2) * )) * z5) * x) - ((( - ((1 / 2) * )) * z5) * (x *' ))) by A1, Th36;



 A23: ( len (z6 * x)) = ( len x) by Th3;

 ( len ((a * x) *' )) = ( len (a * x)) & ( len ( - ((a * x) *' ))) = ( len ((a * x) *' )) by Def1, Th5;



 then ( Im (a * x)) = ((( - ((1 / 2) * )) * ( - ((a * x) *' ))) + (( - ((1 / 2) * )) * (a * x))) by Th25

 .= ((( - ((1 / 2) * )) * ( - ((a *' ) * (x *' )))) + (( - ((1 / 2) * )) * (a * x))) by Th13

 .= ((( - ((1 / 2) * )) * ( - ((a *' ) * (x *' )))) + (( - ((1 / 2) * )) * ((z5 + ( * z6)) * x))) by COMPLEX1: 13

 .= ((( - ((1 / 2) * )) * ( - ((z5 - (z6 * )) * (x *' )))) + (( - ((1 / 2) * )) * ((z5 + ( * z6)) * x))) by COMPLEX1:def 11

 .= ((( - ((1 / 2) * )) * (( - (z5 - (z6 * ))) * (x *' ))) + (( - ((1 / 2) * )) * ((z5 + ( * z6)) * x))) by Th45

 .= ((( - ((1 / 2) * )) * ((( - z5) + (z6 * )) * (x *' ))) + (( - ((1 / 2) * )) * ((z5 + ( * z6)) * x)))

 .= ((( - ((1 / 2) * )) * ((( - z5) * (x *' )) + (( * z6) * (x *' )))) + (( - ((1 / 2) * )) * ((z5 + ( * z6)) * x))) by Th52

 .= ((( - ((1 / 2) * )) * ((( - z5) * (x *' )) + (( * z6) * (x *' )))) + (( - ((1 / 2) * )) * ((z5 * x) + (( * z6) * x)))) by Th52

 .= ((( - ((1 / 2) * )) * ((( - z5) * (x *' )) + (( * z6) * (x *' )))) + ((( - ((1 / 2) * )) * (z5 * x)) + (( - ((1 / 2) * )) * (( * z6) * x)))) by A4, Th25

 .= (((( - ((1 / 2) * )) * (( - z5) * (x *' ))) + (( - ((1 / 2) * )) * (( * z6) * (x *' )))) + ((( - ((1 / 2) * )) * (z5 * x)) + (( - ((1 / 2) * )) * (( * z6) * x)))) by A16, Th25

 .= ((((( - ((1 / 2) * )) * ( - z5)) * (x *' )) + (( - ((1 / 2) * )) * (( * z6) * (x *' )))) + ((( - ((1 / 2) * )) * (z5 * x)) + (( - ((1 / 2) * )) * (( * z6) * x)))) by Th44

 .= ((((( - ((1 / 2) * )) * ( - z5)) * (x *' )) + (( - ((1 / 2) * )) * ( * (z6 * (x *' ))))) + ((( - ((1 / 2) * )) * (z5 * x)) + (( - ((1 / 2) * )) * (( * z6) * x)))) by Th44

 .= ((((( - ((1 / 2) * )) * ( - z5)) * (x *' )) + ((( - ((1 / 2) * )) * ) * (z6 * (x *' )))) + ((( - ((1 / 2) * )) * (z5 * x)) + (( - ((1 / 2) * )) * (( * z6) * x)))) by Th44

 .= ((((( - ((1 / 2) * )) * ( - z5)) * (x *' )) + ((( - ((1 / 2) * )) * ) * (z6 * (x *' )))) + (((( - ((1 / 2) * )) * z5) * x) + (( - ((1 / 2) * )) * (( * z6) * x)))) by Th44

 .= ((((( - ((1 / 2) * )) * ( - z5)) * (x *' )) + ((( - ((1 / 2) * )) * ) * (z6 * (x *' )))) + (((( - ((1 / 2) * )) * z5) * x) + (( - ((1 / 2) * )) * ( * (z6 * x))))) by Th44

 .= ((((1 / 2) * (z6 * x)) + ((( - ((1 / 2) * )) * z5) * x)) + (((1 / 2) * (z6 * (x *' ))) + ((((1 / 2) * ) * z5) * (x *' )))) by Th44

 .= (((((1 / 2) * (z6 * x)) + ((( - ((1 / 2) * )) * z5) * x)) + ((1 / 2) * (z6 * (x *' )))) + ((((1 / 2) * ) * z5) * (x *' ))) by A1, A23, A17, A18, A14, A21, Th24

 .= (((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) + ((( - ((1 / 2) * )) * z5) * x)) + ((((1 / 2) * ) * z5) * (x *' ))) by A1, A23, A17, A20, A18, Th24

 .= ((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) + (((( - ((1 / 2) * )) * z5) * x) + ((((1 / 2) * ) * z5) * (x *' )))) by A1, A23, A17, A20, A14, A19, Th24

 .= (((((1 / 2) * z6) * x) + ((1 / 2) * (z6 * (x *' )))) + (((( - ((1 / 2) * )) * z5) * x) + ((((1 / 2) * ) * z5) * (x *' )))) by Th44

 .= (((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *' ))) + (((( - ((1 / 2) * )) * z5) * x) + (( - (( - ((1 / 2) * )) * z5)) * (x *' )))) by Th44

 .= ((( Im a) * ( Re x)) + (( Re a) * ( Im x))) by A15, A22, Th45;

 hence thesis by A13;

 end;

 begin

 theorem :: COMPLSP2:66



 Th55: for x1,x2,y be FinSequence of COMPLEX st ( len x1) = ( len x2) & ( len x2) = ( len y) holds |((x1 + x2), y)| = ( |(x1, y)| + |(x2, y)|)

 proof

 let x1,x2,y be FinSequence of COMPLEX ;

 assume that

 A1: ( len x1) = ( len x2) and

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



 A3: ( len ( Re x1)) = ( len x1) & ( len ( Re x2)) = ( len x2) by Th40;



 A4: ( len ( Im y)) = ( len y) by Th40;



 A5: ( len ( Im x1)) = ( len x1) & ( len ( Im x2)) = ( len x2) by Th40;



 A6: ( len ( Re y)) = ( len y) by Th40;

 |((x1 + x2), y)| = ((( |((( Re x1) + ( Re x2)), ( Re y))| - ( * |(( Re (x1 + x2)), ( Im y))|)) + ( * |(( Im (x1 + x2)), ( Re y))|)) + |(( Im (x1 + x2)), ( Im y))|) by A1, Th41

 .= ((( |((( Re x1) + ( Re x2)), ( Re y))| - ( * |((( Re x1) + ( Re x2)), ( Im y))|)) + ( * |(( Im (x1 + x2)), ( Re y))|)) + |(( Im (x1 + x2)), ( Im y))|) by A1, Th41

 .= ((( |((( Re x1) + ( Re x2)), ( Re y))| - ( * |((( Re x1) + ( Re x2)), ( Im y))|)) + ( * |((( Im x1) + ( Im x2)), ( Re y))|)) + |(( Im (x1 + x2)), ( Im y))|) by A1, Th41

 .= ((( |((( Re x1) + ( Re x2)), ( Re y))| - ( * |((( Re x1) + ( Re x2)), ( Im y))|)) + ( * |((( Im x1) + ( Im x2)), ( Re y))|)) + |((( Im x1) + ( Im x2)), ( Im y))|) by A1, Th41

 .= (((( |(( Re x1), ( Re y))| + |(( Re x2), ( Re y))|) - ( * |((( Re x1) + ( Re x2)), ( Im y))|)) + ( * |((( Im x1) + ( Im x2)), ( Re y))|)) + |((( Im x1) + ( Im x2)), ( Im y))|) by A1, A2, A3, A6, RVSUM_1: 120

 .= (((( |(( Re x1), ( Re y))| + |(( Re x2), ( Re y))|) - ( * ( |(( Re x1), ( Im y))| + |(( Re x2), ( Im y))|))) + ( * |((( Im x1) + ( Im x2)), ( Re y))|)) + |((( Im x1) + ( Im x2)), ( Im y))|) by A1, A2, A3, A4, RVSUM_1: 120

 .= (((( |(( Re x1), ( Re y))| + |(( Re x2), ( Re y))|) - ( * ( |(( Re x1), ( Im y))| + |(( Re x2), ( Im y))|))) + ( * ( |(( Im x1), ( Re y))| + |(( Im x2), ( Re y))|))) + |((( Im x1) + ( Im x2)), ( Im y))|) by A1, A2, A6, A5, RVSUM_1: 120

 .= (((( |(( Re x1), ( Re y))| + |(( Re x2), ( Re y))|) - ( * ( |(( Re x1), ( Im y))| + |(( Re x2), ( Im y))|))) + ( * ( |(( Im x1), ( Re y))| + |(( Im x2), ( Re y))|))) + ( |(( Im x1), ( Im y))| + |(( Im x2), ( Im y))|)) by A1, A2, A5, A4, RVSUM_1: 120

 .= ( |(x1, y)| + |(x2, y)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:67



 Th56: for x1,x2 be FinSequence of COMPLEX st ( len x1) = ( len x2) holds |(( - x1), x2)| = ( - |(x1, x2)|)

 proof

 let x1,x2 be FinSequence of COMPLEX ;

 assume

 A1: ( len x1) = ( len x2);



 A2: ( len ( * x1)) = ( len x1) by Th3;

 |(( - x1), x2)| = |((( * ) * x1), x2)|

 .= |(( * ( * x1)), x2)| by Th44

 .= ( * |(( * x1), x2)|) by A1, A2, Th49

 .= ( * ( * |(x1, x2)|)) by A1, Th49

 .= (( - 1) * |(x1, x2)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:68



 Th57: for x1,x2 be FinSequence of COMPLEX st ( len x1) = ( len x2) holds |(x1, ( - x2))| = ( - |(x1, x2)|)

 proof

 let x1,x2 be FinSequence of COMPLEX ;

 assume

 A1: ( len x1) = ( len x2);



 A2: ( len ( * x2)) = ( len x2) by Th3;

 |(x1, ( - x2))| = |(x1, (( * ) * x2))|

 .= |(x1, ( * ( * x2)))| by Th44

 .= ( - ( * |(x1, ( * x2))|)) by A1, A2, Th50

 .= ( - ( * ( - ( * |(x1, x2)|)))) by A1, Th50

 .= ( - |(x1, x2)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:69

 for x1,x2 be FinSequence of COMPLEX st ( len x1) = ( len x2) holds |(( - x1), ( - x2))| = |(x1, x2)|

 proof

 let x1,x2 be FinSequence of COMPLEX ;

 assume

 A1: ( len x1) = ( len x2);

 then ( len ( - x2)) = ( len x1) by Th5;



 then |(( - x1), ( - x2))| = ( - |(x1, ( - x2))|) by Th56

 .= ( - ( - |(x1, x2)|)) by A1, Th57;

 hence thesis;

 end;

 theorem :: COMPLSP2:70



 Th59: for x1,x2,x3 be FinSequence of COMPLEX st ( len x1) = ( len x2) & ( len x2) = ( len x3) holds |((x1 - x2), x3)| = ( |(x1, x3)| - |(x2, x3)|)

 proof

 let x1,x2,x3 be FinSequence of COMPLEX ;

 assume that

 A1: ( len x1) = ( len x2) and

 A2: ( len x2) = ( len x3);

 ( len ( - x2)) = ( len x2) by Th5;



 then |((x1 - x2), x3)| = ( |(x1, x3)| + |(( - x2), x3)|) by A1, A2, Th55

 .= ( |(x1, x3)| + ( - |(x2, x3)|)) by A2, Th56;

 hence thesis;

 end;

 theorem :: COMPLSP2:71



 Th60: for x,y1,y2 be FinSequence of COMPLEX st ( len x) = ( len y1) & ( len y1) = ( len y2) holds |(x, (y1 + y2))| = ( |(x, y1)| + |(x, y2)|)

 proof

 let x,y1,y2 be FinSequence of COMPLEX ;

 assume that

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

 A2: ( len y1) = ( len y2);



 A3: ( len ( Re y1)) = ( len y1) & ( len ( Re y2)) = ( len y2) by Th40;



 A4: ( len ( Im x)) = ( len x) by Th40;



 A5: ( len ( Im y1)) = ( len y1) & ( len ( Im y2)) = ( len y2) by Th40;



 A6: ( len ( Re x)) = ( len x) by Th40;

 |(x, (y1 + y2))| = ((( |(( Re x), (( Re y1) + ( Re y2)))| - ( * |(( Re x), ( Im (y1 + y2)))|)) + ( * |(( Im x), ( Re (y1 + y2)))|)) + |(( Im x), ( Im (y1 + y2)))|) by A2, Th41

 .= ((( |(( Re x), (( Re y1) + ( Re y2)))| - ( * |(( Re x), ( Im (y1 + y2)))|)) + ( * |(( Im x), ( Re (y1 + y2)))|)) + |(( Im x), (( Im y1) + ( Im y2)))|) by A2, Th41

 .= ((( |(( Re x), (( Re y1) + ( Re y2)))| - ( * |(( Re x), (( Im y1) + ( Im y2)))|)) + ( * |(( Im x), ( Re (y1 + y2)))|)) + |(( Im x), (( Im y1) + ( Im y2)))|) by A2, Th41

 .= ((( |(( Re x), (( Re y1) + ( Re y2)))| - ( * |(( Re x), (( Im y1) + ( Im y2)))|)) + ( * |(( Im x), (( Re y1) + ( Re y2)))|)) + |(( Im x), (( Im y1) + ( Im y2)))|) by A2, Th41

 .= (((( |(( Re x), ( Re y1))| + |(( Re x), ( Re y2))|) - ( * |(( Re x), (( Im y1) + ( Im y2)))|)) + ( * |(( Im x), (( Re y1) + ( Re y2)))|)) + |(( Im x), (( Im y1) + ( Im y2)))|) by A1, A2, A3, A6, RVSUM_1: 120

 .= (((( |(( Re x), ( Re y1))| + |(( Re x), ( Re y2))|) - ( * |(( Re x), (( Im y1) + ( Im y2)))|)) + ( * |(( Im x), (( Re y1) + ( Re y2)))|)) + ( |(( Im x), ( Im y1))| + |(( Im x), ( Im y2))|)) by A1, A2, A5, A4, RVSUM_1: 120

 .= (((( |(( Re x), ( Re y1))| + |(( Re x), ( Re y2))|) - ( * ( |(( Re x), ( Im y1))| + |(( Re x), ( Im y2))|))) + ( * |(( Im x), (( Re y1) + ( Re y2)))|)) + ( |(( Im x), ( Im y1))| + |(( Im x), ( Im y2))|)) by A1, A2, A6, A5, RVSUM_1: 120

 .= (((( |(( Re x), ( Re y1))| + |(( Re x), ( Re y2))|) - ( * ( |(( Re x), ( Im y1))| + |(( Re x), ( Im y2))|))) + ( * ( |(( Im x), ( Re y1))| + |(( Im x), ( Re y2))|))) + ( |(( Im x), ( Im y1))| + |(( Im x), ( Im y2))|)) by A1, A2, A3, A4, RVSUM_1: 120

 .= ( |(x, y1)| + |(x, y2)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:72



 Th61: for x,y1,y2 be FinSequence of COMPLEX st ( len x) = ( len y1) & ( len y1) = ( len y2) holds |(x, (y1 - y2))| = ( |(x, y1)| - |(x, y2)|)

 proof

 let x,y1,y2 be FinSequence of COMPLEX ;

 assume that

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

 A2: ( len y1) = ( len y2);



 A3: ( len ( Re y1)) = ( len y1) & ( len ( Re y2)) = ( len y2) by Th40;



 A4: ( len ( Im x)) = ( len x) by Th40;



 A5: ( len ( Im y1)) = ( len y1) & ( len ( Im y2)) = ( len y2) by Th40;



 A6: ( len ( Re x)) = ( len x) by Th40;

 |(x, (y1 - y2))| = ((( |(( Re x), (( Re y1) - ( Re y2)))| - ( * |(( Re x), ( Im (y1 - y2)))|)) + ( * |(( Im x), ( Re (y1 - y2)))|)) + |(( Im x), ( Im (y1 - y2)))|) by A2, Th43

 .= ((( |(( Re x), (( Re y1) - ( Re y2)))| - ( * |(( Re x), ( Im (y1 - y2)))|)) + ( * |(( Im x), ( Re (y1 - y2)))|)) + |(( Im x), (( Im y1) - ( Im y2)))|) by A2, Th43

 .= ((( |(( Re x), (( Re y1) - ( Re y2)))| - ( * |(( Re x), (( Im y1) - ( Im y2)))|)) + ( * |(( Im x), ( Re (y1 - y2)))|)) + |(( Im x), (( Im y1) - ( Im y2)))|) by A2, Th43

 .= ((( |(( Re x), (( Re y1) - ( Re y2)))| - ( * |(( Re x), (( Im y1) - ( Im y2)))|)) + ( * |(( Im x), (( Re y1) - ( Re y2)))|)) + |(( Im x), (( Im y1) - ( Im y2)))|) by A2, Th43

 .= (((( |(( Re x), ( Re y1))| - |(( Re x), ( Re y2))|) - ( * |(( Re x), (( Im y1) - ( Im y2)))|)) + ( * |(( Im x), (( Re y1) - ( Re y2)))|)) + |(( Im x), (( Im y1) - ( Im y2)))|) by A1, A2, A3, A6, RVSUM_1: 124

 .= (((( |(( Re x), ( Re y1))| - |(( Re x), ( Re y2))|) - ( * |(( Re x), (( Im y1) - ( Im y2)))|)) + ( * |(( Im x), (( Re y1) - ( Re y2)))|)) + ( |(( Im x), ( Im y1))| - |(( Im x), ( Im y2))|)) by A1, A2, A5, A4, RVSUM_1: 124

 .= (((( |(( Re x), ( Re y1))| - |(( Re x), ( Re y2))|) - ( * ( |(( Re x), ( Im y1))| - |(( Re x), ( Im y2))|))) + ( * |(( Im x), (( Re y1) - ( Re y2)))|)) + ( |(( Im x), ( Im y1))| - |(( Im x), ( Im y2))|)) by A1, A2, A6, A5, RVSUM_1: 124

 .= (((( |(( Re x), ( Re y1))| - |(( Re x), ( Re y2))|) - ( * ( |(( Re x), ( Im y1))| - |(( Re x), ( Im y2))|))) + ( * ( |(( Im x), ( Re y1))| - |(( Im x), ( Re y2))|))) + ( |(( Im x), ( Im y1))| - |(( Im x), ( Im y2))|)) by A1, A2, A3, A4, RVSUM_1: 124

 .= ( |(x, y1)| - |(x, y2)|);

 hence thesis;

 end;

 theorem :: COMPLSP2:73



 Th62: for x1,x2,y1,y2 be FinSequence of COMPLEX st ( len x1) = ( len x2) & ( len x2) = ( len y1) & ( len y1) = ( len y2) holds |((x1 + x2), (y1 + y2))| = ((( |(x1, y1)| + |(x1, y2)|) + |(x2, y1)|) + |(x2, y2)|)

 proof

 let x1,x2,y1,y2 be FinSequence of COMPLEX ;

 assume that

 A1: ( len x1) = ( len x2) and

 A2: ( len x2) = ( len y1) and

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

 |((x1 + x2), y2)| = ( |(x1, y2)| + |(x2, y2)|) by A1, A2, A3, Th55;

 then

 A4: ( |((x1 + x2), y1)| + |((x1 + x2), y2)|) = (( |(x1, y1)| + |(x2, y1)|) + ( |(x1, y2)| + |(x2, y2)|)) by A1, A2, Th55;

 ( len (x1 + x2)) = ( len x1) by A1, Th6;

 hence thesis by A1, A2, A3, A4, Th60;

 end;

 theorem :: COMPLSP2:74



 Th63: for x1,x2,y1,y2 be FinSequence of COMPLEX st ( len x1) = ( len x2) & ( len x2) = ( len y1) & ( len y1) = ( len y2) holds |((x1 - x2), (y1 - y2))| = ((( |(x1, y1)| - |(x1, y2)|) - |(x2, y1)|) + |(x2, y2)|)

 proof

 let x1,x2,y1,y2 be FinSequence of COMPLEX ;

 assume that

 A1: ( len x1) = ( len x2) and

 A2: ( len x2) = ( len y1) and

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

 |(x1, (y1 - y2))| = ( |(x1, y1)| - |(x1, y2)|) by A1, A2, A3, Th61;

 then

 A4: ( |(x1, (y1 - y2))| - |(x2, (y1 - y2))|) = (( |(x1, y1)| - |(x1, y2)|) - ( |(x2, y1)| - |(x2, y2)|)) by A2, A3, Th61;

 ( len (y1 - y2)) = ( len y1) by A3, Th7;

 hence thesis by A1, A2, A4, Th59;

 end;

 theorem :: COMPLSP2:75



 Th64: for x,y be FinSequence of COMPLEX holds |(x, y)| = ( |(y, x)| *' )

 proof

 let x,y be FinSequence of COMPLEX ;

 set x1 = |(( Re y), ( Re x))|, x2 = |(( Re y), ( Im x))|, y1 = |(( Im y), ( Re x))|, y2 = |(( Im y), ( Im x))|;

 reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of REAL by XREAL_0:def 1;



 A1: ( Im x19) = 0 by COMPLEX1:def 2;



 A2: ( Im x29) = 0 by COMPLEX1:def 2;



 A3: ( Im y29) = 0 by COMPLEX1:def 2;



 A4: ( Im y19) = 0 by COMPLEX1:def 2;

 reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of COMPLEX by XCMPLX_0:def 2;

 ( |(y, x)| *' ) = (((x19 + y29) + ( * (y19 - x29))) *' )

 .= (((x19 + y29) *' ) + (( * (y19 - x29)) *' )) by COMPLEX1: 32

 .= (((x19 *' ) + (y29 *' )) + (( * (y19 - x29)) *' )) by COMPLEX1: 32

 .= ((x19 + (y29 *' )) + (( * (y19 - x29)) *' )) by A1, COMPLEX1: 38

 .= ((x19 + y29) + (( * (y19 - x29)) *' )) by A3, COMPLEX1: 38

 .= ((x19 + y29) + (( - ) * ((y19 - x29) *' ))) by COMPLEX1: 31, COMPLEX1: 35

 .= ((x19 + y29) + (( - ) * ((y19 *' ) - (x29 *' )))) by COMPLEX1: 34

 .= ((x19 + y29) + (( - ) * (y19 - (x29 *' )))) by A4, COMPLEX1: 38

 .= ((x19 + y29) + (( - ) * (y19 - x29))) by A2, COMPLEX1: 38

 .= |(x, y)|;

 hence thesis;

 end;

 theorem :: COMPLSP2:76

 for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |((x + y), (x + y))| = (( |(x, x)| + (2 * ( Re |(x, y)|))) + |(y, y)|)

 proof

 let x,y be FinSequence of COMPLEX ;

 set z = |(x, y)|;

 assume ( len x) = ( len y);



 then |((x + y), (x + y))| = ((( |(x, x)| + |(x, y)|) + |(y, x)|) + |(y, y)|) by Th62

 .= ((( |(x, x)| + |(x, y)|) + ( |(x, y)| *' )) + |(y, y)|) by Th64

 .= (( |(x, x)| + (z + (z *' ))) + |(y, y)|)

 .= (( |(x, x)| + (2 * ( Re |(x, y)|))) + |(y, y)|) by Th20;

 hence thesis;

 end;

 theorem :: COMPLSP2:77

 for x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |((x - y), (x - y))| = (( |(x, x)| - (2 * ( Re |(x, y)|))) + |(y, y)|)

 proof

 let x,y be FinSequence of COMPLEX ;

 set z = |(x, y)|;

 assume ( len x) = ( len y);



 then |((x - y), (x - y))| = ((( |(x, x)| - |(x, y)|) - |(y, x)|) + |(y, y)|) by Th63

 .= ((( |(x, x)| - |(x, y)|) - ( |(x, y)| *' )) + |(y, y)|) by Th64

 .= (( |(x, x)| - (z + (z *' ))) + |(y, y)|)

 .= (( |(x, x)| - (2 * ( Re |(x, y)|))) + |(y, y)|) by Th20;

 hence thesis;

 end;

 theorem :: COMPLSP2:78



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

 proof

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

 assume

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



 A2: ( len (( Re a) * ( Im x))) = ( len ( Im x)) & ( len (( Im a) * ( Re x))) = ( len ( Re x)) by RVSUM_1: 117;



 A3: ( len (( Re a) * ( Re x))) = ( len ( Re x)) & ( len (( Im a) * ( Im x))) = ( len ( Im x)) by RVSUM_1: 117;



 A4: ( len ( Re x)) = ( len x) by Th40;



 A5: ( len ( Im y)) = ( len y) by Th40;



 A6: ( len ( Re y)) = ( len y) by Th40;



 A7: ( len ( Im x)) = ( len x) by Th40;

 |((a * x), y)| = ((( |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Re y))| - ( * |(( Re (a * x)), ( Im y))|)) + ( * |(( Im (a * x)), ( Re y))|)) + |(( Im (a * x)), ( Im y))|) by Th54

 .= ((( |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Re y))| - ( * |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Im y))|)) + ( * |(( Im (a * x)), ( Re y))|)) + |(( Im (a * x)), ( Im y))|) by Th54

 .= ((( |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Re y))| - ( * |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Im y))|)) + ( * |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Re y))|)) + |(( Im (a * x)), ( Im y))|) by Th54

 .= ((( |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Re y))| - ( * |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Im y))|)) + ( * |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Re y))|)) + |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Im y))|) by Th54

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * |(((( Re a) * ( Re x)) - (( Im a) * ( Im x))), ( Im y))|)) + ( * |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Re y))|)) + |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Im y))|) by A1, A4, A6, A7, A3, RVSUM_1: 124

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * ( |((( Re a) * ( Re x)), ( Im y))| - |((( Im a) * ( Im x)), ( Im y))|))) + ( * |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Re y))|)) + |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Im y))|) by A1, A4, A7, A5, A3, RVSUM_1: 124

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * ( |((( Re a) * ( Re x)), ( Im y))| - |((( Im a) * ( Im x)), ( Im y))|))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + |(((( Im a) * ( Re x)) + (( Re a) * ( Im x))), ( Im y))|) by A1, A4, A6, A7, A2, RVSUM_1: 120

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * ( |((( Re a) * ( Re x)), ( Im y))| - |((( Im a) * ( Im x)), ( Im y))|))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A4, A7, A5, A2, RVSUM_1: 120

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * ((( Re a) * |(( Re x), ( Im y))|) - |((( Im a) * ( Im x)), ( Im y))|))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A4, A5, RVSUM_1: 121

 .= (((( |((( Re a) * ( Re x)), ( Re y))| - |((( Im a) * ( Im x)), ( Re y))|) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A7, A5, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - |((( Im a) * ( Im x)), ( Re y))|) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A4, A6, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - (( Im a) * |(( Im x), ( Re y))|)) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ( |((( Im a) * ( Re x)), ( Re y))| + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A6, A7, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - (( Im a) * |(( Im x), ( Re y))|)) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ((( Im a) * |(( Re x), ( Re y))|) + |((( Re a) * ( Im x)), ( Re y))|))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A4, A6, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - (( Im a) * |(( Im x), ( Re y))|)) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ((( Im a) * |(( Re x), ( Re y))|) + (( Re a) * |(( Im x), ( Re y))|)))) + ( |((( Im a) * ( Re x)), ( Im y))| + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A6, A7, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - (( Im a) * |(( Im x), ( Re y))|)) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ((( Im a) * |(( Re x), ( Re y))|) + (( Re a) * |(( Im x), ( Re y))|)))) + ((( Im a) * |(( Re x), ( Im y))|) + |((( Re a) * ( Im x)), ( Im y))|)) by A1, A4, A5, RVSUM_1: 121

 .= (((((( Re a) * |(( Re x), ( Re y))|) - (( Im a) * |(( Im x), ( Re y))|)) - ( * ((( Re a) * |(( Re x), ( Im y))|) - (( Im a) * |(( Im x), ( Im y))|)))) + ( * ((( Im a) * |(( Re x), ( Re y))|) + (( Re a) * |(( Im x), ( Re y))|)))) + ((( Im a) * |(( Re x), ( Im y))|) + (( Re a) * |(( Im x), ( Im y))|))) by A1, A7, A5, RVSUM_1: 121

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

 .= ((((((( Re a) * |(( Re x), ( Re y))|) + (( * ( Im a)) * |(( Re x), ( Re y))|)) - ((( Re a) * ) * |(( Re x), ( Im y))|)) + (( Im a) * |(( Re x), ( Im y))|)) + ((( Re a) + ( * ( Im a))) * ( * |(( Im x), ( Re y))|))) + (a * |(( Im x), ( Im y))|)) by COMPLEX1: 13

 .= (((((( Re a) * |(( Re x), ( Re y))|) + (( * ( Im a)) * |(( Re x), ( Re y))|)) - ((( Re a) + ( * ( Im a))) * ( * |(( Re x), ( Im y))|))) + (a * ( * |(( Im x), ( Re y))|))) + (a * |(( Im x), ( Im y))|)) by COMPLEX1: 13

 .= (((((( Re a) + ( * ( Im a))) * |(( Re x), ( Re y))|) - (a * ( * |(( Re x), ( Im y))|))) + (a * ( * |(( Im x), ( Re y))|))) + (a * |(( Im x), ( Im y))|)) by COMPLEX1: 13

 .= ((((a * |(( Re x), ( Re y))|) - (a * ( * |(( Re x), ( Im y))|))) + (a * ( * |(( Im x), ( Re y))|))) + (a * |(( Im x), ( Im y))|)) by COMPLEX1: 13

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

 hence thesis;

 end;

 theorem :: COMPLSP2:79



 Th68: for a be Element of COMPLEX , x,y be FinSequence of COMPLEX st ( len x) = ( len y) holds |(x, (a * y))| = ((a *' ) * |(x, y)|)

 proof

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

 assume

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

 |(x, (a * y))| = ( |((a * y), x)| *' ) by Th64

 .= ((a * |(y, x)|) *' ) by A1, Th67

 .= ((a *' ) * ( |(y, x)| *' )) by COMPLEX1: 35

 .= ((a *' ) * |(x, y)|) by Th64;

 hence thesis;

 end;

 theorem :: COMPLSP2:80

 for a,b be Element of COMPLEX , x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds |(((a * x) + (b * y)), z)| = ((a * |(x, z)|) + (b * |(y, z)|))

 proof

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

 assume that

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

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

 ( len (a * x)) = ( len x) & ( len (b * y)) = ( len y) by Th3;



 then |(((a * x) + (b * y)), z)| = ( |((a * x), z)| + |((b * y), z)|) by A1, A2, Th55

 .= ((a * |(x, z)|) + |((b * y), z)|) by A1, A2, Th67

 .= ((a * |(x, z)|) + (b * |(y, z)|)) by A2, Th67;

 hence thesis;

 end;

 theorem :: COMPLSP2:81

 for a,b be Element of COMPLEX , x,y,z be FinSequence of COMPLEX st ( len x) = ( len y) & ( len y) = ( len z) holds |(x, ((a * y) + (b * z)))| = (((a *' ) * |(x, y)|) + ((b *' ) * |(x, z)|))

 proof

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

 assume that

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

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

 ( len (a * y)) = ( len y) & ( len (b * z)) = ( len z) by Th3;



 then |(x, ((a * y) + (b * z)))| = ( |(x, (a * y))| + |(x, (b * z))|) by A1, A2, Th60

 .= (((a *' ) * |(x, y)|) + |(x, (b * z))|) by A1, Th68

 .= (((a *' ) * |(x, y)|) + ((b *' ) * |(x, z)|)) by A1, A2, Th68;

 hence thesis;

 end;