rvsum_1.miz



    begin

    registration

      let n be natural Number;

      cluster n -element natural-valued for FinSequence;

      existence

      proof

        take (n |-> 0 );

        thus thesis;

      end;

    end

    registration

      cluster real-valued for FinSequence;

      existence

      proof

         the FinSequence of REAL is real-valued;

        hence thesis;

      end;

    end

    definition

      let F be real-valued Relation;

      :: original: rng

      redefine

      func rng F -> Subset of REAL ;

      coherence by VALUED_0:def 3;

    end

    registration

      let D be non empty set;

      let F be Function of REAL , D;

      let F1 be real-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) = REAL & ( rng F1) c= REAL by FUNCT_2:def 1;

        hence thesis by A1, RELAT_1: 27;

      end;

    end

    registration

      let r be Real;

      cluster <*r*> -> real-valued;

      coherence

      proof

        reconsider p = r as Element of REAL by XREAL_0:def 1;

         <*p*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2 be Real;

      cluster <*r1, r2*> -> real-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2 as Element of REAL by XREAL_0:def 1;

         <*p1, p2*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2,r3 be Real;

      cluster <*r1, r2, r3*> -> real-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2, p3 = r3 as Element of REAL by XREAL_0:def 1;

         <*p1, p2, p3*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2,r3,r4 be Real;

      cluster <*r1, r2, r3, r4*> -> real-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2, p3 = r3, p4 = r4 as Element of REAL by XREAL_0:def 1;

         <*p1, p2, p3, p4*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let j be natural Number, r be Real;

      cluster (j |-> r) -> real-valued;

      coherence ;

    end

    registration

      let f,g be real-valued FinSequence;

      cluster (f ^ g) -> real-valued;

      coherence

      proof

        ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

        then ( rng (f ^ g)) c= REAL by XBOOLE_1: 8;

        hence thesis by VALUED_0:def 3;

      end;

    end

    reserve s for set,

i,j for natural Number,

k for Nat,

x,x1,x2,x3 for Real,

r,r1,r2,r3,r4 for Real,

