rvsum_2.miz



    begin

    definition

      let F be complex-valued Relation;

      :: original: rng

      redefine

      func rng F -> Subset of COMPLEX ;

      coherence by VALUED_0:def 1;

    end

    registration

      let D be non empty set;

      let F be Function of COMPLEX , D;

      let F1 be complex-valued FinSequence;

      cluster (F * F1) -> FinSequence-like;

      coherence

      proof

        consider n1 be Nat such that

         A1: ( dom F1) = ( Seg n1) by FINSEQ_1:def 2;

        take n1;

        ( dom F) = COMPLEX & ( rng F1) c= COMPLEX by FUNCT_2:def 1;

        hence thesis by A1, RELAT_1: 27;

      end;

    end

    reserve s for set,

i,j for Nat,

x,x1,x2 for Element of COMPLEX ,

c,c1,c2,c3 for Complex,

F,F1,F2 for complex-valued FinSequence,

R,R1,R2 for i -element FinSequence of COMPLEX ;

    definition

      :: RVSUM_2:def1

      func sqrcomplex -> UnOp of COMPLEX means

      : Def1: for c holds (it . c) = (c ^2 );

      existence

      proof

        deffunc F( Element of COMPLEX ) = ($1 ^2 );

        consider G be Function of COMPLEX , COMPLEX such that

         A1: for x be Element of COMPLEX holds (G . x) = F(x) from FUNCT_2:sch 4;

        take G;

        let c;

        c in COMPLEX by XCMPLX_0:def 2;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let G1,G2 be UnOp of COMPLEX such that

         A2: for c holds (G1 . c) = (c ^2 ) and

         A3: for c holds (G2 . c) = (c ^2 );

        now

          let x;

          (G1 . x) = (x ^2 ) by A2;

          hence (G1 . x) = (G2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: RVSUM_2:1

     sqrcomplex is_distributive_wrt multcomplex

    proof

      let x1, x2;

      

      thus ( sqrcomplex . ( multcomplex . (x1,x2))) = ( sqrcomplex . (x1 * x2)) by BINOP_2:def 5

      .= ((x1 * x2) ^2 ) by Def1

      .= ((x1 ^2 ) * (x2 ^2 ))

      .= ( multcomplex . ((x1 ^2 ),(x2 ^2 ))) by BINOP_2:def 5

      .= ( multcomplex . (( sqrcomplex . x1),(x2 ^2 ))) by Def1

      .= ( multcomplex . (( sqrcomplex . x1),( sqrcomplex . x2))) by Def1;

    end;

    

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

    proof

      reconsider a = c, s = c1 as Element of COMPLEX by XCMPLX_0:def 2;

      

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

      .= ( multcomplex . (a,s))

      .= (c * c1) by BINOP_2:def 5;

    end;

    theorem :: RVSUM_2:2

    (c multcomplex ) is_distributive_wrt addcomplex

    proof

      c in COMPLEX by XCMPLX_0:def 2;

      hence thesis by FINSEQOP: 54, SEQ_4: 54;

    end;

    begin

    

     Lm2: F is FinSequence of COMPLEX

    proof

      thus ( rng F) c= COMPLEX ;

    end;

    definition

      let F1, F2;

      :: original: +

      redefine

      :: RVSUM_2:def2

      func F1 + F2 -> FinSequence of COMPLEX equals ( addcomplex .: (F1,F2));

      coherence by Lm2;

      compatibility

      proof

        reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

        let F be FinSequence of COMPLEX ;

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

        then [:( rng F3), ( rng F4):] c= ( dom addcomplex ) by ZFMISC_1: 96;

        then

         A1: ( dom ( addcomplex .: (F1,F2))) = (( dom F1) /\ ( dom F2)) by FUNCOP_1: 69;

        

         A2: ( dom (F1 + F2)) = (( dom F1) /\ ( dom F2)) by VALUED_1:def 1;

        thus F = (F1 + F2) implies F = ( addcomplex .: (F1,F2))

        proof

          assume

           A3: F = (F1 + F2);

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

          proof

            let z be set;

            assume z in ( dom ( addcomplex .: (F1,F2)));

            

            hence (F . z) = ((F1 . z) + (F2 . z)) by A2, A1, A3, VALUED_1:def 1

            .= ( addcomplex . ((F1 . z),(F2 . z))) by BINOP_2:def 3;

          end;

          hence thesis by A2, A1, A3, FUNCOP_1: 21;

        end;

        assume

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

        now

          let c be object;

          assume c in ( dom F);

          

          hence (F . c) = ( addcomplex . ((F1 . c),(F2 . c))) by A4, FUNCOP_1: 22

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

        end;

        hence thesis by A1, A4, VALUED_1:def 1;

      end;

      commutativity

      proof

        let F be FinSequence of COMPLEX ;

        let F1, F2;

        assume

         A5: F = ( addcomplex .: (F1,F2));

        reconsider F1, F2 as FinSequence of COMPLEX by Lm2;

        

         A6: ( dom addcomplex ) = [: COMPLEX , COMPLEX :] by FUNCT_2:def 1;

        then

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

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

        

        then

         A8: ( dom ( addcomplex .: (F1,F2))) = (( dom F1) /\ ( dom F2)) by FUNCOP_1: 69

        .= ( dom ( addcomplex .: (F2,F1))) by A7, FUNCOP_1: 69;

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

        proof

          let z be set;

          assume z in ( dom ( addcomplex .: (F2,F1)));

          

          hence (F . z) = ( addcomplex . ((F1 . z),(F2 . z))) by A5, A8, FUNCOP_1: 22

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

          .= ( addcomplex . ((F2 . z),(F1 . z))) by BINOP_2:def 3;

        end;

        hence thesis by A5, A8, FUNCOP_1: 21;

      end;

    end

    definition

      let i, R1, R2;

      :: original: +

      redefine

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

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_2:3

    ((R1 + R2) . s) = ((R1 . s) + (R2 . s))

    proof

      per cases ;

        suppose

         A1: not s in ( Seg i);

        then

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

        

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

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

        

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

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

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

      end;

        suppose s in ( Seg i);

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

        hence thesis by VALUED_1:def 1;

      end;

    end;

    theorem :: RVSUM_2:4

    (( <*> COMPLEX ) + F) = ( <*> COMPLEX )

    proof

      F is FinSequence of COMPLEX by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_2:5

    ( <*c1*> + <*c2*>) = <*(c1 + c2)*>

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ( <*s1*> + <*s2*>) = <*( addcomplex . (s1,s2))*> by FINSEQ_2: 74

      .= <*(c1 + c2)*> by BINOP_2:def 3;

      hence thesis;

    end;

    theorem :: RVSUM_2:6

    ((i |-> c1) + (i |-> c2)) = (i |-> (c1 + c2))

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ((i |-> s1) + (i |-> s2)) = (i |-> ( addcomplex . (s1,s2))) by FINSEQOP: 17

      .= (i |-> (c1 + c2)) by BINOP_2:def 3;

      hence thesis;

    end;

    definition

      let F;

      :: original: -

      redefine

      :: RVSUM_2:def3

      func - F -> FinSequence of COMPLEX equals ( compcomplex * F);

      coherence by Lm2;

      compatibility

      proof

        let F1 be FinSequence of COMPLEX ;

        

         A1: ( dom ( - F)) = ( dom F) by VALUED_1: 8;

        

         A2: ( rng F) c= COMPLEX & ( dom compcomplex ) = COMPLEX by FUNCT_2:def 1;

        then

         A3: ( dom ( compcomplex * F)) = ( dom F) by RELAT_1: 27;

        thus F1 = ( - F) implies F1 = ( compcomplex * F)

        proof

          assume

           A4: F1 = ( - F);

          now

            let c be object;

            assume

             A5: c in ( dom F1);

            

            thus (F1 . c) = ( - (F . c)) by A4, VALUED_1: 8

            .= ( compcomplex . (F . c)) by BINOP_2:def 1

            .= (( compcomplex * F) . c) by A1, A4, A5, FUNCT_1: 13;

          end;

          hence thesis by A3, A4, FUNCT_1: 2, VALUED_1: 8;

        end;

        assume

         A6: F1 = ( compcomplex * F);

        now

          let c be object;

          assume

           A7: c in ( dom F1);

          

          thus (( - F) . c) = ( - (F . c)) by VALUED_1: 8

          .= ( compcomplex . (F . c)) by BINOP_2:def 1

          .= (( compcomplex * F) . c) by A6, A7, FUNCT_1: 12;

        end;

        hence thesis by A1, A2, A6, FUNCT_1: 2, RELAT_1: 27;

      end;

    end

    definition

      let i, R;

      :: original: -

      redefine

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

      coherence by FINSEQ_2: 113;

    end

    theorem :: RVSUM_2:7

    ( - <*c*>) = <*( - c)*>

    proof

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

      ( - <*s*>) = <*( compcomplex . s)*> by FINSEQ_2: 35

      .= <*( - c)*> by BINOP_2:def 1;

      hence thesis;

    end;

    theorem :: RVSUM_2:8

    

     Th8: ( - (i |-> c)) = (i |-> ( - c))

    proof

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

      ( - (i |-> s)) = (i |-> ( compcomplex . s)) by FINSEQOP: 16

      .= (i |-> ( - c)) by BINOP_2:def 1;

      hence thesis;

    end;

    theorem :: RVSUM_2:9

    (R1 + R) = (R2 + R) implies R1 = R2

    proof

      assume (R1 + R) = (R2 + R);

      then (R1 + (R + ( - R))) = ((R2 + R) + ( - R)) by FINSEQOP: 28;

      then

       A1: (R1 + (R + ( - R))) = (R2 + (R + ( - R))) by FINSEQOP: 28;

      (R + ( - R)) = (i |-> 0c ) by BINOP_2: 1, FINSEQOP: 73, SEQ_4: 51, SEQ_4: 52;

      then R1 = (R2 + (i |-> 0c )) by A1, BINOP_2: 1, FINSEQOP: 56;

      hence thesis by BINOP_2: 1, FINSEQOP: 56;

    end;

    theorem :: RVSUM_2:10

    

     Th10: ( - (F1 + F2)) = (( - F1) + ( - F2))

    proof

      

       A1: ( dom ( - (F1 + F2))) = ( dom (F1 + F2)) by VALUED_1: 8;

      

       A2: ( dom (F1 + F2)) = (( dom F1) /\ ( dom F2)) by VALUED_1:def 1;

      

       A3: ( dom (( - F1) + ( - F2))) = (( dom ( - F1)) /\ ( dom ( - F2))) by VALUED_1:def 1

      .= (( dom F1) /\ ( dom ( - F2))) by VALUED_1: 8

      .= (( dom F1) /\ ( dom F2)) by VALUED_1: 8;

      now

        let i;

        assume

         A4: i in ( dom ( - (F1 + F2)));

        

        thus (( - (F1 + F2)) . i) = ( - ((F1 + F2) . i)) by VALUED_1: 8

        .= ( - ((F1 . i) + (F2 . i))) by A1, A4, VALUED_1:def 1

        .= (( - (F1 . i)) + ( - (F2 . i)))

        .= (( - (F1 . i)) + (( - F2) . i)) by VALUED_1: 8

        .= ((( - F1) . i) + (( - F2) . i)) by VALUED_1: 8

        .= ((( - F1) + ( - F2)) . i) by A1, A2, A3, A4, VALUED_1:def 1;

      end;

      hence thesis by A2, A3, FINSEQ_1: 13, VALUED_1: 8;

    end;

    definition

      let F1, F2;

      :: original: -

      redefine

      :: RVSUM_2:def4

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

      coherence by Lm2;

      compatibility

      proof

        reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

        let F be FinSequence of COMPLEX ;

        

         A1: ( dom (F1 - F2)) = (( dom F1) /\ ( dom F2)) by VALUED_1: 12;

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

        then

         A2: [:( rng F3), ( rng F4):] c= ( dom diffcomplex ) by ZFMISC_1: 96;

        then

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

        thus F = (F1 - F2) implies F = ( diffcomplex .: (F1,F2))

        proof

          assume

           A4: F = (F1 - F2);

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

          proof

            let z be set;

            assume z in ( dom ( diffcomplex .: (F1,F2)));

            

            hence (F . z) = ((F1 . z) - (F2 . z)) by A1, A3, A4, VALUED_1: 13

            .= ( diffcomplex . ((F1 . z),(F2 . z))) by BINOP_2:def 4;

          end;

          hence thesis by A1, A3, A4, FUNCOP_1: 21;

        end;

        assume

         A5: F = ( diffcomplex .: (F1,F2));

        now

          let c be object;

          assume c in ( dom F);

          

          hence (F . c) = ( diffcomplex . ((F1 . c),(F2 . c))) by A5, FUNCOP_1: 22

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

        end;

        hence thesis by A1, A2, A5, FUNCOP_1: 69, VALUED_1: 14;

      end;

    end

    definition

      let i, R1, R2;

      :: original: -

      redefine

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

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_2:11

    ((R1 - R2) . s) = ((R1 . s) - (R2 . s))

    proof

      per cases ;

        suppose

         A1: not s in ( Seg i);

        then

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

        

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

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

        

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

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

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

      end;

        suppose s in ( Seg i);

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

        hence thesis by VALUED_1: 13;

      end;

    end;

    theorem :: RVSUM_2:12

    (( <*> COMPLEX ) - F) = ( <*> COMPLEX ) & (F - ( <*> COMPLEX )) = ( <*> COMPLEX )

    proof

      F is FinSequence of COMPLEX by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_2:13

    ( <*c1*> - <*c2*>) = <*(c1 - c2)*>

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ( <*s1*> - <*s2*>) = <*( diffcomplex . (s1,s2))*> by FINSEQ_2: 74

      .= <*(c1 - c2)*> by BINOP_2:def 4;

      hence thesis;

    end;

    theorem :: RVSUM_2:14

    ((i |-> c1) - (i |-> c2)) = (i |-> (c1 - c2))

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ((i |-> s1) - (i |-> s2)) = (i |-> ( diffcomplex . (s1,s2))) by FINSEQOP: 17

      .= (i |-> (c1 - c2)) by BINOP_2:def 4;

      hence thesis;

    end;

    theorem :: RVSUM_2:15

    (R - (i |-> 0c )) = R

    proof

      

      thus (R - (i |-> 0c )) = (R + (i |-> ( - 0 ))) by Th8

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

    end;

    theorem :: RVSUM_2:16

    ( - (F1 - F2)) = (F2 - F1)

    proof

      

      thus ( - (F1 - F2)) = (( - F1) + ( - ( - F2))) by Th10

      .= (F2 - F1);

    end;

    theorem :: RVSUM_2:17

    ( - (F1 - F2)) = (( - F1) + F2)

    proof

      

      thus ( - (F1 - F2)) = (( - F1) + ( - ( - F2))) by Th10

      .= (( - F1) + F2);

    end;

    theorem :: RVSUM_2:18

    (R1 - R2) = (i |-> 0c ) implies R1 = R2

    proof

      assume (R1 - R2) = (i |-> 0c );

      then R1 = ( - ( - R2)) by BINOP_2: 1, FINSEQOP: 74, SEQ_4: 51, SEQ_4: 52;

      hence thesis;

    end;

    theorem :: RVSUM_2:19

    R1 = ((R1 + R) - R)

    proof

      

      thus R1 = (R1 + (i |-> 0c )) by BINOP_2: 1, FINSEQOP: 56

      .= (R1 + (R - R)) by BINOP_2: 1, FINSEQOP: 73, SEQ_4: 51, SEQ_4: 52

      .= ((R1 + R) - R) by RFUNCT_1: 23;

    end;

    theorem :: RVSUM_2:20

    R1 = ((R1 - R) + R)

    proof

      

      thus R1 = (R1 + (i |-> 0c )) by BINOP_2: 1, FINSEQOP: 56

      .= (R1 + (( - R) + R)) by BINOP_2: 1, FINSEQOP: 73, SEQ_4: 51, SEQ_4: 52

      .= ((R1 - R) + R) by FINSEQOP: 28;

    end;

    notation

      let F, c;

      synonym c * F for c (#) F;

    end

    definition

      let F, c;

      :: original: *

      redefine

      :: RVSUM_2:def5

      func c * F -> FinSequence of COMPLEX equals ((c multcomplex ) * F);

      coherence by Lm2;

      compatibility

      proof

        let F1 be FinSequence of COMPLEX ;

        

         A1: ( dom (c * F)) = ( dom F) by VALUED_1:def 5;

        

         A2: ( rng F) c= COMPLEX & ( dom (c multcomplex )) = COMPLEX by FUNCT_2:def 1;

        then

         A3: ( dom ((c multcomplex ) * F)) = ( dom F) by RELAT_1: 27;

        thus F1 = (c * F) implies F1 = ((c multcomplex ) * F)

        proof

          assume

           A4: F1 = (c * F);

          now

            let s be object;

            assume

             A5: s in ( dom F1);

            

            hence (F1 . s) = (c * (F . s)) by A4, VALUED_1:def 5

            .= ((c multcomplex ) . (F . s)) by Lm1

            .= (((c multcomplex ) * F) . s) by A1, A4, A5, FUNCT_1: 13;

          end;

          hence thesis by A1, A3, A4, FUNCT_1: 2;

        end;

        assume

         A6: F1 = ((c multcomplex ) * F);

        now

          let s be object;

          assume

           A7: s in ( dom F1);

          

          thus ((c * F) . s) = (c * (F . s)) by VALUED_1: 6

          .= ((c multcomplex ) . (F . s)) by Lm1

          .= (((c multcomplex ) * F) . s) by A6, A7, FUNCT_1: 12;

        end;

        hence thesis by A1, A2, A6, FUNCT_1: 2, RELAT_1: 27;

      end;

    end

    definition

      let i, R, c;

      :: original: *

      redefine

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

      coherence by FINSEQ_2: 113;

    end

    theorem :: RVSUM_2:21

    (c * <*c1*>) = <*(c * c1)*>

    proof

      reconsider s = c, s1 = c1 as Element of COMPLEX by XCMPLX_0:def 2;

      (s * <*s1*>) = <*(( multcomplex [;] (s,( id COMPLEX ))) . s1)*> by FINSEQ_2: 35

      .= <*(c * c1)*> by Lm1;

      hence thesis;

    end;

    theorem :: RVSUM_2:22

    

     Th22: (c1 * (i |-> c2)) = (i |-> (c1 * c2))

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      (s1 * (i |-> s2)) = (i |-> (( multcomplex [;] (s1,( id COMPLEX ))) . s2)) by FINSEQOP: 16

      .= (i |-> (c1 * c2)) by Lm1;

      hence thesis;

    end;

    theorem :: RVSUM_2:23

    ((c1 + c2) * F) = ((c1 * F) + (c2 * F))

    proof

      

       A1: ( dom ((c1 + c2) * F)) = ( dom F) by VALUED_1:def 5;

      

       A2: ( dom ((c1 * F) + (c2 * F))) = (( dom (c1 * F)) /\ ( dom (c2 * F))) by VALUED_1:def 1;

      

       A3: ( dom (c1 * F)) = ( dom F) by VALUED_1:def 5;

      

       A4: ( dom (c2 * F)) = ( dom F) by VALUED_1:def 5;

      now

        let i;

        assume

         A5: i in ( dom ((c1 + c2) * F));

        

        thus (((c1 + c2) * F) . i) = ((c1 + c2) * (F . i)) by VALUED_1: 6

        .= ((c1 * (F . i)) + (c2 * (F . i)))

        .= ((c1 * (F . i)) + ((c2 * F) . i)) by VALUED_1: 6

        .= (((c1 * F) . i) + ((c2 * F) . i)) by VALUED_1: 6

        .= (((c1 * F) + (c2 * F)) . i) by A1, A2, A3, A4, A5, VALUED_1:def 1;

      end;

      hence thesis by A1, A2, A3, A4, FINSEQ_1: 13;

    end;

    theorem :: RVSUM_2:24

    ( 0c * R) = (i |-> 0c )

    proof

      

       A1: ( rng R) c= COMPLEX ;

      

      thus ( 0c * R) = ( multcomplex [;] ( 0c ,(( id COMPLEX ) * R))) by FUNCOP_1: 34

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

      .= (i |-> 0c ) by BINOP_2: 1, FINSEQOP: 76, SEQ_4: 51, SEQ_4: 54;

    end;

    notation

      let F1, F2;

      synonym mlt (F1,F2) for F1 (#) F2;

    end

    definition

      let F1, F2;

      :: original: mlt

      redefine

      :: RVSUM_2:def6

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

      coherence by Lm2;

      compatibility

      proof

        reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

        let F be FinSequence of COMPLEX ;

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

        then [:( rng F3), ( rng F4):] c= ( dom multcomplex ) by ZFMISC_1: 96;

        then

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

        

         A2: ( dom ( mlt (F1,F2))) = (( dom F1) /\ ( dom F2)) by VALUED_1:def 4;

        thus F = ( mlt (F1,F2)) implies F = ( multcomplex .: (F1,F2))

        proof

          assume

           A3: F = ( mlt (F1,F2));

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

          proof

            let z be set;

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

            

            thus (F . z) = ((F1 . z) * (F2 . z)) by A3, VALUED_1: 5

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

          end;

          hence thesis by A1, A2, A3, FUNCOP_1: 21;

        end;

        assume

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

        now

          let c be object;

          assume c in ( dom F);

          

          hence (F . c) = ( multcomplex . ((F1 . c),(F2 . c))) by A4, FUNCOP_1: 22

          .= ((F1 . c) * (F2 . c)) by BINOP_2:def 5;

        end;

        hence thesis by A1, A4, VALUED_1:def 4;

      end;

      commutativity

      proof

        let F be FinSequence of COMPLEX ;

        let F1, F2;

        reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

        

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

        then

         A6: [:( rng F4), ( rng F3):] c= ( dom multcomplex ) by ZFMISC_1: 96;

         [:( rng F3), ( rng F4):] c= ( dom multcomplex ) by A5, ZFMISC_1: 96;

        

        then

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

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

        assume

         A8: 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

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

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

          

          thus (F . z) = ( multcomplex . ((F1 . z),(F2 . z))) by A8, A7, A9, FUNCOP_1: 22

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

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

        end;

        hence thesis by A8, A7, FUNCOP_1: 21;

      end;

    end

    definition

      let i, R1, R2;

      :: original: mlt

      redefine

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

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_2:25

    ( mlt (( <*> COMPLEX ),F)) = ( <*> COMPLEX )

    proof

      F is FinSequence of COMPLEX by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_2:26

    ( mlt ( <*c1*>, <*c2*>)) = <*(c1 * c2)*>

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ( mlt ( <*s1*>, <*s2*>)) = <*( multcomplex . (s1,s2))*> by FINSEQ_2: 74

      .= <*(c1 * c2)*> by BINOP_2:def 5;

      hence thesis;

    end;

    theorem :: RVSUM_2:27

    

     Th27: ( mlt ((i |-> c),R)) = (c * R)

    proof

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

      ( mlt ((i |-> s),R)) = ( multcomplex [;] (s,R)) by FINSEQOP: 20

      .= (c * R) by FINSEQOP: 22;

      hence thesis;

    end;

    theorem :: RVSUM_2:28

    ( mlt ((i |-> c1),(i |-> c2))) = (i |-> (c1 * c2))

    proof

      reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

      ( mlt ((i |-> s1),(i |-> s2))) = (s1 * (i |-> s2)) by Th27

      .= (i |-> (c1 * c2)) by Th22;

      hence thesis;

    end;

    begin

    theorem :: RVSUM_2:29

    

     Th29: ( Sum ( <*> COMPLEX )) = 0c by BINOP_2: 1, FINSOP_1: 10;

    registration

      let f be empty FinSequence;

      cluster ( Sum f) -> zero;

      coherence by Th29;

    end

    theorem :: RVSUM_2:30

    ( Sum <*c*>) = c

    proof

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

      ( Sum <*c*>) = c by FINSOP_1: 11;

      hence thesis;

    end;

    theorem :: RVSUM_2:31

    

     Th31: ( Sum (F ^ <*c*>)) = (( Sum F) + c)

    proof

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

      reconsider F1 = F as FinSequence of COMPLEX by Lm2;

      

      thus ( Sum (F ^ <*c*>)) = ( Sum (F1 ^ <*s*>))

      .= ( addcomplex . (( addcomplex $$ F1),s)) by FINSOP_1: 4

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

      .= (( Sum F) + c);

    end;

    theorem :: RVSUM_2:32

    

     Th32: ( Sum (F1 ^ F2)) = (( Sum F1) + ( Sum F2))

    proof

      reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

      

      thus ( Sum (F1 ^ F2)) = ( Sum (F3 ^ F4))

      .= ( addcomplex . (( addcomplex $$ F3),( addcomplex $$ F4))) by FINSOP_1: 5

      .= (( Sum F3) + ( Sum F4)) by BINOP_2:def 3

      .= (( Sum F1) + ( Sum F2));

    end;

    theorem :: RVSUM_2:33

    ( Sum ( <*c*> ^ F)) = (c + ( Sum F))

    proof

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

      

      thus ( Sum ( <*c*> ^ F)) = (( Sum <*s*>) + ( Sum F)) by Th32

      .= (c + ( Sum F)) by FINSOP_1: 11;

    end;

    theorem :: RVSUM_2:34

    

     Th34: ( Sum <*c1, c2*>) = (c1 + c2)

    proof

      reconsider s1 = c1 as Element of COMPLEX by XCMPLX_0:def 2;

      

      thus ( Sum <*c1, c2*>) = (( Sum <*s1*>) + c2) by Th31

      .= (c1 + c2) by FINSOP_1: 11;

    end;

    theorem :: RVSUM_2:35

    ( Sum <*c1, c2, c3*>) = ((c1 + c2) + c3)

    proof

      

      thus ( Sum <*c1, c2, c3*>) = (( Sum <*c1, c2*>) + c3) by Th31

      .= ((c1 + c2) + c3) by Th34;

    end;

    theorem :: RVSUM_2:36

    

     Th36: ( Sum (i |-> c)) = (i * c)

    proof

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

      defpred P[ Nat] means ( Sum ($1 |-> c)) = ($1 * c);

      

       A1: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A2: ( Sum (i |-> c)) = (i * c);

        

        thus ( Sum ((i + 1) |-> c)) = ( Sum ((i |-> c) ^ <*c*>)) by FINSEQ_2: 60

        .= ((i * c) + (1 * c)) by A2, Th31

        .= ((i + 1) * c);

      end;

      

       A3: P[ 0 ];

      for i holds P[i] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: RVSUM_2:37

    ( Sum (i |-> 0c )) = 0c

    proof

      

      thus ( Sum (i |-> 0c )) = (i * 0 ) by Th36

      .= 0c ;

    end;

    theorem :: RVSUM_2:38

    ( Sum (c * F)) = (c * ( Sum F))

    proof

      reconsider F1 = F as FinSequence of COMPLEX by Lm2;

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

      set cM = ( multcomplex [;] (s,( id COMPLEX )));

      

      thus ( Sum (c * F)) = (cM . ( addcomplex $$ F1)) by SEQ_4: 51, SEQ_4: 54, SETWOP_2: 30

      .= (c * ( Sum F1)) by Lm1

      .= (c * ( Sum F));

    end;

    theorem :: RVSUM_2:39

    

     Th39: ( Sum ( - F)) = ( - ( Sum F))

    proof

      reconsider F1 = F as FinSequence of COMPLEX by Lm2;

      

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

      .= ( - ( Sum F1)) by BINOP_2:def 1

      .= ( - ( Sum F));

    end;

    theorem :: RVSUM_2:40

    

     Th40: ( Sum (R1 + R2)) = (( Sum R1) + ( Sum R2))

    proof

      reconsider T1 = R1, T2 = R2 as Element of (i -tuples_on COMPLEX ) by FINSEQ_2: 131;

      

      thus ( Sum (R1 + R2)) = ( addcomplex . (( addcomplex $$ T1),( addcomplex $$ T2))) by SETWOP_2: 35

      .= (( Sum R1) + ( Sum R2)) by BINOP_2:def 3;

    end;

    theorem :: RVSUM_2:41

    ( Sum (R1 - R2)) = (( Sum R1) - ( Sum R2))

    proof

      

      thus ( Sum (R1 - R2)) = (( Sum R1) + ( Sum ( - R2))) by Th40

      .= (( Sum R1) - ( Sum R2)) by Th39;

    end;

    begin

    

     Lm3: for F be empty FinSequence holds ( Product F) = 1

    proof

      ( Product ( <*> COMPLEX )) = 1 by BINOP_2: 6, FINSOP_1: 10;

      hence thesis;

    end;

    theorem :: RVSUM_2:42

    

     Th42: ( Product ( <*> COMPLEX )) = 1 by Lm3;

    registration

      let f be empty FinSequence;

      reduce (1 * ( Product f)) to 1;

      reducibility by Th42;

    end

    theorem :: RVSUM_2:43

    ( Product ( <*c*> ^ F)) = (c * ( Product F))

    proof

      

      thus ( Product ( <*c*> ^ F)) = (( Product <*c*>) * ( Product F)) by RVSUM_1: 97

      .= (c * ( Product F));

    end;

    theorem :: RVSUM_2:44

    for R be Element of ( 0 -tuples_on COMPLEX ) holds ( Product R) = 1 by Lm3;

    theorem :: RVSUM_2:45

    ( Product ((i + j) |-> c)) = (( Product (i |-> c)) * ( Product (j |-> c)))

    proof

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

      ( Product ((i + j) |-> s)) = ( multcomplex . (( multcomplex $$ (i |-> s)),( multcomplex $$ (j |-> s)))) by SETWOP_2: 26

      .= (( Product (i |-> s)) * ( Product (j |-> s))) by BINOP_2:def 5;

      hence thesis;

    end;

    theorem :: RVSUM_2:46

    ( Product ((i * j) |-> c)) = ( Product (j |-> ( Product (i |-> c))))

    proof

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

      ( Product ((i * j) |-> c)) = ( Product (j |-> ( Product (i |-> c)))) by SETWOP_2: 27;

      hence thesis;

    end;

    theorem :: RVSUM_2:47

    ( Product (i |-> (c1 * c2))) = (( Product (i |-> c1)) * ( Product (i |-> c2)))

    proof

      reconsider s1 = c1, s2 = c2, ss = (c1 * c2) as Element of COMPLEX by XCMPLX_0:def 2;

      ( multcomplex . (c1,c2)) = (c1 * c2) by BINOP_2:def 5;

      

      then ( Product (i |-> ss)) = ( multcomplex $$ (i |-> ( multcomplex . (s1,s2))))

      .= ( multcomplex . (( multcomplex $$ (i |-> s1)),( multcomplex $$ (i |-> s2)))) by SETWOP_2: 36

      .= (( Product (i |-> s1)) * ( Product (i |-> s2))) by BINOP_2:def 5;

      hence thesis;

    end;

    theorem :: RVSUM_2:48

    

     Th48: ( Product ( mlt (R1,R2))) = (( Product R1) * ( Product R2))

    proof

      reconsider T1 = R1, T2 = R2 as Element of (i -tuples_on COMPLEX ) by FINSEQ_2: 131;

      

      thus ( Product ( mlt (R1,R2))) = ( multcomplex . (( multcomplex $$ T1),( multcomplex $$ T2))) by SETWOP_2: 35

      .= (( Product R1) * ( Product R2)) by BINOP_2:def 5;

    end;

    theorem :: RVSUM_2:49

    ( Product (c * R)) = (( Product (i |-> c)) * ( Product R))

    proof

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

      

      thus ( Product (c * R)) = ( Product ( mlt ((i |-> s),R))) by Th27

      .= (( Product (i |-> c)) * ( Product R)) by Th48;

    end;

    begin

    theorem :: RVSUM_2:50

    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 :: RVSUM_2:51

    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 :: RVSUM_2:52

    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 :: RVSUM_2:53

    for a be Real, x be complex-valued FinSequence holds ( len (a * x)) = ( len x)

    proof

      let a be Real, 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;

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

      hence thesis;

    end;

    theorem :: RVSUM_2:54

    for x,y,z be complex-valued FinSequence 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 complex-valued FinSequence;

      

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

      assume ( len x) = ( len y) & ( len y) = ( len z);

      then

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

      

       A2: ( 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;

      

       A3: ( 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;

      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

         A4: 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

         A5: d = (a + b) by A2, A3, A4, VALUED_1:def 1;

        

        thus (( mlt ((x + y),z)) . i) = (d * e) by VALUED_1: 5

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

        .= ((( mlt (x,z)) . i) + (b * e)) by VALUED_1: 5

        .= ((( mlt (x,z)) . i) + (( mlt (y,z)) . i)) by VALUED_1: 5

        .= ((( mlt (x,z)) + ( mlt (y,z))) . i) by A2, A4, VALUED_1:def 1;

      end;

      hence thesis by A2, FINSEQ_1: 13;

    end;