F,F1,F2,F3 for real-valued FinSequence,

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

    theorem :: RVSUM_1:1

     0 is_a_unity_wrt addreal by BINOP_2: 2, SETWISEO: 14;

    definition

      :: original: diffreal

      redefine

      :: RVSUM_1:def1

      func diffreal equals ( addreal * (( id REAL ), compreal ));

      compatibility

      proof

        let b be BinOp of REAL ;

        now

          let r1,r2 be Element of REAL ;

          

          thus ( diffreal . (r1,r2)) = (r1 - r2) by BINOP_2:def 10

          .= (r1 + ( - r2))

          .= ( addreal . (r1,( - r2))) by BINOP_2:def 9

          .= ( addreal . (r1,( compreal . r2))) by BINOP_2:def 7

          .= (( addreal * (( id REAL ), compreal )) . (r1,r2)) by FINSEQOP: 82;

        end;

        hence thesis;

      end;

      correctness ;

    end

    definition

      :: RVSUM_1:def2

      func sqrreal -> UnOp of REAL means

      : Def2: for r holds (it . r) = (r ^2 );

      existence

      proof

        deffunc F( Real) = ( In (($1 ^2 ), REAL ));

        consider G be Function of REAL , REAL such that

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

        take G;

        let r;

        r in REAL by XREAL_0:def 1;

        then (G . r) = F(r) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let G1,G2 be UnOp of REAL such that

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

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

        now

          let x be Element of REAL ;

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

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

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: RVSUM_1:2

    1 is_a_unity_wrt multreal by BINOP_2: 7, SETWISEO: 14;

    theorem :: RVSUM_1:3

    

     Th3: multreal is_distributive_wrt addreal

    proof

      now

        let x1,x2,x3 be Element of REAL ;

        

        thus ( multreal . (x1,( addreal . (x2,x3)))) = ( multreal . (x1,(x2 + x3))) by BINOP_2:def 9

        .= (x1 * (x2 + x3)) by BINOP_2:def 11

        .= ((x1 * x2) + (x1 * x3))

        .= ( addreal . ((x1 * x2),(x1 * x3))) by BINOP_2:def 9

        .= ( addreal . (( multreal . (x1,x2)),(x1 * x3))) by BINOP_2:def 11

        .= ( addreal . (( multreal . (x1,x2)),( multreal . (x1,x3)))) by BINOP_2:def 11;

        

        thus ( multreal . (( addreal . (x1,x2)),x3)) = ( multreal . ((x1 + x2),x3)) by BINOP_2:def 9

        .= ((x1 + x2) * x3) by BINOP_2:def 11

        .= ((x1 * x3) + (x2 * x3))

        .= ( addreal . ((x1 * x3),(x2 * x3))) by BINOP_2:def 9

        .= ( addreal . (( multreal . (x1,x3)),(x2 * x3))) by BINOP_2:def 11

        .= ( addreal . (( multreal . (x1,x3)),( multreal . (x2,x3)))) by BINOP_2:def 11;

      end;

      hence thesis by BINOP_1: 11;

    end;

    theorem :: RVSUM_1:4

     sqrreal is_distributive_wrt multreal

    proof

      let x1,x2 be Element of REAL ;

      

      thus ( sqrreal . ( multreal . (x1,x2))) = ( sqrreal . (x1 * x2)) by BINOP_2:def 11

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

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

      .= ( multreal . ((x1 ^2 ),(x2 ^2 ))) by BINOP_2:def 11

      .= ( multreal . (( sqrreal . x1),(x2 ^2 ))) by Def2

      .= ( multreal . (( sqrreal . x1),( sqrreal . x2))) by Def2;

    end;

    definition

      let x be Real;

      :: RVSUM_1:def3

      func x multreal -> UnOp of REAL equals ( multreal [;] (x,( id REAL )));

      coherence

      proof

        reconsider y = x as Element of REAL by XREAL_0:def 1;

        ( multreal [;] (y,( id REAL ))) is UnOp of REAL ;

        hence thesis;

      end;

    end

    

     Lm1: (( multreal [;] (r,( id REAL ))) . r1) = (r * r1)

    proof

      reconsider a = r, s = r1 as Element of REAL by XREAL_0:def 1;

      

      thus (( multreal [;] (r,( id REAL ))) . r1) = ( multreal . (a,(( id REAL ) . s))) by FUNCOP_1: 53

      .= ( multreal . (a,s))

      .= (r * r1) by BINOP_2:def 11;

    end;

    theorem :: RVSUM_1:5

    ((r multreal ) . r1) = (r * r1) by Lm1;

    theorem :: RVSUM_1:6

    (r multreal ) is_distributive_wrt addreal

    proof

      r in REAL by XREAL_0:def 1;

      hence thesis by Th3, FINSEQOP: 54;

    end;

    theorem :: RVSUM_1:7

    

     Th7: compreal is_an_inverseOp_wrt addreal

    proof

      let x be Element of REAL ;

      

      thus ( addreal . (x,( compreal . x))) = (x + ( compreal . x)) by BINOP_2:def 9

      .= (x + ( - x)) by BINOP_2:def 7

      .= ( the_unity_wrt addreal ) by BINOP_2: 2;

      

      thus ( addreal . (( compreal . x),x)) = (( compreal . x) + x) by BINOP_2:def 9

      .= (( - x) + x) by BINOP_2:def 7

      .= ( the_unity_wrt addreal ) by BINOP_2: 2;

    end;

    theorem :: RVSUM_1:8

    

     Th8: addreal is having_an_inverseOp by Th7;

    theorem :: RVSUM_1:9

    

     Th9: ( the_inverseOp_wrt addreal ) = compreal by Th7, Th8, FINSEQOP:def 3;

    theorem :: RVSUM_1:10

     compreal is_distributive_wrt addreal by Th8, Th9, FINSEQOP: 63;

    

     Lm2: F is FinSequence of REAL

    proof

      thus ( rng F) c= REAL ;

    end;

    definition

      let F1, F2;

      :: original: +

      redefine

      :: RVSUM_1:def4

      func F1 + F2 -> FinSequence of REAL equals ( addreal .: (F1,F2));

      coherence by Lm2;

      compatibility

      proof

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

        let F be FinSequence of REAL ;

        ( dom addreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

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

        then

         A1: ( dom ( addreal .: (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 = ( addreal .: (F1,F2))

        proof

          assume

           A3: F = (F1 + F2);

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

          proof

            let z be set;

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

            

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

            .= ( addreal . ((F1 . z),(F2 . z))) by BINOP_2:def 9;

          end;

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

        end;

        assume

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

        now

          let c be object;

          assume c in ( dom F);

          

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

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

        end;

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

      end;

      commutativity

      proof

        let F be FinSequence of REAL ;

        let F1, F2;

        assume

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

        reconsider F1, F2 as FinSequence of REAL by Lm2;

        

         A6: ( dom addreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

        then

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

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

        

        then

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

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

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

        proof

          let z be set;

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

          

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

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

          .= ( addreal . ((F2 . z),(F1 . z))) by BINOP_2:def 9;

        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 REAL ) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_1: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 qua Element of NAT + 0 qua Element of NAT ) by FUNCT_1:def 2

        .= ((R1 . s) + 0 qua Element of NAT ) 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_1:12

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

    proof

      F is FinSequence of REAL by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_1:13

    ( <*r1*> + <*r2*>) = <*(r1 + r2)*>

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= <*(r1 + r2)*> by BINOP_2:def 9;

      hence thesis;

    end;

    theorem :: RVSUM_1:14

    ((i |-> r1) + (i |-> r2)) = (i |-> (r1 + r2))

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> (r1 + r2)) by BINOP_2:def 9;

      hence thesis;

    end;

    theorem :: RVSUM_1:15

    (F1 + (F2 + F3)) = ((F1 + F2) + F3) by RFUNCT_1: 8;

    theorem :: RVSUM_1:16

    (R + (i |-> 0 qua Real)) = R by BINOP_2: 2, FINSEQOP: 56;

    theorem :: RVSUM_1:17

    (( - F) . s) = ( - (F . s)) by VALUED_1: 8;

    definition

      let F;

      :: original: -

      redefine

      :: RVSUM_1:def5

      func - F -> FinSequence of REAL equals ( compreal * F);

      coherence by Lm2;

      compatibility

      proof

        let F1 be FinSequence of REAL ;

        

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

        

         A2: ( rng F) c= REAL & ( dom compreal ) = REAL by FUNCT_2:def 1;

        then

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

        thus F1 = ( - F) implies F1 = ( compreal * 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

            .= ( compreal . (F . c)) by BINOP_2:def 7

            .= (( compreal * 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 = ( compreal * F);

        now

          let c be object;

          assume

           A7: c in ( dom F1);

          

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

          .= ( compreal . (F . c)) by BINOP_2:def 7

          .= (( compreal * 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 REAL ) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: RVSUM_1:18

    (( - F) . s) = ( - (F . s)) by VALUED_1: 8;

    theorem :: RVSUM_1:19

    ( - ( <*> REAL )) = ( <*> REAL );

    theorem :: RVSUM_1:20

    ( - <*r*>) = <*( - r)*>

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

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

      .= <*( - r)*> by BINOP_2:def 7;

      hence thesis;

    end;

    theorem :: RVSUM_1:21

    

     Th21: ( - (i |-> r)) = (i |-> ( - r))

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> ( - r)) by BINOP_2:def 7;

      hence thesis;

    end;

    theorem :: RVSUM_1:22

    (R + ( - R)) = (i |-> 0 ) by Th8, Th9, BINOP_2: 2, FINSEQOP: 73;

    theorem :: RVSUM_1:23

    (R1 + R2) = (i |-> 0 ) implies R1 = ( - R2) by Th8, Th9, BINOP_2: 2, FINSEQOP: 74;

    theorem :: RVSUM_1:24

    for R1,R2 be complex-valued Function st ( - R1) = ( - R2) holds R1 = R2

    proof

      let R1,R2 be complex-valued Function;

      assume ( - R1) = ( - R2);

      

      hence R1 = ( - ( - R2))

      .= R2;

    end;

    theorem :: RVSUM_1:25

    (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 |-> 0 ) by Th8, Th9, BINOP_2: 2, FINSEQOP: 73;

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

      hence thesis by BINOP_2: 2, FINSEQOP: 56;

    end;

    theorem :: RVSUM_1:26

    

     Th26: ( - (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 be Nat;

        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_1:def6

      func F1 - F2 -> FinSequence of REAL equals ( diffreal .: (F1,F2));

      coherence by Lm2;

      compatibility

      proof

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

        let F be FinSequence of REAL ;

        

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

        ( dom diffreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

        then

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

        then

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

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

        proof

          assume

           A4: F = (F1 - F2);

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

          proof

            let z be set;

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

            

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

            .= ( diffreal . ((F1 . z),(F2 . z))) by BINOP_2:def 10;

          end;

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

        end;

        assume

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

        now

          let c be object;

          assume c in ( dom F);

          

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

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

        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 REAL ) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_1:27

    ((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 qua Element of NAT - 0 qua Element of NAT ) by FUNCT_1:def 2

        .= ((R1 . s) - 0 qua Element of NAT ) 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_1:28

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

    proof

      F is FinSequence of REAL by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_1:29

    ( <*r1*> - <*r2*>) = <*(r1 - r2)*>

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= <*(r1 - r2)*> by BINOP_2:def 10;

      hence thesis;

    end;

    theorem :: RVSUM_1:30

    ((i |-> r1) - (i |-> r2)) = (i |-> (r1 - r2))

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> (r1 - r2)) by BINOP_2:def 10;

      hence thesis;

    end;

    theorem :: RVSUM_1:31

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

    theorem :: RVSUM_1:32

    (R - (i |-> 0 qua Real)) = R

    proof

      

      thus (R - (i |-> 0 qua Real)) = (R + (i |-> ( - 0 qua Element of NAT ))) by Th21

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

    end;

    theorem :: RVSUM_1:33

    ((i |-> 0 qua Real) - R) = ( - R) by BINOP_2: 2, FINSEQOP: 56;

    theorem :: RVSUM_1:34

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

    theorem :: RVSUM_1:35

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

    proof

      

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

      .= (F2 - F1);

    end;

    theorem :: RVSUM_1:36

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

    proof

      

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

      .= (( - F1) + F2);

    end;

    theorem :: RVSUM_1:37

    (R - R) = (i |-> 0 ) by Th8, Th9, BINOP_2: 2, FINSEQOP: 73;

    theorem :: RVSUM_1:38

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

    proof

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

      then R1 = ( - ( - R2)) by Th8, Th9, BINOP_2: 2, FINSEQOP: 74;

      hence thesis;

    end;

    theorem :: RVSUM_1:39

    ((F1 - F2) - F3) = (F1 - (F2 + F3)) by RFUNCT_1: 20;

    theorem :: RVSUM_1:40

    (F1 + (F2 - F3)) = ((F1 + F2) - F3) by RFUNCT_1: 23;

    theorem :: RVSUM_1:41

    (F1 - (F2 - F3)) = ((F1 - F2) + F3) by RFUNCT_1: 22;

    theorem :: RVSUM_1:42

    R1 = ((R1 + R) - R)

    proof

      

      thus R1 = (R1 + (i |-> 0 qua Real)) by BINOP_2: 2, FINSEQOP: 56

      .= (R1 + (R - R)) by Th8, Th9, BINOP_2: 2, FINSEQOP: 73

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

    end;

    theorem :: RVSUM_1:43

    R1 = ((R1 - R) + R)

    proof

      

      thus R1 = (R1 + (i |-> 0 qua Real)) by BINOP_2: 2, FINSEQOP: 56

      .= (R1 + (( - R) + R)) by Th8, Th9, BINOP_2: 2, FINSEQOP: 73

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

    end;

    notation

      let F;

      let r be Real;

      synonym r * F for r (#) F;

    end

    theorem :: RVSUM_1:44

    ((r * F) . s) = (r * (F . s)) by VALUED_1: 6;

    definition

      let F;

      let r be Real;

      :: original: *

      redefine

      :: RVSUM_1:def7

      func r * F -> FinSequence of REAL equals ((r multreal ) * F);

      coherence by Lm2;

      compatibility

      proof

        let F1 be FinSequence of REAL ;

        

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

        

         A2: ( rng F) c= REAL & ( dom (r multreal )) = REAL by FUNCT_2:def 1;

        then

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

        thus F1 = (r * F) implies F1 = ((r multreal ) * F)

        proof

          assume

           A4: F1 = (r * F);

          now

            let c be object;

            assume

             A5: c in ( dom F1);

            

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

            .= ((r multreal ) . (F . c)) by Lm1

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

          end;

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

        end;

        assume

         A6: F1 = ((r multreal ) * F);

        now

          let c be object;

          assume

           A7: c in ( dom F1);

          

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

          .= ((r multreal ) . (F . c)) by Lm1

          .= (((r multreal ) * 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, r;

      :: original: *

      redefine

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

      coherence by FINSEQ_2: 113;

    end

    theorem :: RVSUM_1:45

    ((r * F) . s) = (r * (F . s)) by VALUED_1: 6;

    theorem :: RVSUM_1:46

    (r * ( <*> REAL )) = ( <*> REAL );

    theorem :: RVSUM_1:47

    (r * <*r1*>) = <*(r * r1)*>

    proof

      reconsider s = r, s1 = r1 as Element of REAL by XREAL_0:def 1;

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

      .= <*(r * r1)*> by Lm1;

      hence thesis;

    end;

    theorem :: RVSUM_1:48

    

     Th48: (r1 * (i |-> r2)) = (i |-> (r1 * r2))

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> (r1 * r2)) by Lm1;

      hence thesis;

    end;

    theorem :: RVSUM_1:49

    ((r1 * r2) * F) = (r1 * (r2 * F)) by RFUNCT_1: 17;

    theorem :: RVSUM_1:50

    ((r1 + r2) * F) = ((r1 * F) + (r2 * F))

    proof

      

       A1: ( dom ((r1 + r2) * F)) = ( dom F) by VALUED_1:def 5;

      

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

      

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

      

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

      now

        let i be Nat;

        assume

         A5: i in ( dom ((r1 + r2) * F));

        

        thus (((r1 + r2) * F) . i) = ((r1 + r2) * (F . i)) by VALUED_1: 6

        .= ((r1 * (F . i)) + (r2 * (F . i)))

        .= ((r1 * (F . i)) + ((r2 * F) . i)) by VALUED_1: 6

        .= (((r1 * F) . i) + ((r2 * F) . i)) by VALUED_1: 6

        .= (((r1 * F) + (r2 * 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_1:51

    (r * (F1 + F2)) = ((r * F1) + (r * F2)) by RFUNCT_1: 16;

    theorem :: RVSUM_1:52

    (1 * F) = F by RFUNCT_1: 21;

    theorem :: RVSUM_1:53

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

    proof

      

       A1: ( rng R) c= REAL ;

      

      thus ( 0 * R) = ( multreal [;] ( 0 ,(( id REAL ) * R))) by FUNCOP_1: 34

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

      .= (i |-> 0 ) by Th3, Th8, BINOP_2: 2, FINSEQOP: 76;

    end;

    theorem :: RVSUM_1:54

    (( - 1) * F) = ( - F);

    notation

      let F;

      synonym sqr F for F ^2 ;

    end

    definition

      let F;

      :: original: sqr

      redefine

      :: RVSUM_1:def8

      func sqr F -> FinSequence of REAL equals ( sqrreal * F);

      compatibility

      proof

        let f be FinSequence of REAL ;

        ( sqr F) = ( sqrreal * F)

        proof

          ( dom sqrreal ) = REAL by FUNCT_2:def 1;

          then

           A1: ( rng F) c= ( dom sqrreal );

          

           A2: ( dom ( sqr F)) = ( dom F) by VALUED_1: 11

          .= ( dom ( sqrreal * F)) by A1, RELAT_1: 27;

          hence ( len ( sqr F)) = ( len ( sqrreal * F)) by FINSEQ_3: 29;

          let k;

          assume 1 <= k & k <= ( len ( sqr F));

          then

           A3: k in ( dom ( sqr F)) by FINSEQ_3: 25;

          

          thus (( sqr F) . k) = ((F . k) ^2 ) by VALUED_1: 11

          .= ( sqrreal . (F . k)) by Def2

          .= (( sqrreal * F) . k) by A2, A3, FUNCT_1: 12;

        end;

        hence thesis;

      end;

      coherence by Lm2;

    end

    definition

      let i, R;

      :: original: sqr

      redefine

      func sqr R -> Element of (i -tuples_on REAL ) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: RVSUM_1:55

    ( sqr <*r*>) = <*(r ^2 )*>

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      ( sqr <*s*>) = <*( sqrreal . s)*> by FINSEQ_2: 35

      .= <*(r ^2 )*> by Def2;

      hence thesis;

    end;

    theorem :: RVSUM_1:56

    ( sqr (i |-> r)) = (i |-> (r ^2 ))

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> (r ^2 )) by Def2;

      hence thesis;

    end;

    theorem :: RVSUM_1:57

    

     Th57: ( sqr ( - F)) = ( sqr F)

    proof

      

       A1: ( dom ( sqr ( - F))) = ( dom ( - F)) by VALUED_1: 11

      .= ( dom F) by VALUED_1: 8;

      

       A2: ( dom ( sqr F)) = ( dom F) by VALUED_1: 11;

      now

        let j be Nat;

        assume j in ( dom ( sqr ( - F)));

        set r = (F . j), r9 = (( - F) . j);

        

        thus (( sqr ( - F)) . j) = (r9 ^2 ) by VALUED_1: 11

        .= (( - r) ^2 ) by VALUED_1: 8

        .= (r ^2 )

        .= (( sqr F) . j) by VALUED_1: 11;

      end;

      hence thesis by A1, A2, FINSEQ_1: 13;

    end;

    theorem :: RVSUM_1:58

    

     Th58: ( sqr (r * F)) = ((r ^2 ) * ( sqr F))

    proof

      

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

      

       A2: ( dom ((r ^2 ) * ( sqr F))) = ( dom ( sqr F)) by VALUED_1:def 5;

      

       A3: ( dom ( sqr F)) = ( dom F) by VALUED_1: 11;

      now

        let i be Nat;

        assume i in ( dom ( sqr (r * F)));

        

        thus (( sqr (r * F)) . i) = (((r * F) . i) ^2 ) by VALUED_1: 11

        .= ((r * (F . i)) ^2 ) by VALUED_1: 6

        .= ((r ^2 ) * ((F . i) ^2 ))

        .= ((r ^2 ) * (( sqr F) . i)) by VALUED_1: 11

        .= (((r ^2 ) * ( sqr F)) . i) by VALUED_1: 6;

      end;

      hence thesis by A1, A2, A3, FINSEQ_1: 13, VALUED_1: 11;

    end;

    notation

      let F1, F2;

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

    end

    definition

      let F1, F2;

      :: original: mlt

      redefine

      :: RVSUM_1:def9

      func mlt (F1,F2) -> FinSequence of REAL equals ( multreal .: (F1,F2));

      coherence by Lm2;

      compatibility

      proof

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

        let F be FinSequence of REAL ;

        ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

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

        then

         A1: ( dom ( multreal .: (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 = ( multreal .: (F1,F2))

        proof

          assume

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

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

          proof

            let z be set;

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

            

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

            .= ( multreal . ((F1 . z),(F2 . z))) by BINOP_2:def 11;

          end;

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

        end;

        assume

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

        now

          let c be object;

          assume c in ( dom F);

          

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

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

        end;

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

      end;

      commutativity

      proof

        let F be FinSequence of REAL ;

        let F1, F2;

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

        

         A5: ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

        then

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

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

        

        then

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

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

        assume

         A8: F = ( multreal .: (F1,F2));

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

        proof

          let z be set such that

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

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

          

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

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

          .= ( multreal . ((F2 . z),(F1 . z))) by BINOP_2:def 11;

        end;

        hence thesis by A8, A7, FUNCOP_1: 21;

      end;

    end

    theorem :: RVSUM_1:59

    (( mlt (F1,F2)) . s) = ((F1 . s) * (F2 . s)) by VALUED_1: 5;

    definition

      let i, R1, R2;

      :: original: mlt

      redefine

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

      coherence by FINSEQ_2: 120;

    end

    theorem :: RVSUM_1:60

    (( mlt (F1,F2)) . s) = ((F1 . s) * (F2 . s)) by VALUED_1: 5;

    theorem :: RVSUM_1:61

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

    proof

      F is FinSequence of REAL by Lm2;

      hence thesis by FINSEQ_2: 73;

    end;

    theorem :: RVSUM_1:62

    ( mlt ( <*r1*>, <*r2*>)) = <*(r1 * r2)*>

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= <*(r1 * r2)*> by BINOP_2:def 11;

      hence thesis;

    end;

    theorem :: RVSUM_1:63

    

     Th63: ( mlt ((i |-> r),R)) = (r * R)

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:64

    ( mlt ((i |-> r1),(i |-> r2))) = (i |-> (r1 * r2))

    proof

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

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

      .= (i |-> (r1 * r2)) by Th48;

      hence thesis;

    end;

    theorem :: RVSUM_1:65

    (r * ( mlt (F1,F2))) = ( mlt ((r * F1),F2)) by RFUNCT_1: 12;

    theorem :: RVSUM_1:66

    (r * R) = ( mlt ((i |-> r),R)) by Th63;

    theorem :: RVSUM_1:67

    ( sqr F) = ( mlt (F,F));

    theorem :: RVSUM_1:68

    

     Th68: ( sqr (F1 + F2)) = ((( sqr F1) + (2 * ( mlt (F1,F2)))) + ( sqr F2))

    proof

      

       A1: ( dom ( sqr (F1 + F2))) = ( dom (F1 + F2)) by VALUED_1: 11;

      

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

      

       A3: ( dom (( sqr F1) + (2 * ( mlt (F1,F2))))) = (( dom ( sqr F1)) /\ ( dom (2 * ( mlt (F1,F2))))) by VALUED_1:def 1

      .= (( dom F1) /\ ( dom (2 * ( mlt (F1,F2))))) by VALUED_1: 11

      .= (( dom F1) /\ ( dom ( mlt (F1,F2)))) by VALUED_1:def 5

      .= (( dom F1) /\ (( dom F1) /\ ( dom F2))) by VALUED_1:def 4

      .= ((( dom F1) /\ ( dom F1)) /\ ( dom F2)) by XBOOLE_1: 16

      .= (( dom F1) /\ ( dom F2));

      

      then

       A4: ( dom ((( sqr F1) + (2 * ( mlt (F1,F2)))) + ( sqr F2))) = ((( dom F1) /\ ( dom F2)) /\ ( dom ( sqr F2))) by VALUED_1:def 1

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

      .= (( dom F1) /\ (( dom F2) /\ ( dom F2))) by XBOOLE_1: 16;

      now

        let j be Nat;

        assume

         A5: j in ( dom ( sqr (F1 + F2)));

        set r1r2 = ((F1 + F2) . j), r1 = (F1 . j), r2 = (F2 . j), r192 = (( sqr F1) . j), r292 = (( sqr F2) . j), r1r2a = (( mlt (F1,F2)) . j), 2r1r2 = ((2 * ( mlt (F1,F2))) . j), r1922r1r2 = ((( sqr F1) + (2 * ( mlt (F1,F2)))) . j);

        

        thus (( sqr (F1 + F2)) . j) = (r1r2 ^2 ) by VALUED_1: 11

        .= ((r1 + r2) ^2 ) by A1, A5, VALUED_1:def 1

        .= (((r1 ^2 ) + ((2 * r1) * r2)) + (r2 ^2 ))

        .= ((r192 + (2 * (r1 * r2))) + (r2 ^2 )) by VALUED_1: 11

        .= ((r192 + (2 * (r1 * r2))) + r292) by VALUED_1: 11

        .= ((r192 + (2 * r1r2a)) + r292) by VALUED_1: 5

        .= ((r192 + 2r1r2) + r292) by VALUED_1: 6

        .= (r1922r1r2 + r292) by A1, A2, A3, A5, VALUED_1:def 1

        .= (((( sqr F1) + (2 * ( mlt (F1,F2)))) + ( sqr F2)) . j) by A1, A2, A4, A5, VALUED_1:def 1;

      end;

      hence thesis by A2, A4, FINSEQ_1: 13, VALUED_1: 11;

    end;

    theorem :: RVSUM_1:69

    

     Th69: ( sqr (F1 - F2)) = ((( sqr F1) - (2 * ( mlt (F1,F2)))) + ( sqr F2))

    proof

      

      thus ( sqr (F1 - F2)) = ((( sqr F1) + (2 * ( mlt (F1,( - F2))))) + ( sqr ( - F2))) by Th68

      .= ((( sqr F1) + (2 * ( mlt (F1,( - F2))))) + ( sqr F2)) by Th57

      .= ((( sqr F1) + (2 * (( - 1) * ( mlt (F1,F2))))) + ( sqr F2)) by RFUNCT_1: 12

      .= ((( sqr F1) + ((( - 1) * 2) * ( mlt (F1,F2)))) + ( sqr F2)) by RFUNCT_1: 17

      .= ((( sqr F1) - (2 * ( mlt (F1,F2)))) + ( sqr F2)) by RFUNCT_1: 17;

    end;

    theorem :: RVSUM_1:70

    ( sqr ( mlt (F1,F2))) = ( mlt (( sqr F1),( sqr F2)))

    proof

      

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

      

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

      

       A3: ( dom ( sqr F1)) = ( dom F1) by VALUED_1: 11;

      

       A4: ( dom ( sqr F2)) = ( dom F2) by VALUED_1: 11;

      now

        let i be Nat;

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

        

        thus (( sqr ( mlt (F1,F2))) . i) = ((( mlt (F1,F2)) . i) ^2 ) by VALUED_1: 11

        .= (((F1 . i) * (F2 . i)) ^2 ) by VALUED_1: 5

        .= (((F1 . i) ^2 ) * ((F2 . i) ^2 ))

        .= ((( sqr F1) . i) * ((F2 . i) ^2 )) by VALUED_1: 11

        .= ((( sqr F1) . i) * (( sqr F2) . i)) by VALUED_1: 11

        .= (( mlt (( sqr F1),( sqr F2))) . i) by VALUED_1: 5;

      end;

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

    end;

    registration

      cluster -> complex-valued for FinSequence of COMPLEX ;

      coherence ;

      cluster real-valued complex-valued for FinSequence;

      existence

      proof

        ( <*> REAL ) is real-valued;

        hence thesis;

      end;

    end

    definition

      let F be complex-valued FinSequence;

      :: RVSUM_1:def10

      func Sum F -> Complex means

      : Def10: ex f be FinSequence of COMPLEX st f = F & it = ( addcomplex $$ f);

      existence

      proof

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

        then

        reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;

        take ( addcomplex $$ f);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be real-valued FinSequence;

      cluster ( Sum F) -> real;

      coherence

      proof

        set mc = addcomplex ;

        consider f be FinSequence of COMPLEX such that

         A1: f = F and

         A2: ( Sum F) = ( addcomplex $$ f) by Def10;

        set g = ( [#] (f,( the_unity_wrt mc)));

        defpred P[ Nat] means (mc $$ (( finSeg $1),( [#] (f,( the_unity_wrt mc))))) is real;

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A4: P[k];

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (g . (k + 1)) is real

          proof

            per cases ;

              suppose (k + 1) in ( dom f);

              then (g . (k + 1)) = (f . (k + 1)) by SETWOP_2: 20;

              hence thesis by A1;

            end;

              suppose not (k + 1) in ( dom f);

              hence thesis by BINOP_2: 1, SETWOP_2: 20;

            end;

          end;

          then

          reconsider a = (g . (k + 1)), b = (mc $$ (( finSeg k),g)) as Real by A4;

           not (k + 1) in ( Seg k) by FINSEQ_3: 8;

          

          then (mc $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),g)) = (mc . ((mc $$ (( finSeg k),g)),(g . (k + 1)))) by SETWOP_2: 2

          .= (b + a) by BINOP_2:def 3;

          hence thesis by FINSEQ_1: 9;

        end;

        

         A5: (mc $$ f) = (mc $$ (( findom f),( [#] (f,( the_unity_wrt mc))))) & ex n be Nat st ( dom f) = ( Seg n) by FINSEQ_1:def 2, SETWOP_2:def 2;

        ( Seg 0 ) = ( {}. NAT );

        then

         A6: P[ 0 ] by BINOP_2: 1, SETWISEO: 31;

        for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

        hence thesis by A2, A5;

      end;

    end

    theorem :: RVSUM_1:71

    

     Th71: for F be FinSequence of REAL holds ( Sum F) = ( addreal $$ F)

    proof

      set g = addreal , h = addcomplex ;

      let F be FinSequence of REAL ;

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

      then

      reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;

      defpred P[ Nat] means (g $$ (( finSeg $1),( [#] (F,( the_unity_wrt g))))) = (h $$ (( finSeg $1),( [#] (f,( the_unity_wrt h)))));

      consider n be Nat such that

       A1: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

      

       A2: (g $$ F) = (g $$ (( finSeg n),( [#] (F,( the_unity_wrt g))))) & (h $$ f) = (h $$ (( finSeg n),( [#] (f,( the_unity_wrt h))))) by A1, SETWOP_2:def 2;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        set j = ( [#] (f,( the_unity_wrt h)));

        set i = ( [#] (F,( the_unity_wrt g)));

        let k be Nat;

        assume

         A4: P[k];

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A5: (i . (k + 1)) = (j . (k + 1))

        proof

          per cases ;

            suppose

             A6: (k + 1) in ( dom f);

            

            then (j . (k + 1)) = (F . (k + 1)) by SETWOP_2: 20

            .= (i . (k + 1)) by A6, SETWOP_2: 20;

            hence thesis;

          end;

            suppose

             A7: not (k + 1) in ( dom f);

            

            then (j . (k + 1)) = ( the_unity_wrt h) by SETWOP_2: 20

            .= (i . (k + 1)) by A7, BINOP_2: 1, BINOP_2: 2, SETWOP_2: 20;

            hence thesis;

          end;

        end;

        

         A8: not (k + 1) in ( Seg k) by FINSEQ_3: 8;

        (g $$ (( finSeg (k + 1)),i)) = (g $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),i)) by FINSEQ_1: 9

        .= (g . ((g $$ (( finSeg k),i)),(i . (k + 1)))) by A8, SETWOP_2: 2

        .= ((g $$ (( finSeg k),i)) + (i . (k + 1))) by BINOP_2:def 9

        .= (h . ((h $$ (( finSeg k),j)),(j . (k + 1)))) by A4, A5, BINOP_2:def 3

        .= (h $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),j)) by A8, SETWOP_2: 2

        .= (h $$ (( finSeg (k + 1)),j)) by FINSEQ_1: 9;

        hence thesis;

      end;

      

       A9: ( Seg 0 ) = ( {}. NAT );

      

      then (g $$ (( finSeg 0 ),( [#] (F,( the_unity_wrt g))))) = ( the_unity_wrt h) by BINOP_2: 1, BINOP_2: 2, SETWISEO: 31

      .= (h $$ (( finSeg 0 ),( [#] (f,( the_unity_wrt h))))) by A9, SETWISEO: 31;

      then

       A10: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A10, A3);

      then (g $$ F) = (h $$ f) by A2;

      hence thesis by Def10;

    end;

    definition

      let F be FinSequence of COMPLEX ;

      :: original: Sum

      redefine

      :: RVSUM_1:def11

      func Sum F -> Element of COMPLEX equals ( addcomplex $$ F);

      coherence by XCMPLX_0:def 2;

      compatibility by Def10;

    end

    definition

      let F be FinSequence of REAL ;

      :: original: Sum

      redefine

      :: RVSUM_1:def12

      func Sum F -> Real equals ( addreal $$ F);

      coherence ;

      compatibility by Th71;

    end

    theorem :: RVSUM_1:72

    

     Th72: ( Sum ( <*> REAL )) = 0 by BINOP_2: 2, FINSOP_1: 10;

    theorem :: RVSUM_1:73

    ( Sum <*r*>) = r

    proof

      reconsider r as Element of REAL by XREAL_0:def 1;

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

      hence thesis;

    end;

    theorem :: RVSUM_1:74

    

     Th74: ( Sum (F ^ <*r*>)) = (( Sum F) + r)

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      reconsider F1 = F as FinSequence of REAL by Lm2;

      

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

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

      .= (( Sum F1) + r) by BINOP_2:def 9

      .= (( Sum F) + r);

    end;

    theorem :: RVSUM_1:75

    

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

    proof

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

      

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

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

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

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

    end;

    theorem :: RVSUM_1:76

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

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      

      thus ( Sum ( <*r*> ^ F)) = (( Sum <*s*>) + ( Sum F)) by Th75

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

    end;

    theorem :: RVSUM_1:77

    

     Th77: ( Sum <*r1, r2*>) = (r1 + r2)

    proof

      reconsider s1 = r1 as Element of REAL by XREAL_0:def 1;

      

      thus ( Sum <*r1, r2*>) = (( Sum <*s1*>) + r2) by Th74

      .= (r1 + r2) by FINSOP_1: 11;

    end;

    theorem :: RVSUM_1:78

    

     Th78: ( Sum <*r1, r2, r3*>) = ((r1 + r2) + r3)

    proof

      

      thus ( Sum <*r1, r2, r3*>) = (( Sum <*r1, r2*>) + r3) by Th74

      .= ((r1 + r2) + r3) by Th77;

    end;

    theorem :: RVSUM_1:79

    for R be Element of ( 0 -tuples_on REAL ) holds ( Sum R) = 0 by Th72;

    theorem :: RVSUM_1:80

    

     Th80: ( Sum (i |-> r)) = (i * r)

    proof

      

       A0: i is Nat by TARSKI: 1;

      reconsider r as Element of REAL by XREAL_0:def 1;

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

      

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

      proof

        let i be Nat such that

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

        

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

        .= ((i * r) + (1 * r)) by A2, Th74

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

      end;

      

       A3: P[ 0 ] by Th72;

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

      hence thesis by A0;

    end;

    theorem :: RVSUM_1:81

    

     Th81: ( Sum (i |-> 0 qua Real)) = 0

    proof

      

      thus ( Sum (i |-> 0 qua Real)) = (i * 0 qua Element of NAT ) by Th80

      .= 0 ;

    end;

    

     Lm: for R1 be i -element real-valued FinSequence holds R1 is Element of (i -tuples_on REAL )

    proof

      let R1 be i -element real-valued FinSequence;

      

       A1: R1 is FinSequence of REAL by Lm2;

      ( len R1) = i by CARD_1:def 7;

      hence thesis by A1, FINSEQ_2: 92;

    end;

    theorem :: RVSUM_1:82

    

     Th82: for R1,R2 be i -element real-valued FinSequence holds (for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j)) implies ( Sum R1) <= ( Sum R2)

    proof

      let R1,R2 be i -element real-valued FinSequence;

      

       A0: i is Nat by TARSKI: 1;

      defpred P[ Nat] means for R1,R2 be $1 -element real-valued FinSequence st for j be Nat st j in ( Seg $1) holds (R1 . j) <= (R2 . j) holds ( Sum R1) <= ( Sum R2);

      

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

      proof

        let i be Nat such that

         A2: for R1,R2 be i -element real-valued FinSequence st for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j) holds ( Sum R1) <= ( Sum R2);

        set n = (i + 1);

        let R1,R2 be n -element real-valued FinSequence such that

         A3: for j be Nat st j in ( Seg n) holds (R1 . j) <= (R2 . j);

        R1 is Element of (n -tuples_on REAL ) by Lm;

        then

        consider R19 be Element of (i -tuples_on REAL ), x1 be Element of REAL such that

         A4: R1 = (R19 ^ <*x1*>) by FINSEQ_2: 117;

        R2 is Element of (n -tuples_on REAL ) by Lm;

        then

        consider R29 be Element of (i -tuples_on REAL ), x2 be Element of REAL such that

         A5: R2 = (R29 ^ <*x2*>) by FINSEQ_2: 117;

        for j be Nat st j in ( Seg i) holds (R19 . j) <= (R29 . j)

        proof

          let j be Nat such that

           A6: j in ( Seg i);

          ( Seg ( len R29)) = ( dom R29) & ( len R29) = i by CARD_1:def 7, FINSEQ_1:def 3;

          then

           A7: (R29 . j) = (R2 . j) by A5, A6, FINSEQ_1:def 7;

          ( Seg ( len R19)) = ( dom R19) & ( len R19) = i by CARD_1:def 7, FINSEQ_1:def 3;

          then (R19 . j) = (R1 . j) by A4, A6, FINSEQ_1:def 7;

          hence thesis by A3, A6, A7, FINSEQ_2: 8;

        end;

        then

         A8: ( Sum R19) <= ( Sum R29) by A2;

        

         A9: (R2 . n) = x2 by A5, FINSEQ_2: 116;

        (R1 . n) = x1 by A4, FINSEQ_2: 116;

        then

         A10: x1 <= x2 by A3, A9, FINSEQ_1: 4;

        

         A11: ( Sum R2) = (( Sum R29) + x2) by A5, Th74;

        ( Sum R1) = (( Sum R19) + x1) by A4, Th74;

        hence thesis by A10, A8, A11, XREAL_1: 7;

      end;

      

       A12: P[ 0 ];

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

      hence thesis by A0;

    end;

    theorem :: RVSUM_1:83

    

     Th83: for R1,R2 be i -element real-valued FinSequence holds (for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j)) & (ex j be Nat st j in ( Seg i) & (R1 . j) < (R2 . j)) implies ( Sum R1) < ( Sum R2)

    proof

      let R1,R2 be i -element real-valued FinSequence;

      

       A0: i is Nat by TARSKI: 1;

      defpred P[ Nat] means for R1,R2 be $1 -element real-valued FinSequence st (for j be Nat st j in ( Seg $1) holds (R1 . j) <= (R2 . j)) & (ex j be Nat st j in ( Seg $1) & (R1 . j) < (R2 . j)) holds ( Sum R1) < ( Sum R2);

      now

        let i be Nat such that

         A1: P[i];

        let R1,R2 be (i + 1) -element real-valued FinSequence such that

         A2: for j be Nat st j in ( Seg (i + 1)) holds (R1 . j) <= (R2 . j);

        given j be Nat such that

         A3: j in ( Seg (i + 1)) and

         A4: (R1 . j) < (R2 . j);

        R1 is Element of ((i + 1) -tuples_on REAL ) by Lm;

        then

        consider R19 be Element of (i -tuples_on REAL ), x1 be Element of REAL such that

         A5: R1 = (R19 ^ <*x1*>) by FINSEQ_2: 117;

        R2 is Element of ((i + 1) -tuples_on REAL ) by Lm;

        then

        consider R29 be Element of (i -tuples_on REAL ), x2 be Element of REAL such that

         A6: R2 = (R29 ^ <*x2*>) by FINSEQ_2: 117;

        

         A7: for j be Nat st j in ( Seg i) holds (R19 . j) <= (R29 . j)

        proof

          let j be Nat such that

           A8: j in ( Seg i);

          ( Seg ( len R29)) = ( dom R29) & ( len R29) = i by CARD_1:def 7, FINSEQ_1:def 3;

          then

           A9: (R29 . j) = (R2 . j) by A6, A8, FINSEQ_1:def 7;

          ( Seg ( len R19)) = ( dom R19) & ( len R19) = i by CARD_1:def 7, FINSEQ_1:def 3;

          then (R19 . j) = (R1 . j) by A5, A8, FINSEQ_1:def 7;

          hence thesis by A2, A8, A9, FINSEQ_2: 8;

        end;

        

         A10: (R2 . (i + 1)) = x2 by A6, FINSEQ_2: 116;

        

         A11: (R1 . (i + 1)) = x1 by A5, FINSEQ_2: 116;

        now

          per cases by A3, FINSEQ_2: 7;

            suppose

             A12: j in ( Seg i);

            ( Seg ( len R29)) = ( dom R29) & ( len R29) = i by CARD_1:def 7, FINSEQ_1:def 3;

            then

             A13: (R29 . j) = (R2 . j) by A6, A12, FINSEQ_1:def 7;

            

             A14: ( Sum R1) = (( Sum R19) + x1) & ( Sum R2) = (( Sum R29) + x2) by A5, A6, Th74;

            

             A15: x1 <= x2 by A2, A11, A10, FINSEQ_1: 4;

            ( Seg ( len R19)) = ( dom R19) & ( len R19) = i by CARD_1:def 7, FINSEQ_1:def 3;

            then (R19 . j) = (R1 . j) by A5, A12, FINSEQ_1:def 7;

            then ( Sum R19) < ( Sum R29) by A1, A4, A7, A12, A13;

            hence ( Sum R1) < ( Sum R2) by A14, A15, XREAL_1: 8;

          end;

            suppose

             A16: j = (i + 1);

            

             A17: ( Sum R2) = (( Sum R29) + x2) by A6, Th74;

            ( Sum R19) <= ( Sum R29) & ( Sum R1) = (( Sum R19) + x1) by A5, A7, Th74, Th82;

            hence ( Sum R1) < ( Sum R2) by A4, A11, A10, A16, A17, XREAL_1: 8;

          end;

        end;

        hence ( Sum R1) < ( Sum R2);

      end;

      then

       A18: for i be Nat st P[i] holds P[(i + 1)];

      

       A19: P[ 0 ];

      for i be Nat holds P[i] from NAT_1:sch 2( A19, A18);

      hence thesis by A0;

    end;

    theorem :: RVSUM_1:84

    

     Th84: (for i be Nat st i in ( dom F) holds 0 <= (F . i)) implies 0 <= ( Sum F)

    proof

      reconsider F1 = F as FinSequence of REAL by Lm2;

      set i = ( len F);

      set R1 = (i |-> ( In ( 0 , REAL )));

      reconsider R2 = F1 as Element of (i -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

      assume

       A2: for i be Nat st i in ( dom F) holds 0 <= (F . i);

      for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j)

      proof

        let j be Nat;

        assume

         A3: j in ( Seg i);

        (R1 . j) = ( In ( 0 , REAL ));

        hence thesis by A2, A1, A3;

      end;

      then ( Sum R1) <= ( Sum R2) by Th82;

      hence thesis by Th81;

    end;

    theorem :: RVSUM_1:85

    

     Th85: (for i be Nat st i in ( dom F) holds 0 <= (F . i)) & (ex i be Nat st i in ( dom F) & 0 < (F . i)) implies 0 < ( Sum F)

    proof

      reconsider F1 = F as FinSequence of REAL by Lm2;

      set i = ( len F), R1 = (i |-> ( In ( 0 , REAL )));

      reconsider R2 = F1 as Element of (i -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

      assume

       A2: for i be Nat st i in ( dom F) holds 0 <= (F . i);

      

       A3: for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j)

      proof

        let j be Nat;

        (R1 . j) = ( In ( 0 , REAL ));

        hence thesis by A2, A1;

      end;

      given j be Nat such that

       A4: j in ( dom F) and

       A5: 0 < (F . j);

      (R1 . j) = 0 ;

      then ( Sum R1) < ( Sum R2) by A1, A3, A4, A5, Th83;

      hence thesis by Th81;

    end;

    theorem :: RVSUM_1:86

    

     Th86: 0 <= ( Sum ( sqr F))

    proof

      now

        let i be Nat such that i in ( dom ( sqr F));

         0 <= ((F . i) ^2 ) by XREAL_1: 63;

        hence 0 <= (( sqr F) . i) by VALUED_1: 11;

      end;

      hence thesis by Th84;

    end;

    theorem :: RVSUM_1:87

    

     Th87: ( Sum (r * F)) = (r * ( Sum F))

    proof

      reconsider F1 = F as FinSequence of REAL by Lm2;

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      set rM = ( multreal [;] (s,( id REAL )));

      

      thus ( Sum (r * F)) = (rM . ( addreal $$ F1)) by Th3, Th8, SETWOP_2: 30

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

      .= (r * ( Sum F));

    end;

    theorem :: RVSUM_1:88

    

     Th88: ( Sum ( - F)) = ( - ( Sum F))

    proof

      reconsider F1 = F as FinSequence of REAL by Lm2;

      

      thus ( Sum ( - F)) = ( compreal . ( addreal $$ F1)) by Th8, Th9, SETWOP_2: 31

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

      .= ( - ( Sum F));

    end;

    theorem :: RVSUM_1:89

    

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

    proof

      i is Nat by TARSKI: 1;

      

      hence ( Sum (R1 + R2)) = ( addreal . (( addreal $$ R1),( addreal $$ R2))) by SETWOP_2: 35

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

    end;

    theorem :: RVSUM_1:90

    

     Th90: ( Sum (R1 - R2)) = (( Sum R1) - ( Sum R2))

    proof

      

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

      .= (( Sum R1) + ( - ( Sum R2))) by Th88

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

    end;

    theorem :: RVSUM_1:91

    ( Sum ( sqr R)) = 0 implies R = (i |-> 0 )

    proof

      assume

       A1: ( Sum ( sqr R)) = 0 ;

      

       A2: ( len R) = i by CARD_1:def 7;

      

       A3: ( len (i |-> 0 )) = i by CARD_1:def 7;

      assume R <> (i |-> 0 );

      then

      consider j be Nat such that

       A4: j in ( dom R) and

       A5: (R . j) <> ((i |-> 0 ) . j) by A2, A3, FINSEQ_2: 9;

      set x = (R . j), x9 = (( sqr R) . j);

      

       A6: ( dom R) = ( Seg ( len R)) by FINSEQ_1:def 3;

      x <> 0 by A5;

      then 0 < (x ^2 ) by SQUARE_1: 12;

      then

       A7: 0 < x9 by VALUED_1: 11;

       A8:

      now

        let k such that k in ( dom ( sqr R));

        set r = (( sqr R) . k);

        set x = (R . k);

         0 <= (x ^2 ) by XREAL_1: 63;

        hence 0 <= r by VALUED_1: 11;

      end;

      ( dom ( sqr R)) = ( Seg ( len ( sqr R))) by FINSEQ_1:def 3;

      then j in ( dom ( sqr R)) by A4, A6, FINSEQ_2: 33;

      hence thesis by A1, A8, A7, Th85;

    end;

    theorem :: RVSUM_1:92

    (( Sum ( mlt (R1,R2))) ^2 ) <= (( Sum ( sqr R1)) * ( Sum ( sqr R2)))

    proof

      

       A0: i is Nat by TARSKI: 1;

      defpred P[ Nat] means for R1,R2 be Element of ($1 -tuples_on REAL ) holds (( Sum ( mlt (R1,R2))) ^2 ) <= (( Sum ( sqr R1)) * ( Sum ( sqr R2)));

      

       A1: for c be Nat st P[c] holds P[(c + 1)]

      proof

        let c be Nat such that

         A2: for R1,R2 be Element of (c -tuples_on REAL ) holds (( Sum ( mlt (R1,R2))) ^2 ) <= (( Sum ( sqr R1)) * ( Sum ( sqr R2)));

        let R1,R2 be Element of ((c + 1) -tuples_on REAL );

        consider R19 be Element of (c -tuples_on REAL ), x1 be Element of REAL such that

         A3: R1 = (R19 ^ <*x1*>) by FINSEQ_2: 117;

        consider R29 be Element of (c -tuples_on REAL ), x2 be Element of REAL such that

         A4: R2 = (R29 ^ <*x2*>) by FINSEQ_2: 117;

        

         A5: for R be Element of (c -tuples_on REAL ) holds ( Sum ( sqr (R ^ <*r*>))) = (( Sum ( sqr R)) + (r ^2 ))

        proof

          let R be Element of (c -tuples_on REAL );

          reconsider s = r as Element of REAL by XREAL_0:def 1;

          ( sqr (R ^ <*s*>)) = (( sqrreal * R) ^ <*( sqrreal . s)*>) by FINSEQOP: 8

          .= (( sqr R) ^ <*(r ^2 )*>) by Def2;

          hence thesis by Th74;

        end;

        

        then

         A6: (( Sum ( sqr R29)) + (x2 ^2 )) = ( Sum ( sqr (R29 ^ <*x2*>)))

        .= ( Sum ( sqr R2)) by A4;

        ((( Sum ( mlt (R19,R29))) ^2 ) + 0 qua Element of NAT ) <= (( Sum ( sqr R19)) * ( Sum ( sqr R29))) by A2;

        then

         A7: 0 <= ((( Sum ( sqr R19)) * ( Sum ( sqr R29))) - (( Sum ( mlt (R19,R29))) ^2 )) by XREAL_1: 19;

        ( mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>))) = (( multreal .: (R19,R29)) ^ <*( multreal . (x1,x2))*>) by FINSEQOP: 10

        .= (( mlt (R19,R29)) ^ <*(x1 * x2)*>) by BINOP_2:def 11;

        then

         A8: ( Sum ( mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>)))) = (( Sum ( mlt (R19,R29))) + (x1 * x2)) by Th74;

        

         A9: ((2 * (x1 * x2)) * ( Sum ( mlt (R19,R29)))) = (2 * ((x1 * x2) * ( Sum ( mlt (R19,R29)))))

        .= (2 * ( Sum ((x1 * x2) * ( mlt (R19,R29))))) by Th87

        .= (2 * ( Sum (x1 * (x2 * ( mlt (R19,R29)))))) by RFUNCT_1: 17

        .= (2 * ( Sum (x1 * ( mlt (R29,(x2 * R19)))))) by RFUNCT_1: 12

        .= (2 * ( Sum ( mlt ((x1 * R29),(x2 * R19))))) by FINSEQOP: 26;

        

         A10: ( - ((( Sum ( mlt (R19,R29))) + (x1 * x2)) ^2 )) = (( - ((x1 * x2) ^2 )) + ( - (((2 * (x1 * x2)) * ( Sum ( mlt (R19,R29)))) + (( Sum ( mlt (R19,R29))) ^2 ))))

        .= (( - ((x1 ^2 ) * (x2 ^2 ))) + (( - (( Sum ( mlt (R19,R29))) ^2 )) + ( - (2 * ( Sum ( mlt ((x1 * R29),(x2 * R19)))))))) by A9;

        

         A11: 0 <= ( Sum ( sqr ((x1 * R29) - (x2 * R19)))) by Th86;

        

         A12: ((( Sum ( sqr R19)) + (x1 ^2 )) * (( Sum ( sqr R29)) + (x2 ^2 ))) = (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + (((x1 ^2 ) * ( Sum ( sqr R29))) + (( Sum ( sqr R19)) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 )))

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + (( Sum ((x1 ^2 ) * ( sqr R29))) + (( Sum ( sqr R19)) * (x2 ^2 )))) + ((x1 ^2 ) * (x2 ^2 ))) by Th87

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + (( Sum ( sqr (x1 * R29))) + ((x2 ^2 ) * ( Sum ( sqr R19))))) + ((x1 ^2 ) * (x2 ^2 ))) by Th58

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + (( Sum ( sqr (x1 * R29))) + ( Sum ((x2 ^2 ) * ( sqr R19))))) + ((x1 ^2 ) * (x2 ^2 ))) by Th87

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + (( Sum ( sqr (x1 * R29))) + ( Sum ( sqr (x2 * R19))))) + ((x1 ^2 ) * (x2 ^2 ))) by Th58;

        

         A13: ((( Sum ( sqr (x1 * R29))) + ( Sum ( sqr (x2 * R19)))) + ( - (2 * ( Sum ( mlt ((x1 * R29),(x2 * R19))))))) = ((( Sum ( sqr (x1 * R29))) - (2 * ( Sum ( mlt ((x1 * R29),(x2 * R19)))))) + ( Sum ( sqr (x2 * R19))))

        .= ((( Sum ( sqr (x1 * R29))) - ( Sum (2 * ( mlt ((x1 * R29),(x2 * R19)))))) + ( Sum ( sqr (x2 * R19)))) by Th87

        .= (( Sum (( sqr (x1 * R29)) - (2 * ( mlt ((x1 * R29),(x2 * R19)))))) + ( Sum ( sqr (x2 * R19)))) by Th90

        .= ( Sum ((( sqr (x1 * R29)) - (2 * ( mlt ((x1 * R29),(x2 * R19))))) + ( sqr (x2 * R19)))) by Th89;

        (( Sum ( sqr R19)) + (x1 ^2 )) = ( Sum ( sqr R1)) by A3, A5;

        

        then ((( Sum ( sqr R1)) * ( Sum ( sqr R2))) - (( Sum ( mlt (R1,R2))) ^2 )) = (((( Sum ( sqr R19)) + (x1 ^2 )) * (( Sum ( sqr R29)) + (x2 ^2 ))) + ( - ((( Sum ( mlt (R19,R29))) + (x1 * x2)) ^2 ))) by A3, A4, A8, A6

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) + ( - (( Sum ( mlt (R19,R29))) ^2 ))) + ((( Sum ( sqr (x1 * R29))) + ( Sum ( sqr (x2 * R19)))) + ( - (2 * ( Sum ( mlt ((x1 * R29),(x2 * R19)))))))) by A12, A10

        .= (((( Sum ( sqr R19)) * ( Sum ( sqr R29))) - (( Sum ( mlt (R19,R29))) ^2 )) + ( Sum ( sqr ((x1 * R29) - (x2 * R19))))) by A13, Th69;

        then ((( Sum ( mlt (R1,R2))) ^2 ) + 0 qua Element of NAT ) <= (( Sum ( sqr R1)) * ( Sum ( sqr R2))) by A7, A11, XREAL_1: 19;

        hence thesis;

      end;

      

       A14: P[ 0 ];

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

      hence thesis by A0;

    end;

    definition

      let F be complex-valued FinSequence;

      :: RVSUM_1:def13

      func Product F -> Complex means

      : Def13: ex f be FinSequence of COMPLEX st f = F & it = ( multcomplex $$ f);

      existence

      proof

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

        then

        reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;

        take ( multcomplex $$ f);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be real-valued FinSequence;

      cluster ( Product F) -> real;

      coherence

      proof

        set mc = multcomplex ;

        consider f be FinSequence of COMPLEX such that

         A1: f = F and

         A2: ( Product F) = ( multcomplex $$ f) by Def13;

        set g = ( [#] (f,( the_unity_wrt mc)));

        defpred P[ Nat] means (mc $$ (( finSeg $1),( [#] (f,( the_unity_wrt mc))))) is real;

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A4: P[k];

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (g . (k + 1)) is real

          proof

            per cases ;

              suppose (k + 1) in ( dom f);

              then (g . (k + 1)) = (f . (k + 1)) by SETWOP_2: 20;

              hence thesis by A1;

            end;

              suppose not (k + 1) in ( dom f);

              hence thesis by BINOP_2: 6, SETWOP_2: 20;

            end;

          end;

          then

          reconsider a = (g . (k + 1)), b = (mc $$ (( finSeg k),g)) as Real by A4;

           not (k + 1) in ( Seg k) by FINSEQ_3: 8;

          

          then (mc $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),g)) = (mc . ((mc $$ (( finSeg k),g)),(g . (k + 1)))) by SETWOP_2: 2

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

          hence thesis by FINSEQ_1: 9;

        end;

        

         A5: (mc $$ f) = (mc $$ (( findom f),( [#] (f,( the_unity_wrt mc))))) & ex n be Nat st ( dom f) = ( Seg n) by FINSEQ_1:def 2, SETWOP_2:def 2;

        ( Seg 0 ) = ( {}. NAT );

        then

         A6: P[ 0 ] by BINOP_2: 6, SETWISEO: 31;

        for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

        hence thesis by A2, A5;

      end;

    end

    theorem :: RVSUM_1:93

    

     Th93: for F be FinSequence of REAL holds ( Product F) = ( multreal $$ F)

    proof

      set g = multreal , h = multcomplex ;

      let F be FinSequence of REAL ;

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

      then

      reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;

      defpred P[ Nat] means (g $$ (( finSeg $1),( [#] (F,( the_unity_wrt g))))) = (h $$ (( finSeg $1),( [#] (f,( the_unity_wrt h)))));

      consider n be Nat such that

       A1: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

      

       A2: (g $$ F) = (g $$ (( finSeg n),( [#] (F,( the_unity_wrt g))))) & (h $$ f) = (h $$ (( finSeg n),( [#] (f,( the_unity_wrt h))))) by A1, SETWOP_2:def 2;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        set j = ( [#] (f,( the_unity_wrt h)));

        set i = ( [#] (F,( the_unity_wrt g)));

        let k be Nat;

        assume

         A4: P[k];

        

         A5: (i . (k + 1)) = (j . (k + 1))

        proof

          per cases ;

            suppose

             A6: (k + 1) in ( dom f);

            

            then (j . (k + 1)) = (F . (k + 1)) by SETWOP_2: 20

            .= (i . (k + 1)) by A6, SETWOP_2: 20;

            hence thesis;

          end;

            suppose

             A7: not (k + 1) in ( dom f);

            

            then (j . (k + 1)) = ( the_unity_wrt h) by SETWOP_2: 20

            .= (i . (k + 1)) by A7, BINOP_2: 6, BINOP_2: 7, SETWOP_2: 20;

            hence thesis;

          end;

        end;

        

         A8: not (k + 1) in ( Seg k) by FINSEQ_3: 8;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        (g $$ (( finSeg (k + 1)),i)) = (g $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),i)) by FINSEQ_1: 9

        .= (g . ((g $$ (( finSeg k),i)),(i . (k + 1)))) by A8, SETWOP_2: 2

        .= ((g $$ (( finSeg k),i)) * (i . (k + 1))) by BINOP_2:def 11

        .= (h . ((h $$ (( finSeg k),j)),(j . (k + 1)))) by A4, A5, BINOP_2:def 5

        .= (h $$ ((( finSeg k) \/ {.( In ((k + 1), NAT )).}),j)) by A8, SETWOP_2: 2

        .= (h $$ (( finSeg (k + 1)),j)) by FINSEQ_1: 9;

        hence thesis;

      end;

      

       A9: ( Seg 0 ) = ( {}. NAT );

      

      then (g $$ (( finSeg 0 ),( [#] (F,( the_unity_wrt g))))) = ( the_unity_wrt h) by BINOP_2: 6, BINOP_2: 7, SETWISEO: 31

      .= (h $$ (( finSeg 0 ),( [#] (f,( the_unity_wrt h))))) by A9, SETWISEO: 31;

      then

       A10: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A10, A3);

      then (g $$ F) = (h $$ f) by A2;

      hence thesis by Def13;

    end;

    definition

      let F be FinSequence of COMPLEX ;

      :: original: Product

      redefine

      :: RVSUM_1:def14

      func Product F -> Element of COMPLEX equals ( multcomplex $$ F);

      coherence by XCMPLX_0:def 2;

      compatibility by Def13;

    end

    definition

      let F be FinSequence of REAL ;

      :: original: Product

      redefine

      :: RVSUM_1:def15

      func Product F -> Real equals ( multreal $$ F);

      coherence ;

      compatibility by Th93;

    end

    

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

    proof

      ( Product ( <*> REAL )) = 1 by BINOP_2: 7, FINSOP_1: 10;

      hence thesis;

    end;

    theorem :: RVSUM_1:94

    

     Th94: ( Product ( <*> REAL )) = 1 by Lm3;

    registration

      let r be Complex;

      cluster <*r*> -> complex-valued;

      coherence

      proof

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

        reconsider f = <*p*> as FinSequence of COMPLEX ;

        f is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2 be Complex;

      cluster <*r1, r2*> -> complex-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2 as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider f = <*p1, p2*> as FinSequence of COMPLEX ;

        f is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2,r3 be Complex;

      cluster <*r1, r2, r3*> -> complex-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2, p3 = r3 as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider f = <*p1, p2, p3*> as FinSequence of COMPLEX ;

        f is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let j be natural Number, c be Complex;

      cluster (j |-> c) -> complex-valued;

      coherence ;

    end

    theorem :: RVSUM_1:95

    

     Th95: for r be Complex holds ( Product <*r*>) = r

    proof

      let r be Complex;

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

      reconsider F = <*r9*> as FinSequence of COMPLEX ;

      ( multcomplex $$ F) = r by FINSOP_1: 11;

      hence thesis by Def13;

    end;

    registration

      let c be Complex;

      reduce ( Product <*c*>) to c;

      reducibility by Th95;

    end

    registration

      let f,g be complex-valued FinSequence;

      cluster (f ^ g) -> complex-valued;

      coherence

      proof

        

         A1: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

        ( rng f) c= COMPLEX & ( rng g) c= COMPLEX by VALUED_0:def 1;

        then ( rng (f ^ g)) c= COMPLEX by A1, XBOOLE_1: 8;

        hence thesis by VALUED_0:def 1;

      end;

    end

    theorem :: RVSUM_1:96

    

     Th96: for F be complex-valued FinSequence, r be Complex holds ( Product (F ^ <*r*>)) = (( Product F) * r)

    proof

      let F be complex-valued FinSequence, r be Complex;

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

      ( rng F) c= COMPLEX & ( rng (F ^ <*p*>)) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider Fr = (F ^ <*r*>), Ff = F as FinSequence of COMPLEX by FINSEQ_1:def 4;

      

      thus ( Product (F ^ <*r*>)) = ( multcomplex $$ Fr) by Def13

      .= ( multcomplex . (( Product Ff),p)) by FINSOP_1: 4

      .= (( Product F) * r) by BINOP_2:def 5;

    end;

    theorem :: RVSUM_1:97

    

     Th97: for F1,F2 be complex-valued FinSequence holds ( Product (F1 ^ F2)) = (( Product F1) * ( Product F2))

    proof

      let F1,F2 be complex-valued FinSequence;

      

       A1: ( rng (F1 ^ F2)) c= COMPLEX by VALUED_0:def 1;

      ( rng F1) c= COMPLEX & ( rng F2) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider FF = (F1 ^ F2), f1 = F1, f2 = F2 as FinSequence of COMPLEX by A1, FINSEQ_1:def 4;

      

      thus ( Product (F1 ^ F2)) = ( multcomplex $$ FF) by Def13

      .= ( multcomplex . (( Product f1),( Product f2))) by FINSOP_1: 5

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

    end;

    theorem :: RVSUM_1:98

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

    proof

      

      thus ( Product ( <*r*> ^ F)) = (( Product <*r*>) * ( Product F)) by Th97

      .= (r * ( Product F));

    end;

    theorem :: RVSUM_1:99

    

     Th99: for r1,r2 be Complex holds ( Product <*r1, r2*>) = (r1 * r2)

    proof

      let r1,r2 be Complex;

      

      thus ( Product <*r1, r2*>) = (( Product <*r1*>) * r2) by Th96

      .= (r1 * r2);

    end;

    theorem :: RVSUM_1:100

    for r1,r2,r3 be Complex holds ( Product <*r1, r2, r3*>) = ((r1 * r2) * r3)

    proof

      let r1,r2,r3 be Complex;

      

      thus ( Product <*r1, r2, r3*>) = (( Product <*r1, r2*>) * r3) by Th96

      .= ((r1 * r2) * r3) by Th99;

    end;

    theorem :: RVSUM_1:101

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

    theorem :: RVSUM_1:102

    ( Product (i |-> 1)) = 1

    proof

      i is Nat by TARSKI: 1;

      then ( Product (i |-> ( the_unity_wrt multreal ))) = ( the_unity_wrt multreal ) by SETWOP_2: 25;

      hence thesis by BINOP_2: 7;

    end;

    

     Lm4: for p be complex-valued FinSequence st ( len p) <> 0 holds ex q be complex-valued FinSequence, d be Complex st p = (q ^ <*d*>)

    proof

      let p be complex-valued FinSequence;

      assume ( len p) <> 0 ;

      then

      consider q be FinSequence, d be object such that

       A1: p = (q ^ <*d*>) by CARD_1: 27, FINSEQ_1: 46;

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

      then

       A2: p is FinSequence of COMPLEX by FINSEQ_1:def 4;

      for i be Nat st i in ( dom q) holds (q . i) in COMPLEX

      proof

        let i be Nat;

        assume i in ( dom q);

        then (p . i) = (q . i) & i in ( dom p) by A1, FINSEQ_1:def 7, FINSEQ_2: 15;

        hence thesis by A2, FINSEQ_2: 11;

      end;

      then

       A3: q is FinSequence of COMPLEX by FINSEQ_2: 12;

      ( len p) = (( len q) + 1) by A1, FINSEQ_2: 16;

      then (p . ( len p)) = d by A1, FINSEQ_1: 42;

      hence thesis by A1, A3;

    end;

    theorem :: RVSUM_1:103

    for F be complex-valued FinSequence holds (ex k st k in ( dom F) & (F . k) = 0 ) iff ( Product F) = 0

    proof

      defpred P[ Nat] means for F be complex-valued FinSequence st ( len F) = $1 holds (ex k st k in ( Seg $1) & (F . k) = 0 ) iff ( Product F) = 0 ;

      let F be complex-valued FinSequence;

      

       A1: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

      

       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A3: for F be complex-valued FinSequence st ( len F) = i holds (ex k st k in ( Seg i) & (F . k) = 0 ) iff ( Product F) = 0 ;

        let F be complex-valued FinSequence;

        assume

         A4: ( len F) = (i + 1);

        then

        consider F9 be complex-valued FinSequence, x be Complex such that

         A5: F = (F9 ^ <*x*>) by Lm4;

        

         A6: ( len F) = (( len F9) + 1) by A5, FINSEQ_2: 16;

        

         A7: ( Product F) = (( Product F9) * x) by A5, Th96;

        thus (ex k st k in ( Seg (i + 1)) & (F . k) = 0 ) implies ( Product F) = 0

        proof

          given k such that

           A8: k in ( Seg (i + 1)) and

           A9: (F . k) = 0 ;

          now

            per cases by A8, FINSEQ_2: 7;

              suppose

               A10: k in ( Seg i);

              ( Seg ( len F9)) = ( dom F9) by FINSEQ_1:def 3;

              then (F9 . k) = (F . k) by A4, A5, A6, A10, FINSEQ_1:def 7;

              then ( Product F9) = 0 by A3, A4, A6, A9, A10;

              hence thesis by A7;

            end;

              suppose k = (i + 1);

              then x = 0 by A4, A5, A6, A9, FINSEQ_1: 42;

              hence thesis by A7;

            end;

          end;

          hence thesis;

        end;

        assume

         A11: ( Product F) = 0 ;

        per cases by A7, A11;

          suppose ( Product F9) = 0 ;

          then

          consider k such that

           A12: k in ( Seg i) and

           A13: (F9 . k) = 0 by A3, A4, A6;

          ( Seg ( len F9)) = ( dom F9) by FINSEQ_1:def 3;

          then (F . k) = 0 by A4, A5, A6, A12, A13, FINSEQ_1:def 7;

          hence thesis by A12, FINSEQ_2: 8;

        end;

          suppose x = 0 ;

          then (F . (i + 1)) = 0 by A4, A5, A6, FINSEQ_1: 42;

          hence thesis by FINSEQ_1: 4;

        end;

      end;

      

       A14: P[ 0 ]

      proof

        let F be complex-valued FinSequence;

        assume ( len F) = 0 ;

        then F = ( <*> COMPLEX );

        hence thesis by Th94;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A14, A2);

      hence thesis by A1;

    end;

    theorem :: RVSUM_1:104

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

    proof

      reconsider i, j as Nat by TARSKI: 1;

      reconsider s = r as Element of REAL by XREAL_0:def 1;

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:105

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

    proof

      reconsider r as Element of REAL by XREAL_0:def 1;

      reconsider pr = ( Product (i |-> r)) as Element of REAL ;

      i is Nat & j is Nat by TARSKI: 1;

      then ( Product ((i * j) |-> r)) = ( Product (j |-> pr)) by SETWOP_2: 27;

      hence thesis;

    end;

    theorem :: RVSUM_1:106

    ( Product (i |-> (r1 * r2))) = (( Product (i |-> r1)) * ( Product (i |-> r2)))

    proof

      reconsider i as Nat by TARSKI: 1;

      reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;

      reconsider ss = (s1 * s2) as Element of REAL ;

      ( Product (i |-> ss)) = ( multreal $$ (i |-> ( multreal . (s1,s2)))) by BINOP_2:def 11

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:107

    

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

    proof

      i is Nat by TARSKI: 1;

      

      hence ( Product ( mlt (R1,R2))) = ( multreal . (( multreal $$ R1),( multreal $$ R2))) by SETWOP_2: 35

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

    end;

    theorem :: RVSUM_1:108

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

    proof

      reconsider s = r as Element of REAL by XREAL_0:def 1;

      

      thus ( Product (r * R)) = ( Product ( mlt ((i |-> s),R))) by Th63

      .= (( Product (i |-> r)) * ( Product R)) by Th107;

    end;

    theorem :: RVSUM_1:109

    ( Product ( sqr R)) = (( Product R) ^2 ) by Th107;

    begin

    reserve z,z1,z2 for Element of COMPLEX ;

    theorem :: RVSUM_1:110

    for F be FinSequence of COMPLEX holds ( Product F) = ( multcomplex $$ F);

    theorem :: RVSUM_1:111

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

    proof

      reconsider i, j as Nat by TARSKI: 1;

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:112

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

    proof

      i is Nat & j is Nat by TARSKI: 1;

      hence thesis by SETWOP_2: 27;

    end;

    

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

    proof

      let F be complex-valued FinSequence;

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

    end;

    theorem :: RVSUM_1:113

    ( Product (i |-> (z1 * z2))) = (( Product (i |-> z1)) * ( Product (i |-> z2)))

    proof

      reconsider i as Nat by TARSKI: 1;

      reconsider zz = (i |-> (z1 * z2)) as FinSequence of COMPLEX by Lm5;

      ( Product (i |-> (z1 * z2))) = ( Product zz)

      .= ( multcomplex $$ (i |-> ( multcomplex . (z1,z2)))) by BINOP_2:def 5

      .= ( multcomplex . (( multcomplex $$ (i |-> z1)),( multcomplex $$ (i |-> z2)))) by SETWOP_2: 36

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

      hence thesis;

    end;

    begin

    reserve n for Nat,

x,y,a for Real,

p,p1,p2,p3,q,q1,q2 for Element of (n -tuples_on REAL );

    theorem :: RVSUM_1:114

    

     Th114: for x be real-valued FinSequence holds ( len ( - x)) = ( len x)

    proof

      let x be real-valued FinSequence;

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

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: RVSUM_1:115

    

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

    proof

      let x1,x2 be real-valued FinSequence;

      set n = ( len x1);

      

       A1: x2 is FinSequence of REAL by Lm2;

      x1 is FinSequence of REAL by Lm2;

      then

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

      assume ( len x1) = ( len x2);

      then

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

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

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: RVSUM_1:116

    

     Th116: for x1,x2 be real-valued FinSequence st ( len x1) = ( len x2) holds ( len (x1 - x2)) = ( len x1)

    proof

      let x1,x2 be real-valued FinSequence;

      set n = ( len x1);

      

       A1: x2 is FinSequence of REAL by Lm2;

      x1 is FinSequence of REAL by Lm2;

      then

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

      assume ( len x1) = ( len x2);

      then

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

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

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: RVSUM_1:117

    

     Th117: for a be Real, x be real-valued FinSequence holds ( len (a * x)) = ( len x)

    proof

      let a be Real, x be real-valued FinSequence;

      set n = ( len x);

      x is FinSequence of REAL by Lm2;

      then

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:118

    

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

      

       A1: x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL 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 REAL ) 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;

    begin

    definition

      let x1,x2 be real-valued FinSequence;

      :: RVSUM_1:def16

      func |(x1,x2)| -> Real equals ( Sum ( mlt (x1,x2)));

      correctness ;

      commutativity ;

    end

    theorem :: RVSUM_1:119

    

     Th119: for x be real-valued FinSequence holds |(x, x)| >= 0

    proof

      let x be real-valued FinSequence;

      set n = ( len x);

      x is FinSequence of REAL by Lm2;

      then

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

       |(x, x)| = ( Sum ( sqr w));

      hence thesis by Th86;

    end;

    theorem :: RVSUM_1:120

    

     Th120: for x,y,z be real-valued FinSequence st ( len x) = ( len y) & ( len y) = ( len z) holds |((x + y), z)| = ( |(x, z)| + |(y, z)|)

    proof

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

      

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

      assume

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

      then

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

       |((x + y), z)| = ( Sum (( mlt (x,z)) + ( mlt (y,z)))) by A2, Th118

      .= (( Sum ( mlt (x2,z2))) + ( Sum ( mlt (y2,z2)))) by Th89

      .= ( |(x, z)| + |(y, z)|);

      hence thesis;

    end;

    theorem :: RVSUM_1:121

    

     Th121: for x,y be real-valued FinSequence, a be Real st ( len x) = ( len y) holds |((a * x), y)| = (a * |(x, y)|)

    proof

      let x,y be real-valued FinSequence, a be Real;

      reconsider a2 = a as Element of REAL by XREAL_0:def 1;

      

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

      assume ( len x) = ( len y);

      then

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

       |((a * x), y)| = ( Sum (a2 * ( mlt (x2,y2)))) by FINSEQOP: 26

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

      hence thesis;

    end;

    theorem :: RVSUM_1:122

    

     Th122: for x1,x2 be real-valued FinSequence st ( len x1) = ( len x2) holds |(( - x1), x2)| = ( - |(x1, x2)|)

    proof

      let x1,x2 be real-valued FinSequence;

      assume ( len x1) = ( len x2);

      then |(( - x1), x2)| = (( - 1) * |(x1, x2)|) by Th121;

      hence thesis;

    end;

    theorem :: RVSUM_1:123

    for x1,x2 be real-valued FinSequence st ( len x1) = ( len x2) holds |(( - x1), ( - x2))| = |(x1, x2)|

    proof

      let x1,x2 be real-valued FinSequence;

      assume

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

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

      

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:124

    

     Th124: for x1,x2,x3 be real-valued FinSequence st ( len x1) = ( len x2) & ( len x2) = ( len x3) holds |((x1 - x2), x3)| = ( |(x1, x3)| - |(x2, x3)|)

    proof

      let x1,x2,x3 be real-valued FinSequence;

      assume that

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

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

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

      

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:125

    for x,y be Real, x1,x2,x3 be real-valued FinSequence st ( len x1) = ( len x2) & ( len x2) = ( len x3) holds |(((x * x1) + (y * x2)), x3)| = ((x * |(x1, x3)|) + (y * |(x2, x3)|))

    proof

      let x,y be Real, x1,x2,x3 be real-valued FinSequence;

      assume that

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

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

      ( len (x * x1)) = ( len x1) & ( len (y * x2)) = ( len x2) by Th117;

      

      then |(((x * x1) + (y * x2)), x3)| = ( |((x * x1), x3)| + |((y * x2), x3)|) by A1, A2, Th120

      .= ((x * |(x1, x3)|) + |((y * x2), x3)|) by A1, A2, Th121

      .= ((x * |(x1, x3)|) + (y * |(x2, x3)|)) by A2, Th121;

      hence thesis;

    end;

    theorem :: RVSUM_1:126

    

     Th126: for x1,x2,y1,y2 be real-valued FinSequence 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 real-valued FinSequence;

      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, Th120;

      then

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

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

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

    end;

    theorem :: RVSUM_1:127

    

     Th127: for x1,x2,y1,y2 be real-valued FinSequence 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 real-valued FinSequence;

      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, Th124;

      then

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

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

      hence thesis by A1, A2, A4, Th124;

    end;

    theorem :: RVSUM_1:128

    for x,y be real-valued FinSequence st ( len x) = ( len y) holds |((x + y), (x + y))| = (( |(x, x)| + (2 * |(x, y)|)) + |(y, y)|)

    proof

      let x,y be real-valued FinSequence;

      

       A1: (( |(x, x)| + |(x, y)|) + |(x, y)|) = ( |(x, x)| + (2 * |(x, y)|));

      assume ( len x) = ( len y);

      hence thesis by A1, Th126;

    end;

    theorem :: RVSUM_1:129

    for x,y be real-valued FinSequence st ( len x) = ( len y) holds |((x - y), (x - y))| = (( |(x, x)| - (2 * |(x, y)|)) + |(y, y)|)

    proof

      let x,y be real-valued FinSequence;

      assume ( len x) = ( len y);

      

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

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

      hence thesis;

    end;

    theorem :: RVSUM_1:130

    

     Th130: |((p1 + p2), p3)| = ( |(p1, p3)| + |(p2, p3)|)

    proof

      reconsider f1 = p1, f2 = p2, f3 = p3 as real-valued FinSequence;

      ( len f2) = n by CARD_1:def 7;

      then ( len f1) = ( len f2) & ( len f2) = ( len f3) by CARD_1:def 7;

      hence thesis by Th120;

    end;

    theorem :: RVSUM_1:131

    

     Th131: for x be Real holds |((x * p1), p2)| = (x * |(p1, p2)|)

    proof

      let x be Real;

      reconsider f1 = p1, f2 = p2 as real-valued FinSequence;

      ( len f1) = n & ( len f2) = n by CARD_1:def 7;

      hence thesis by Th121;

    end;

    theorem :: RVSUM_1:132

    

     Th132: |(( - p1), p2)| = ( - |(p1, p2)|)

    proof

       |(( - p1), p2)| = |((( - 1) * p1), p2)|

      .= (( - 1) * |(p1, p2)|) by Th131;

      hence thesis;

    end;

    theorem :: RVSUM_1:133

     |(( - p1), ( - p2))| = |(p1, p2)|

    proof

       |(( - p1), ( - p2))| = ( - |(p1, ( - p2))|) by Th132

      .= ( - ( - |(p1, p2)|)) by Th132;

      hence thesis;

    end;

    theorem :: RVSUM_1:134

    

     Th134: |((p1 - p2), p3)| = ( |(p1, p3)| - |(p2, p3)|)

    proof

       |((p1 - p2), p3)| = ( |(p1, p3)| + |(( - p2), p3)|) by Th130

      .= ( |(p1, p3)| + ( - |(p2, p3)|)) by Th132;

      hence thesis;

    end;

    theorem :: RVSUM_1:135

     |(((x * p1) + (y * p2)), p3)| = ((x * |(p1, p3)|) + (y * |(p2, p3)|))

    proof

       |(((x * p1) + (y * p2)), p3)| = ( |((x * p1), p3)| + |((y * p2), p3)|) by Th130

      .= ((x * |(p1, p3)|) + |((y * p2), p3)|) by Th131

      .= ((x * |(p1, p3)|) + (y * |(p2, p3)|)) by Th131;

      hence thesis;

    end;

    theorem :: RVSUM_1:136

    

     Th136: |((p1 + p2), (q1 + q2))| = ((( |(p1, q1)| + |(p1, q2)|) + |(p2, q1)|) + |(p2, q2)|)

    proof

      

       A1: |((p1 + p2), q1)| = ( |(p1, q1)| + |(p2, q1)|) & |((p1 + p2), q2)| = ( |(p1, q2)| + |(p2, q2)|) by Th130;

       |((p1 + p2), (q1 + q2))| = ( |((p1 + p2), q1)| + |((p1 + p2), q2)|) by Th130

      .= ((( |(p1, q1)| + |(p1, q2)|) + |(p2, q1)|) + |(p2, q2)|) by A1;

      hence thesis;

    end;

    theorem :: RVSUM_1:137

    

     Th137: |((p1 - p2), (q1 - q2))| = ((( |(p1, q1)| - |(p1, q2)|) - |(p2, q1)|) + |(p2, q2)|)

    proof

      

       A1: |(p1, (q1 - q2))| = ( |(p1, q1)| - |(p1, q2)|) & |(p2, (q1 - q2))| = ( |(p2, q1)| - |(p2, q2)|) by Th134;

       |((p1 - p2), (q1 - q2))| = ( |(p1, (q1 - q2))| - |(p2, (q1 - q2))|) by Th134

      .= ((( |(p1, q1)| - |(p1, q2)|) - |(p2, q1)|) + |(p2, q2)|) by A1;

      hence thesis;

    end;

    theorem :: RVSUM_1:138

     |((p + q), (p + q))| = (( |(p, p)| + (2 * |(p, q)|)) + |(q, q)|)

    proof

      (( |(p, p)| + |(p, q)|) + |(p, q)|) = ( |(p, p)| + (2 * |(p, q)|));

      hence thesis by Th136;

    end;

    theorem :: RVSUM_1:139

    

     Th139: |((p - q), (p - q))| = (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|)

    proof

       |((p - q), (p - q))| = ((( |(p, p)| - |(p, q)|) - |(p, q)|) + |(q, q)|) by Th137

      .= (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|);

      hence thesis;

    end;

    theorem :: RVSUM_1:140

     |(p, q)| <= ( |(p, p)| + |(q, q)|)

    proof

       0 <= |(p, p)| & 0 <= |(q, q)| by Th119;

      then

       A1: ( 0 / 2) <= (( |(p, p)| + |(q, q)|) / 2);

       |((p - q), (p - q))| = (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|) by Th139

      .= (( |(p, p)| + |(q, q)|) - (2 * |(p, q)|));

      then (2 * |(p, q)|) <= (( |(p, p)| + |(q, q)|) - 0 ) by Th119, XREAL_1: 11;

      then ((2 * |(p, q)|) / 2) <= (( |(p, p)| + |(q, q)|) / 2) by XREAL_1: 72;

      then ( 0 qua Element of NAT + |(p, q)|) <= ((( |(p, p)| + |(q, q)|) / 2) + (( |(p, p)| + |(q, q)|) / 2)) by A1, XREAL_1: 7;

      hence thesis;

    end;

    definition

      let p,q be real-valued FinSequence;

      :: RVSUM_1:def17

      pred p,q are_orthogonal means |(p, q)| = 0 ;

      symmetry ;

    end

    theorem :: RVSUM_1:141

    (p,q) are_orthogonal implies ((a * p),q) are_orthogonal

    proof

      assume (p,q) are_orthogonal ;

      then |(p, q)| = 0 ;

      then (a * |(p, q)|) = 0 ;

      then |((a * p), q)| = 0 by Th131;

      hence thesis;

    end;

    theorem :: RVSUM_1:142

    ( Sum <*r1, r2, r3, r4*>) = (((r1 + r2) + r3) + r4)

    proof

      

      thus ( Sum <*r1, r2, r3, r4*>) = (( Sum <*r1, r2, r3*>) + r4) by Th74

      .= (((r1 + r2) + r3) + r4) by Th78;

    end;

    reserve f,g for real-valued FinSequence;

    theorem :: RVSUM_1:143

    

     Th143: ( len f) = ( len ( sqr f)) & ( dom f) = ( dom ( sqr f))

    proof

      ( rng f) c= REAL & ( dom sqrreal ) = REAL by FUNCT_2:def 1;

      

      hence ( len f) = ( len ( sqrreal * f)) by FINSEQ_2: 29

      .= ( len ( sqr f));

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: RVSUM_1:144

    ( sqr (f ^ g)) = (( sqr f) ^ ( sqr g))

    proof

      

       A1: ( len f) = ( len ( sqr f)) by Th143;

      

       A2: ( len ( sqr (f ^ g))) = ( len (f ^ g)) by Th143;

      

       A3: ( len g) = ( len ( sqr g)) & ( len (f ^ g)) = (( len f) + ( len g)) by Th143, FINSEQ_1: 22;

      

       A4: for i be Nat st 1 <= i & i <= ( len ( sqr (f ^ g))) holds (( sqr (f ^ g)) . i) = ((( sqr f) ^ ( sqr g)) . i)

      proof

        let i be Nat;

        assume that

         A5: 1 <= i and

         A6: i <= ( len ( sqr (f ^ g)));

        

         A7: i in ( dom (f ^ g)) by A2, A5, A6, FINSEQ_3: 25;

        per cases ;

          suppose

           A8: i in ( dom f);

          then

           A9: i in ( dom ( sqr f)) by Th143;

          

          thus (( sqr (f ^ g)) . i) = (( sqrreal * (f ^ g)) . i)

          .= ( sqrreal . ((f ^ g) . i)) by A7, FUNCT_1: 13

          .= ( sqrreal . (f . i)) by A8, FINSEQ_1:def 7

          .= ((f . i) ^2 ) by Def2

          .= (( sqr f) . i) by VALUED_1: 11

          .= ((( sqr f) ^ ( sqr g)) . i) by A9, FINSEQ_1:def 7;

        end;

          suppose not i in ( dom f);

          then

           A10: ( len f) < i by A5, FINSEQ_3: 25;

          then

          reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

          

           A11: i <= ( len (f ^ g)) by A6, Th143;

          

           A12: i <= ( len (( sqr f) ^ ( sqr g))) by A1, A3, A2, A6, FINSEQ_1: 22;

          

          thus (( sqr (f ^ g)) . i) = (( sqrreal * (f ^ g)) . i)

          .= ( sqrreal . ((f ^ g) . i)) by A7, FUNCT_1: 13

          .= ( sqrreal . (g . j)) by A10, A11, FINSEQ_1: 24

          .= ((g . j) ^2 ) by Def2

          .= (( sqr g) . j) by VALUED_1: 11

          .= ((( sqr f) ^ ( sqr g)) . i) by A1, A10, A12, FINSEQ_1: 24;

        end;

      end;

      ( len ( sqr (f ^ g))) = ( len (( sqr f) ^ ( sqr g))) by A1, A3, A2, FINSEQ_1: 22;

      hence thesis by A4;

    end;

    theorem :: RVSUM_1:145

    for F be real-valued FinSequence holds F is FinSequence of REAL

    proof

      let F be real-valued FinSequence;

      thus ( rng F) c= REAL ;

    end;

    theorem :: RVSUM_1:146

    for F be complex-valued FinSequence holds F is FinSequence of COMPLEX by Lm5;

    registration

      let r be natural Number;

      cluster <*r*> -> natural-valued;

      coherence

      proof

        reconsider p = r as Element of NAT by ORDINAL1:def 12;

         <*p*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2 be natural Number;

      cluster <*r1, r2*> -> natural-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2 as Element of NAT by ORDINAL1:def 12;

         <*p1, p2*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let r1,r2,r3 be natural Number;

      cluster <*r1, r2, r3*> -> natural-valued;

      coherence

      proof

        reconsider p1 = r1, p2 = r2, p3 = r3 as Element of NAT by ORDINAL1:def 12;

         <*p1, p2, p3*> is FinSequence-like;

        hence thesis;

      end;

    end

    registration

      let f,g be natural-valued FinSequence;

      cluster (f ^ g) -> natural-valued;

      coherence

      proof

        

         A1: ( rng f) c= NAT & ( rng g) c= NAT by VALUED_0:def 6;

        ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

        then ( rng (f ^ g)) c= NAT by A1, XBOOLE_1: 8;

        hence thesis by VALUED_0:def 6;

      end;

    end