newton04.miz



    begin

    reserve a,b,i,j,k,l,m,n for Nat;

    registration

      let a be positive Real, n be Nat;

      cluster (a |^ n) -> positive;

      coherence by PREPOWER: 6;

    end

    registration

      let a be non negative Real, n be Nat;

      cluster (a |^ n) -> non negative;

      coherence

      proof

        a = 0 or a > 0 ;

        hence thesis;

      end;

    end

    registration

      let a be non negative Real;

      reduce ( sqrt (a |^ 2)) to a;

      reducibility

      proof

        (a |^ 2) = (a ^2 ) by NEWTON: 81;

        hence thesis by SQUARE_1: 22;

      end;

    end

    registration

      cluster real for Complex;

      correctness by COMPLEX1:def 1;

      cluster non real for Complex;

      correctness

      proof

         not <i> is real by COMPLEX1: 18;

        hence thesis;

      end;

    end

    registration

      let a be non real Complex;

      cluster ( Im a) -> non zero;

      coherence

      proof

        a <> (( Re a) + ( 0 * <i> ));

        hence thesis by COMPLEX1: 13;

      end;

    end

    registration

      let a be Real;

      reduce ( Re a) to a;

      reducibility by COMPLEX1:def 1;

    end

    theorem :: NEWTON04:1

    for a be non zero Real, a1 be Complex st (a * a1) is Real holds a1 is Real

    proof

      let a be non zero Real, a1 be Complex;

      ( Im (a1 * a)) = ((( Re a1) * ( Im a)) + (( Re a) * ( Im a1))) by COMPLEX1: 9

      .= ((( Re a1) * 0 ) + (a * ( Im a1)));

      hence thesis;

    end;

    registration

      cluster REAL -valued -> COMPLEX -valued for Relation;

      coherence by NUMBERS: 11;

      cluster RAT -valued -> REAL -valued for Relation;

      coherence by NUMBERS: 12;

      cluster RAT -valued -> COMPLEX -valued for Relation;

      coherence by NUMBERS: 13;

      cluster INT -valued -> RAT -valued for Relation;

      coherence ;

      cluster INT -valued -> REAL -valued for Relation;

      coherence by NUMBERS: 15;

      cluster INT -valued -> COMPLEX -valued for Relation;

      coherence by NUMBERS: 16;

      cluster NAT -valued -> INT -valued for Relation;

      coherence ;

      cluster NAT -valued -> RAT -valued for Relation;

      coherence ;

      cluster NAT -valued -> REAL -valued for Relation;

      coherence by NUMBERS: 19;

      cluster NAT -valued -> COMPLEX -valued for Relation;

      coherence by NUMBERS: 20;

      cluster real-valued -> REAL -valued for Relation;

      coherence

      proof

        let f be Relation;

        assume f is real-valued;

        hence ( rng f) c= REAL by VALUED_0:def 3;

      end;

      cluster complex-valued -> COMPLEX -valued for Relation;

      coherence

      proof

        let f be Relation;

        assume f is complex-valued;

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

      end;

    end

    registration

      let a be object;

      reduce (1 * ( len <*a*>)) to 1;

      reducibility by FINSEQ_1: 40;

    end

    registration

      let a be object, f be FinSequence;

      reduce (( <*a*> ^ f) . 1) to a;

      reducibility by FINSEQ_1: 41;

      reduce ((f ^ <*a*>) . (1 + ( len f))) to a;

      reducibility by FINSEQ_1: 42;

    end

    registration

      let x be Complex;

      reduce ( Sum <*x*>) to x;

      reducibility by RVSUM_2: 30;

    end

    registration

      let f,g be FinSequence;

      reduce ((f ^ g) | ( dom f)) to f;

      reducibility by FINSEQ_1: 21;

      reduce ((f ^ g) | ( len f)) to f;

      reducibility

      proof

        ((f ^ g) | ( dom f)) = ((f ^ g) | ( Seg ( len f))) by FINSEQ_1:def 3;

        hence thesis;

      end;

    end

    theorem :: NEWTON04:2

    

     Th0: for f be FinSequence holds ex D be non empty set st f is FinSequence of D

    proof

      let f be FinSequence;

      f is FinSequence of (( rng f) \/ {1}) by XBOOLE_1: 7, FINSEQ_1:def 4;

      hence thesis;

    end;

    registration

      let f be FinSequence;

      reduce (f . 0 ) to 0 ;

      reducibility

      proof

         not 0 in ( dom f) by FINSEQ_3: 24;

        hence thesis by FUNCT_1:def 2;

      end;

      reduce (f | ( len f)) to f;

      reducibility

      proof

        f = (f ^ {} );

        hence thesis;

      end;

      cluster (f /^ ( len f)) -> empty;

      coherence by RFINSEQ: 27;

    end

    registration

      let n be Nat;

      reduce ( card ( Seg n)) to n;

      reducibility by FINSEQ_1: 57;

      reduce ( card ( Segm n)) to n;

      reducibility by ORDINAL1:def 17;

    end

    registration

      let n be Nat;

      reduce ( len ( id ( Seg n))) to n;

      reducibility

      proof

        n in NAT & ( dom ( id ( Seg n))) = ( Seg n) by ORDINAL1:def 12;

        hence ( len ( id ( Seg n))) = n by FINSEQ_1:def 3;

      end;

      reduce ( len ( idseq n)) to n;

      reducibility

      proof

        ( len ( idseq n)) = ( len ( id ( Seg n))) by FINSEQ_2:def 1;

        hence thesis;

      end;

    end

    registration

      let m,n be Nat;

      reduce (( idseq (m + n)) . m) to m;

      reducibility

      proof

        per cases ;

          suppose m = 0 ;

          hence thesis;

        end;

          suppose m > 0 ;

          then (m + n) >= (m + 0 ) & m >= 1 by NAT_1: 14, XREAL_1: 6;

          then m in ( Seg (m + n));

          hence thesis by FINSEQ_2: 49;

        end;

      end;

      reduce (( Rev ( idseq (m + (n + 1)))) . (m + 1)) to (n + 1);

      reducibility

      proof

        set l = (m + 1), k = ((m + n) + 1);

        

         A0: ((m + n) + 1) = ( len ( idseq ((m + n) + 1))) & ( len ( idseq ((m + n) + 1))) = ( len ( Rev ( idseq ((m + n) + 1)))) by FINSEQ_5:def 3;

        1 <= (m + 1) & (m + 1) <= ((m + 1) + n) by NAT_1: 11;

        then l in ( dom ( Rev ( idseq k))) by A0, FINSEQ_3: 25;

        

        then (( Rev ( idseq k)) . l) = (( idseq k) . ((k - l) + 1)) by A0, FINSEQ_5:def 3

        .= (( idseq (m + (n + 1))) . (n + 1));

        hence thesis;

      end;

    end

    definition

      let a,b be Nat;

      :: original: min

      redefine

      func min (a,b) -> Nat ;

      coherence by XXREAL_0:def 9;

      :: original: max

      redefine

      func max (a,b) -> Nat ;

      coherence by XXREAL_0:def 10;

    end

    registration

      let f be FinSequence, n be Nat;

      reduce (f | (( len f) + n)) to f;

      reducibility by FINSEQ_1: 58, NAT_1: 12;

      reduce (f | ( Seg ( max (( len f),n)))) to f;

      reducibility

      proof

        set l = (( max (( len f),n)) - ( len f));

        (f | ( Seg (( len f) + l))) = (f | (( len f) + l));

        hence thesis;

      end;

      cluster (f /^ (( len f) + n)) -> empty;

      coherence

      proof

        ( 0 + ( len f)) <= (n + ( len f)) by XREAL_1: 6;

        hence thesis by FINSEQ_5: 32;

      end;

      cluster ((f /^ ( len f)) . n) -> zero;

      coherence ;

    end

    theorem :: NEWTON04:3

    for n be Element of NAT , D be set, f be FinSequence of D st n in ( dom f) holds ( len (f | n)) = n

    proof

      let n be Element of NAT , D be set, f be FinSequence of D;

      assume n in ( dom f);

      then n <= ( len f) by FINSEQ_3: 25;

      hence thesis by FINSEQ_1: 59;

    end;

    theorem :: NEWTON04:4

    for n be Element of NAT , D be set, f be FinSequence of D st n >= ( len f) holds ( len (f | n)) = ( len f)

    proof

      let n be Element of NAT , D be set, f be FinSequence of D;

      assume n >= ( len f);

      then

      reconsider k = (n - ( len f)) as Element of NAT by NAT_1: 21;

      ( len (f | n)) = ( len (f | (( len f) + k)));

      hence thesis;

    end;

    registration

      let f be FinSequence, n be non zero Nat;

      cluster (f . (( len f) + n)) -> zero;

      coherence

      proof

        (( len f) + n) > (( len f) + 0 ) by XREAL_1: 6;

        then not (( len f) + n) in ( dom f) by FINSEQ_3: 25;

        hence thesis by FUNCT_1:def 2;

      end;

    end

    registration

      let f be FinSequence of REAL , i,j be Nat;

      reduce ((f | i) | (i + j)) to (f | i);

      reducibility

      proof

        ( len (f | i)) = ( min (( len f),i)) by FINSEQ_2: 21;

        then (i + j) >= ( len (f | i)) by XXREAL_0: 17, NAT_1: 12;

        then

        reconsider k = ((i + j) - ( len (f | i))) as Element of NAT by NAT_1: 21;

        ((f | i) | (i + j)) = ((f | i) | (( len (f | i)) + k));

        hence thesis;

      end;

    end

    registration

      let a be Nat;

      reduce ( Sum (a |-> 0 )) to 0 ;

      reducibility by RVSUM_1: 81;

      cluster ( Sum (a |-> 0 )) -> zero;

      coherence ;

    end

    registration

      let a be Nat, b be object;

      reduce ( len (a |-> b)) to a;

      reducibility by CARD_1:def 7;

    end

    registration

      let a be non zero Nat, b be object;

      cluster (a |-> b) -> non empty;

      coherence ;

      cluster (a |-> b) -> constant;

      coherence

      proof

        (( Seg a) --> b) is constant;

        hence thesis by FINSEQ_2:def 2;

      end;

      reduce ( the_value_of (a |-> b)) to b;

      reducibility

      proof

        reconsider b as set by TARSKI: 1;

        ( the_value_of (( Seg a) --> b)) = b by FUNCOP_1: 79;

        hence thesis by FINSEQ_2:def 2;

      end;

    end

    registration

      let f be constant FinSequence;

      reduce ( Rev f) to f;

      reducibility

      proof

        

         A1: ( dom ( Rev f)) = ( dom f) by FINSEQ_5: 57;

        for i be object st i in ( dom f) holds (( Rev f) . i) = (f . i)

        proof

          let i be object such that

           B1: i in ( dom f);

          

           B2: i in ( dom ( Rev f)) by B1, FINSEQ_5: 57;

          reconsider i as Nat by B1;

          set n = ( len f);

          

           B3: n >= i >= 1 by B1, FINSEQ_3: 25;

          then

          reconsider k = (n - i) as Element of NAT by NAT_1: 21;

          (k + i) >= (k + 1) & (1 + k) >= (1 + 0 ) by B3, XREAL_1: 6;

          then (k + 1) in ( dom f) by FINSEQ_3: 25;

          then (f . (k + 1)) = (f . i) by B1, FUNCT_1:def 10;

          hence thesis by B2, FINSEQ_5:def 3;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

    end

    registration

      let a be Nat, b be non zero Nat, x be object;

      reduce (((a + b) |-> x) . b) to x;

      reducibility

      proof

        (a + b) >= ( 0 + b) by XREAL_1: 6;

        then b >= 1 & b <= (a + b) by NAT_1: 14;

        then b in ( Seg (a + b));

        hence thesis by FINSEQ_2: 57;

      end;

      cluster ((a |-> x) . (a + b)) -> zero;

      coherence

      proof

        (a + b) > (a + 0 ) by XREAL_1: 6;

        then (a + b) > ( len (a |-> x));

        hence thesis;

      end;

    end

    registration

      let a be object, n be Nat;

      reduce ( Rev (n |-> a)) to (n |-> a);

      reducibility

      proof

        n = 0 or n > 0 ;

        then (n |-> a) is empty or (n |-> a) is constant;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      reduce (n choose ( 0 * 1)) to 1;

      reducibility by NEWTON: 19;

      reduce (n choose (n * 1)) to 1;

      reducibility by NEWTON: 21;

    end

    registration

      let f be nonnegative-yielding FinSequence of REAL , i be Nat;

      cluster (f . i) -> non negative;

      coherence

      proof

        per cases ;

          suppose i in ( dom f);

          then (f . i) in ( rng f) by FUNCT_1:def 3;

          hence thesis by PARTFUN3:def 4;

        end;

          suppose not i in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      cluster empty -> nonpositive-yielding for FinSequence;

      coherence

      proof

        let f be FinSequence;

        assume f is empty;

        then for r be Real st r in ( rng f) holds r <= 0 ;

        hence thesis by PARTFUN3:def 3;

      end;

    end

    registration

      let f be nonpositive-yielding FinSequence of REAL , i be Nat;

      cluster (f . i) -> non positive;

      coherence

      proof

        per cases ;

          suppose i in ( dom f);

          then (f . i) in ( rng f) by FUNCT_1: 3;

          hence thesis by PARTFUN3:def 3;

        end;

          suppose not i in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be nonnegative-yielding FinSequence of REAL , i,j be Nat;

      cluster ((f | j) . i) -> non negative;

      coherence

      proof

        ( len (f | j)) = ( min (j,( len f))) by FINSEQ_2: 21;

        then

         A0: j >= ( len (f | j)) by XXREAL_0: 17;

        per cases ;

          suppose

           Q0: j in ( dom f);

          per cases ;

            suppose i in ( dom (f | j));

            then ( len (f | j)) >= i >= 1 by FINSEQ_3: 25;

            then

             A2: 1 <= i & i <= j by A0, XXREAL_0: 2;

            reconsider f as FinSequence of COMPLEX by RVSUM_1: 146;

            ((f | j) . i) = (f . i) by Q0, A2, NEWTON02: 107;

            hence thesis;

          end;

            suppose not i in ( dom (f | j));

            hence thesis by FUNCT_1:def 2;

          end;

        end;

          suppose not j in ( dom f);

          then j > ( len f) or j < 1 by FINSEQ_3: 25;

          then (f | j) = f or j = 0 by FINSEQ_1: 58, NAT_1: 14;

          hence thesis;

        end;

      end;

      cluster ((f /^ j) . i) -> non negative;

      coherence

      proof

        ( rng (f /^ j)) c= ( rng f) by FINSEQ_5: 33;

        then for x be Real holds x in ( rng (f /^ j)) implies x >= 0 by PARTFUN3:def 4;

        then (f /^ j) is nonnegative-yielding by PARTFUN3:def 4;

        hence thesis;

      end;

    end

    registration

      let f be empty real-valued FinSequence;

      cluster ( Product f) -> non negative;

      coherence by RVSUM_1: 94;

    end

    registration

      let f be nonnegative-yielding FinSequence of REAL ;

      cluster ( Sum f) -> non negative;

      coherence

      proof

        for i be Nat st i in ( dom f) holds (f . i) >= 0 ;

        hence thesis by RVSUM_1: 84;

      end;

      cluster ( Product f) -> non negative;

      coherence

      proof

        reconsider g = f as real-valued FinSequence;

        per cases ;

          suppose g is positive-yielding;

          then for x be Real st x in ( rng g) holds x > 0 by PARTFUN3:def 1;

          then for k be Element of NAT st k in ( dom g) holds (g . k) > 0 by FUNCT_1: 3;

          hence thesis by NAT_4: 42;

        end;

          suppose

           B1: not g is positive-yielding;

          ex i be object st i in ( dom g) & (g . i) = 0

          proof

            consider r be Real such that

             C1: r in ( rng g) & r <= 0 by B1, PARTFUN3:def 1;

            r = 0 by PARTFUN3:def 4, C1;

            hence thesis by C1, FUNCT_1:def 3;

          end;

          hence thesis by RVSUM_1: 103;

        end;

      end;

    end

    registration

      let f be nonpositive-yielding FinSequence of REAL ;

      cluster ( Sum f) -> non positive;

      coherence

      proof

        for i be Nat st i in ( dom ( - f)) holds (( - f) . i) >= 0

        proof

          let i be Nat such that

           A1: i in ( dom ( - f));

          i in ( dom f) & (( - f) . i) = ( - (f . i)) by A1, VALUED_1: 8;

          hence thesis;

        end;

        then ( Sum ( - f)) >= ( Sum (( len f) |-> 0 )) by RVSUM_1: 84;

        then (( - ( Sum f)) + ( Sum f)) >= ( 0 + ( Sum f)) by RVSUM_1: 88;

        hence thesis;

      end;

    end

    registration

      let a be object, f be nonnegative-yielding FinSequence of REAL ;

      cluster (f . a) -> non negative;

      coherence

      proof

        a in ( dom f) or not a in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

    end

    registration

      let a be object, f be nonpositive-yielding FinSequence of REAL ;

      cluster (f . a) -> non positive;

      coherence

      proof

        a in ( dom f) or not a in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

    end

    registration

      let D be set;

      let f,g be D -valued FinSequence;

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

      correctness

      proof

        reconsider f, g as FinSequence of D by NEWTON02: 103;

        (f ^ g) is D -valued FinSequence;

        hence thesis;

      end;

    end

    registration

      let f be FinSequence of REAL , n be Nat;

      cluster ((f | n) /^ n) -> empty;

      coherence ;

      cluster (f /^ ( max (( len f),n))) -> empty;

      coherence

      proof

        ((f | ( max (( len f),n))) /^ ( max (( len f),n))) is empty;

        hence thesis;

      end;

    end

    registration

      let D be set;

      cluster empty for FinSequence of D;

      existence

      proof

        ( <*> D) = {} ;

        hence thesis;

      end;

      cluster empty -> nonnegative-yielding for FinSequence of D;

      coherence ;

    end

    registration

      cluster nonnegative-yielding INT -valued -> NAT -valued for FinSequence;

      coherence

      proof

        let f be FinSequence;

        assume

         A1: f is nonnegative-yielding INT -valued;

        then

        reconsider f as FinSequence of INT by NEWTON02: 103;

        reconsider f as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 15;

        for i be Nat st i in ( dom f) holds (f . i) in NAT by A1, INT_1: 3;

        hence thesis by FINSEQ_2: 12;

      end;

      cluster nonnegative-yielding -> NAT -valued for FinSequence of INT ;

      coherence ;

    end

    registration

      let f be COMPLEX -valued FinSequence;

      reduce (f + 0 ) to f;

      reducibility

      proof

        

         A1: ( dom (f + 0 )) = ( dom f) & for c be object st c in ( dom (f + 0 )) holds ((f + 0 ) . c) = ((f . c) + 0 ) by VALUED_1:def 2;

        for c be object st c in ( dom (f + 0 )) holds ((f + 0 ) . c) = (f . c)

        proof

          let c be object such that

           B1: c in ( dom (f + 0 ));

          ((f + 0 ) . c) = ((f . c) + 0 ) by VALUED_1:def 2, B1

          .= (f . c);

          hence thesis;

        end;

        hence thesis by A1, FUNCT_1: 2;

      end;

      reduce (f - 0 ) to f;

      reducibility

      proof

        (f - 0 ) = (( - 0 ) + f) by VALUED_1:def 3;

        hence thesis;

      end;

    end

    registration

      let x be object;

      reduce ( <*x*> . 1) to x;

      reducibility by FINSEQ_1:def 8;

    end

    theorem :: NEWTON04:5

    for f be FinSequence, P be Permutation of ( dom f) holds P is Permutation of ( dom ( Rev f))

    proof

      let f be FinSequence, P be Permutation of ( dom f);

      ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      then ( dom f) = ( dom ( Rev f)) by FINSEQ_3: 29;

      hence thesis;

    end;

    theorem :: NEWTON04:6

    

     MATRIX94: ( Rev ( idseq n)) is Permutation of ( Seg n)

    proof

      reconsider f = ( idseq n) as one-to-one FinSequence-like Function of ( Seg n), ( Seg n) by FINSEQ_2: 55;

      

       A1: ( dom ( Rev ( idseq n))) = ( dom ( idseq n)) by FINSEQ_5: 57

      .= ( dom ( id ( Seg n))) by FINSEQ_2:def 1

      .= ( Seg n);

      

       A2: ( rng ( idseq n)) = ( rng ( id ( Seg n))) by FINSEQ_2:def 1

      .= ( Seg n);

      then ( rng ( Rev f)) c= ( Seg n) by FINSEQ_5: 57;

      then

      reconsider g = ( Rev f) as FinSequence-like Function of ( Seg n), ( Seg n) by A1, FUNCT_2: 2;

      ( rng f) = ( rng ( Rev f)) by FINSEQ_5: 57;

      then g is onto by A2, FUNCT_2:def 3;

      hence thesis;

    end;

    theorem :: NEWTON04:7

    for f be FinSequence holds ( idseq ( len f)) is Permutation of ( dom f)

    proof

      let f be FinSequence;

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

      hence thesis by FINSEQ_2: 55;

    end;

    theorem :: NEWTON04:8

    

     RFP: for f be FinSequence holds ( Rev ( idseq ( len f))) is Permutation of ( dom ( Rev f))

    proof

      let f be FinSequence;

      ( dom ( Rev f)) = ( dom f) by FINSEQ_5: 57

      .= ( Seg ( len f)) by FINSEQ_1:def 3;

      hence thesis by MATRIX94;

    end;

    theorem :: NEWTON04:9

    

     DR: for f be Function, h be Permutation of ( dom f) holds ( dom (f * h)) = ( dom f)

    proof

      let f be Function, h be Permutation of ( dom f);

      ( dom (f * h)) = (h " ( dom f)) by RELAT_1: 147

      .= (h " ( rng h)) by FUNCT_2:def 3

      .= ( dom h) by RELAT_1: 134

      .= ( dom f) by FUNCT_2: 52;

      hence thesis;

    end;

    registration

      let f be FinSequence, h be Permutation of ( dom f);

      cluster (f * h) -> FinSequence-like;

      coherence

      proof

        ( dom (f * h)) = ( dom f) by DR

        .= ( Seg ( len f)) by FINSEQ_1:def 3;

        hence thesis;

      end;

      cluster (f * h) -> ( dom f) -defined;

      coherence ;

    end

    theorem :: NEWTON04:10

    

     REV: for f be FinSequence holds f = (( Rev f) * ( Rev ( idseq ( len f))))

    proof

      let f be FinSequence;

      reconsider P = ( Rev ( idseq ( len f))) as Permutation of ( dom ( Rev f)) by RFP;

      reconsider g = (( Rev f) * P) as FinSequence;

      

       A1: ( dom f) = ( dom ( Rev f)) by FINSEQ_5: 57

      .= ( dom (( Rev f) * P)) by DR;

      for x be object st x in ( dom f) holds (f . x) = (g . x)

      proof

        set n = ( len f);

        let x be object such that

         B1: x in ( dom f);

        reconsider x as Nat by B1;

        

         B2: 1 <= x <= n by B1, FINSEQ_3: 25;

        then

        reconsider m = (x - 1) as Nat;

        reconsider k = (n - x) as Element of NAT by B2, NAT_1: 21;

        set l = (k + 1);

        (1 + 0 ) <= l <= (k + x) by B2, XREAL_1: 6;

        then l in ( dom f) by FINSEQ_3: 25;

        then

         B3: l in ( dom ( Rev f)) by FINSEQ_5: 57;

        (g . x) = (( Rev f) . (( Rev ( idseq (m + l))) . (m + 1))) by A1, B1, FUNCT_1: 12

        .= (f . ((n - l) + 1)) by B3, FINSEQ_5:def 3

        .= (f . x);

        hence thesis;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: NEWTON04:11

    

     FFE: for f be FinSequence holds (f,( Rev f)) are_fiberwise_equipotent

    proof

      let f be FinSequence;

      

       A1: f = (( Rev f) * ( Rev ( idseq ( len f)))) by REV;

      ( Rev ( idseq ( len f))) is Permutation of ( dom ( Rev f)) by RFP;

      hence thesis by A1, RFINSEQ: 4;

    end;

    theorem :: NEWTON04:12

    for D be non empty set, r be D -valued FinSequence st ( len r) = (i + j) holds ex p,q be D -valued FinSequence st ( len p) = i & ( len q) = j & r = (p ^ q)

    proof

      let D be non empty set, r be D -valued FinSequence such that

       A1: ( len r) = (i + j);

      reconsider r1 = r as FinSequence of D by NEWTON02: 103;

      ex p1,q1 be FinSequence of D st ( len p1) = i & ( len q1) = j & r1 = (p1 ^ q1) by A1, FINSEQ_2: 23;

      hence thesis;

    end;

    theorem :: NEWTON04:13

    for f be nonnegative-yielding FinSequence of REAL holds ( Sum f) >= ( Sum (f | j))

    proof

      let f be nonnegative-yielding FinSequence of REAL ;

      

       A1: ((f | j) ^ (f /^ j)) = f by RFINSEQ: 8;

      for i be Nat st i in ( dom (f /^ j)) holds ((f /^ j) . i) >= 0 ;

      then (( Sum (f | j)) + ( Sum (f /^ j))) >= (( Sum (f | j)) + 0 ) by RVSUM_1: 84, XREAL_1: 6;

      hence thesis by A1, RVSUM_1: 75;

    end;

    theorem :: NEWTON04:14

    

     FXX: for f be COMPLEX -valued FinSequence, x1,x2 be Complex holds ((f + x1) + x2) = (f + (x1 + x2))

    proof

      let f be COMPLEX -valued FinSequence, x1,x2 be Complex;

      reconsider X = ( dom f) as set;

      

       A1: ( dom ((f + x1) + x2)) = ( dom (f + x1)) & for c be object st c in ( dom ((f + x1) + x2)) holds (((f + x1) + x2) . c) = (((f + x1) . c) + x2) by VALUED_1:def 2;

      

       A2: ( dom (f + x1)) = ( dom f) & for c be object st c in ( dom (f + x1)) holds ((f + x1) . c) = ((f . c) + x1) by VALUED_1:def 2;

      

       A3: ( dom (f + (x1 + x2))) = ( dom f) & for c be object st c in ( dom (f + (x1 + x2))) holds ((f + (x1 + x2)) . c) = ((f . c) + (x1 + x2)) by VALUED_1:def 2;

      for c be object st c in X holds (((f + x1) + x2) . c) = ((f + (x1 + x2)) . c)

      proof

        let c be object such that

         B1: c in X;

        (((f + x1) + x2) . c) = (((f + x1) . c) + x2) by A1, A2, B1

        .= (((f . c) + x1) + x2) by A2, B1

        .= ((f . c) + (x1 + x2))

        .= ((f + (x1 + x2)) . c) by A3, B1;

        hence thesis;

      end;

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

    end;

    registration

      let f be COMPLEX -valued FinSequence, x be Complex;

      reduce ((f + x) - x) to f;

      reducibility

      proof

        ((f + x) - x) = ((f + x) + ( - x)) by VALUED_1:def 3

        .= (f + (x + ( - x))) by FXX

        .= (f + 0 );

        hence thesis;

      end;

      reduce ((f - x) + x) to f;

      reducibility

      proof

        ((f - x) + x) = ((f + ( - x)) + x) by VALUED_1:def 3

        .= (f + (( - x) + x)) by FXX

        .= (f + 0 );

        hence thesis;

      end;

    end

    registration

      let x,y be Real;

      reduce ( max (( min (x,y)),( max (x,y)))) to ( max (x,y));

      reducibility

      proof

        ( max (x,y)) >= x >= ( min (x,y)) by XXREAL_0: 17, XXREAL_0: 25;

        hence thesis by XXREAL_0:def 10, XXREAL_0: 2;

      end;

      reduce ( min (( min (x,y)),( max (x,y)))) to ( min (x,y));

      reducibility

      proof

        ( max (x,y)) >= x >= ( min (x,y)) by XXREAL_0: 17, XXREAL_0: 25;

        hence thesis by XXREAL_0:def 9, XXREAL_0: 2;

      end;

    end

    registration

      let x,y be Real, z be non negative Real;

      reduce ( min (( min (x,y)),(y + z))) to ( min (x,y));

      reducibility

      proof

        (y + z) >= (y + 0 ) by XREAL_1: 6;

        then ( min (y,(y + z))) = y by XXREAL_0:def 9;

        hence thesis by XXREAL_0: 33;

      end;

      reduce ( max (( max (x,y)),(y - z))) to ( max (x,y));

      reducibility

      proof

        (y - z) <= (y - 0 ) by XREAL_1: 10;

        then ( max ((y - z),y)) = y by XXREAL_0:def 10;

        hence thesis by XXREAL_0: 34;

      end;

    end

    registration

      let f be FinSequence, i,j be Nat;

      reduce ((f | i) | (i + j)) to (f | i);

      reducibility

      proof

        ( len (f | i)) = ( min (( len f),i)) by FINSEQ_2: 21;

        then (i + j) >= ( len (f | i)) by XXREAL_0: 17, NAT_1: 12;

        then

        reconsider k = ((i + j) - ( len (f | i))) as Element of NAT by NAT_1: 21;

        ((f | i) | (i + j)) = ((f | i) | (( len (f | i)) + k));

        hence thesis;

      end;

    end

    registration

      let f be nonnegative-yielding FinSequence of REAL , n be Nat;

      cluster (f | n) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        assume r in ( rng (f | n));

        then ex i be object st i in ( dom (f | n)) & ((f | n) . i) = r by FUNCT_1:def 3;

        hence thesis;

      end;

      cluster (f /^ n) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        assume r in ( rng (f /^ n));

        then ex i be object st i in ( dom (f /^ n)) & ((f /^ n) . i) = r by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    registration

      let f be FinSequence of REAL ;

      cluster (f - ( min f)) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng (f - ( min f))) holds r >= 0

        proof

          let r be Real such that

           A1: r in ( rng (f - ( min f)));

          consider x be object such that

           A2: x in ( dom (f - ( min f))) & r = ((f - ( min f)) . x) by A1, FUNCT_1:def 3;

          

           A3: ( dom (f - ( min f))) = ( dom f) & for i be object st i in ( dom f) holds ((f - ( min f)) . i) = ((f . i) - ( min f)) by VALUED_1: 3;

          reconsider x as Nat by A2;

          1 <= x <= ( len f) by A2, A3, FINSEQ_3: 25;

          then ((f . x) - ( min f)) >= (( min f) - ( min f)) by XREAL_1: 9, RFINSEQ2: 2;

          hence thesis by A2, A3;

        end;

        hence thesis by PARTFUN3:def 4;

      end;

      cluster (f - ( max f)) -> nonpositive-yielding;

      coherence

      proof

        for r be Real st r in ( rng (f - ( max f))) holds r <= 0

        proof

          let r be Real such that

           A1: r in ( rng (f - ( max f)));

          consider x be object such that

           A2: x in ( dom (f - ( max f))) & r = ((f - ( max f)) . x) by A1, FUNCT_1:def 3;

          

           A3: ( dom (f - ( max f))) = ( dom f) & for i be object st i in ( dom f) holds ((f - ( max f)) . i) = ((f . i) - ( max f)) by VALUED_1: 3;

          reconsider x as Nat by A2;

          1 <= x <= ( len f) by A2, A3, FINSEQ_3: 25;

          then ((f . x) - ( max f)) <= (( max f) - ( max f)) by XREAL_1: 9, RFINSEQ2: 1;

          hence thesis by A2, A3;

        end;

        hence thesis by PARTFUN3:def 3;

      end;

    end

    registration

      let f be FinSequence;

      cluster ( Rev f) -> ( len f) -element;

      coherence

      proof

        ( len ( Rev f)) = ( len f) by FINSEQ_5:def 3;

        then (( Rev f) null f) is ( len f) -element;

        hence thesis;

      end;

    end

    registration

      let D be non empty set;

      let f be D -valued FinSequence;

      cluster ( Rev f) -> D -valued;

      coherence

      proof

        ( rng ( Rev f)) = ( rng f) by FINSEQ_5: 57;

        then ( rng ( Rev f)) c= D by RELAT_1:def 19;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

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

      cluster (a (#) f) -> ( len f) -element;

      coherence

      proof

        ( dom (a (#) f)) = ( dom f) by VALUED_1:def 5;

        then ( len (a (#) f)) = ( len f) by FINSEQ_3: 29;

        then ((a (#) f) null f) is ( len f) -element;

        hence thesis;

      end;

    end

    registration

      let a,b be Real, n be Nat;

      reduce ( len ((a,b) In_Power ((n + 1) - 1))) to (n + 1);

      reducibility by NEWTON:def 4;

      cluster ((a,b) In_Power n) -> (n + 1) -element;

      coherence

      proof

        (((a,b) In_Power ((n + 1) - 1)) null n) is (n + 1) -element;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      reduce ( len ( Newton_Coeff ((n + 1) - 1))) to (n + 1);

      reducibility by NEWTON:def 5;

      cluster ( Newton_Coeff n) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng ( Newton_Coeff n)) holds r >= 0 ;

        hence thesis by PARTFUN3:def 4;

      end;

      cluster ( Newton_Coeff n) -> (n + 1) -element;

      coherence

      proof

        (( Newton_Coeff ((n + 1) - 1)) null n) is (n + 1) -element;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      reduce (( Newton_Coeff n) . 2) to n;

      reducibility

      proof

        (n + 1) >= (1 + 1) & (1 + 1) >= (1 + 0 ) by XREAL_1: 6, NAT_1: 14;

        then ( len ( Newton_Coeff n)) >= (1 + 1) >= 1 by NEWTON:def 5;

        then 2 in ( dom ( Newton_Coeff n)) by FINSEQ_3: 25;

        then (( Newton_Coeff n) . 2) = (n choose (2 - 1)) by NEWTON:def 5;

        hence thesis by NEWTON: 23, NAT_1: 14;

      end;

      reduce (( Newton_Coeff n) . n) to n;

      reducibility

      proof

        (n + 1) >= (n + 0 ) & n >= 1 by NAT_1: 14, XREAL_1: 6;

        then ( len ( Newton_Coeff n)) >= n >= 1 by NEWTON:def 5;

        then n in ( dom ( Newton_Coeff n)) by FINSEQ_3: 25;

        then (( Newton_Coeff n) . n) = (n choose (n - 1)) by NEWTON:def 5;

        hence thesis by NEWTON: 24, NAT_1: 14;

      end;

    end

    theorem :: NEWTON04:15

    

     F123: for f1,f2,f3 be complex-valued Function holds ((f1 (#) f2) (#) f3) = (f1 (#) (f2 (#) f3))

    proof

      let f1,f2,f3 be complex-valued Function;

      

       A1: ( dom ((f1 (#) f2) (#) f3)) = (( dom (f1 (#) f2)) /\ ( dom f3)) by VALUED_1:def 4

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by VALUED_1:def 4;

      

       A2: ( dom (f1 (#) (f2 (#) f3))) = (( dom f1) /\ ( dom (f2 (#) f3))) by VALUED_1:def 4

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VALUED_1:def 4;

      then

       A3: ( dom ((f1 (#) f2) (#) f3)) = ( dom (f1 (#) (f2 (#) f3))) by A1, XBOOLE_1: 16;

      for x be object st x in ( dom ((f1 (#) f2) (#) f3)) holds (((f1 (#) f2) (#) f3) . x) = ((f1 (#) (f2 (#) f3)) . x)

      proof

        let x be object such that

         B1: x in ( dom ((f1 (#) f2) (#) f3));

        x in ( dom (f1 (#) (f2 (#) f3))) by B1, A1, A2, XBOOLE_1: 16;

        then

         B2a: x in (( dom (f1 (#) f2)) /\ ( dom f3)) & x in (( dom f1) /\ ( dom (f2 (#) f3))) by VALUED_1:def 4, B1;

        

         B3: (((f1 (#) f2) (#) f3) . x) = (((f1 (#) f2) . x) * (f3 . x)) by VALUED_1:def 4, B1

        .= (((f1 . x) * (f2 . x)) * (f3 . x)) by B2a, VALUED_1:def 4;

        ((f1 (#) (f2 (#) f3)) . x) = ((f1 . x) * ((f2 (#) f3) . x)) by A3, B1, VALUED_1:def 4

        .= ((f1 . x) * ((f2 . x) * (f3 . x))) by B2a, VALUED_1:def 4;

        hence thesis by B3;

      end;

      hence thesis by A1, A2, XBOOLE_1: 16, FUNCT_1: 2;

    end;

    theorem :: NEWTON04:16

    for f,g be FinSequence of COMPLEX , i be object holds ((f (#) g) . i) = ((f . i) * (g . i))

    proof

      let f,g be FinSequence of COMPLEX , i be object;

      per cases ;

        suppose i in ( dom (f (#) g));

        hence thesis by VALUED_1:def 4;

      end;

        suppose

         B1: not i in ( dom (f (#) g));

        then not i in (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then not i in ( dom f) or not i in ( dom g) by XBOOLE_0:def 4;

        then ((f . i) = {} or (g . i) = {} ) & ((f (#) g) . i) = {} by B1, FUNCT_1:def 2;

        hence thesis;

      end;

    end;

    theorem :: NEWTON04:17

    for x,y be Real holds (( max (x,y)) - ( min (x,y))) = |.(x - y).|

    proof

      let x,y be Real;

      per cases ;

        suppose x >= y;

        then ( min (x,y)) = y & ( max (x,y)) = x by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis by ABSVALUE:def 1;

      end;

        suppose

         A1: x < y;

        then

         A2: ( min (x,y)) = x & ( max (x,y)) = y by XXREAL_0:def 9, XXREAL_0:def 10;

        (x - y) < (x - x) by A1, XREAL_1: 10;

        then |.(x - y).| = ( - (x - y)) by ABSVALUE:def 1;

        hence thesis by A2;

      end;

    end;

    theorem :: NEWTON04:18

    for x,y be Real holds (( min (x,y)) * ( max (x,y))) = (x * y) & (( min (x,y)) + ( max (x,y))) = (x + y)

    proof

      let x,y be Real;

      per cases ;

        suppose x >= y;

        then ( min (x,y)) = y & ( max (x,y)) = x by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose x < y;

        then ( min (x,y)) = x & ( max (x,y)) = y by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

    end;

    theorem :: NEWTON04:19

    

     SF: for f be nonnegative-yielding FinSequence of REAL holds ( Sum f) >= ( Sum (f | j))

    proof

      let f be nonnegative-yielding FinSequence of REAL ;

      

       A1: ((f | j) ^ (f /^ j)) = f by RFINSEQ: 8;

      (( Sum (f | j)) + ( Sum (f /^ j))) >= (( Sum (f | j)) + 0 ) by XREAL_1: 6;

      hence thesis by A1, RVSUM_1: 75;

    end;

    theorem :: NEWTON04:20

    for f be nonnegative-yielding FinSequence of REAL holds i >= j implies ( Sum (f | i)) >= ( Sum (f | j))

    proof

      let f be nonnegative-yielding FinSequence of REAL ;

      assume i >= j;

      then ( Sum ((f | i) | j)) = ( Sum (f | j)) by FINSEQ_1: 82;

      hence thesis by SF;

    end;

    theorem :: NEWTON04:21

    

     SN: for f be nonnegative-yielding FinSequence of REAL holds ( Sum f) >= (f . n)

    proof

      let f be nonnegative-yielding FinSequence of REAL ;

      per cases ;

        suppose not n in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

        suppose

         A0: n in ( dom f);

        then

         A0a: ( len f) >= n >= 1 by FINSEQ_3: 25;

        then

        reconsider k = (n - 1) as Nat;

        

         A0b: (k + 1) > (k + 0 ) by XREAL_1: 6;

        then ( len f) > k by A0a, XXREAL_0: 2;

        then

         A1: (f | (k + 1)) = ((f | k) ^ <*(f . (k + 1))*>) by FINSEQ_5: 83;

        

         A2: ( Sum f) = ( Sum (((f | k) ^ <*(f . (k + 1))*>) ^ (f /^ n))) by A1, RFINSEQ: 8

        .= (( Sum ((f | k) ^ <*(f . (k + 1))*>)) + ( Sum (f /^ n))) by RVSUM_1: 75

        .= ((( Sum (f | k)) + (f . (k + 1))) + ( Sum (f /^ n))) by RVSUM_1: 74;

        ((f . (k + 1)) + (( Sum (f | k)) + ( Sum (f /^ n)))) >= ((f . (k + 1)) + 0 ) by XREAL_1: 6;

        hence thesis by A2;

      end;

    end;

    theorem :: NEWTON04:22

    

     DLS: for f,g,h be FinSequence of COMPLEX st ( dom h) = (( dom f) /\ ( dom g)) holds ( len h) = ( min (( len f),( len g)))

    proof

      let f,g,h be FinSequence of COMPLEX such that

       A1: ( dom h) = (( dom f) /\ ( dom g));

      per cases ;

        suppose

         B1: ( len f) >= ( len g);

        then (( dom f) /\ ( dom g)) = ( dom g) by FINSEQ_3: 30, XBOOLE_1: 28;

        then ( len h) = ( len g) by A1, FINSEQ_3: 29;

        hence thesis by B1, XXREAL_0:def 9;

      end;

        suppose

         B1: ( len f) < ( len g);

        then (( dom f) /\ ( dom g)) = ( dom f) by FINSEQ_3: 30, XBOOLE_1: 28;

        then ( len h) = ( len f) by A1, FINSEQ_3: 29;

        hence thesis by B1, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON04:23

    

     FLS: for f,g be FinSequence of COMPLEX holds ( len (f + g)) = ( min (( len f),( len g)))

    proof

      let f,g be FinSequence of COMPLEX ;

      reconsider h = (f + g) as FinSequence of COMPLEX by NEWTON02: 103;

      ( dom h) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

      hence thesis by DLS;

    end;

    theorem :: NEWTON04:24

    for f,g be FinSequence of COMPLEX holds ( len (f (#) g)) = ( min (( len f),( len g)))

    proof

      let f,g be FinSequence of COMPLEX ;

      reconsider h = (f (#) g) as FinSequence of COMPLEX by NEWTON02: 103;

      ( dom h) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

      hence thesis by DLS;

    end;

    theorem :: NEWTON04:25

    for f,g be FinSequence of COMPLEX holds ( len (f - g)) = ( min (( len f),( len g)))

    proof

      let f,g be FinSequence of COMPLEX ;

      reconsider h = ( - g) as FinSequence of COMPLEX by NEWTON02: 103;

      h = (( - 1) (#) g) by VALUED_1:def 6;

      then ( dom h) = ( dom g) by VALUED_1:def 5;

      then

       A1: ( len h) = ( len g) by FINSEQ_3: 29;

      (f - g) = (f + h) by VALUED_1:def 9;

      hence thesis by FLS, A1;

    end;

    theorem :: NEWTON04:26

    

     FS: for f,g be nonnegative-yielding FinSequence of REAL holds ((f (#) g) . n) <= (( Sum f) * (g . n))

    proof

      let f,g be nonnegative-yielding FinSequence of REAL ;

      per cases ;

        suppose n in ( dom (f (#) g));

        then ((f (#) g) . n) = ((f . n) * (g . n)) by VALUED_1:def 4;

        hence thesis by SN, XREAL_1: 64;

      end;

        suppose not n in ( dom (f (#) g));

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: NEWTON04:27

    for r be Real, n be non zero Nat holds ex f be FinSequence of REAL st ( len f) = n & ( Sum f) = r

    proof

      let r be Real, n be non zero Nat;

      reconsider k = (n - 1) as Nat;

       0 in REAL by XREAL_0:def 1;

      then

      reconsider g = (k |-> 0 ) as FinSequence of REAL by FINSEQ_2: 63;

      reconsider h = (g ^ <*r*>) as FinSequence of REAL by RVSUM_1: 145;

      

       A1: ( len (g ^ <*r*>)) = (( len g) + 1) by FINSEQ_2: 16

      .= (k + 1);

      ( Sum (g ^ <*r*>)) = (( Sum (k |-> 0 )) + r) by RVSUM_1: 74

      .= ( 0 + r);

      then ( Sum h) = r & ( len h) = (k + 1) by A1;

      hence thesis;

    end;

    

     LmFG: for f,g be FinSequence of REAL st (for x be Nat holds (f . x) >= (g . x)) holds ( Sum (f | ( min (( len f),( len g))))) >= ( Sum (g | ( min (( len f),( len g)))))

    proof

      let f,g be FinSequence of REAL such that

       A0: for x be Nat holds (f . x) >= (g . x);

      set i = ( min (( len f),( len g))), h = (f | i), j = (g | i);

      per cases ;

        suppose f is empty or g is empty;

        then ( min (( len f),( len g))) = 0 by XXREAL_0:def 9;

        hence thesis;

      end;

        suppose f is non empty & g is non empty;

        then ( len f) >= 1 & ( len g) >= 1 by FINSEQ_1: 20;

        then ( min (( len f),( len g))) >= 1 by XXREAL_0:def 9;

        then

         A3: i in ( dom f) & i in ( dom g) by XXREAL_0: 17, FINSEQ_3: 25;

        then

         A4: ( len h) = i & ( len j) = i by NEWTON02: 110;

        for k be Element of NAT st k in ( dom j) holds (j . k) <= (h . k)

        proof

          let k be Element of NAT ;

          assume k in ( dom j);

          then i >= k >= 1 by A4, FINSEQ_3: 25;

          then ((f | i) . k) = (f . k) & ((g | i) . k) = (g . k) by A3, NEWTON02: 107;

          hence thesis by A0;

        end;

        hence thesis by A4, INTEGRA5: 3;

      end;

    end;

    theorem :: NEWTON04:28

    

     SL: for f be FinSequence of COMPLEX , x be Complex holds (f + x) = (f + (( len f) |-> x))

    proof

      let f be FinSequence of COMPLEX , x be Complex;

      reconsider g = (( len f) |-> x) as FinSequence of COMPLEX by NEWTON02: 103;

      

       A0: ( dom (f + x)) = ( dom f) by VALUED_1:def 2;

      

       A2: ( len (f + g)) = ( min (( len f),( len (( len f) |-> x)))) by FLS

      .= ( len f);

      for i be Nat st i in ( dom (f + x)) holds ((f + x) . i) = ((f + g) . i)

      proof

        let i be Nat such that

         B1: i in ( dom (f + x));

        

         B2: i in ( dom f) by B1, VALUED_1:def 2;

        reconsider i as non zero Nat by B1, FINSEQ_3: 25;

        ( len f) >= i by B2, FINSEQ_3: 25;

        then

        reconsider k = (( len f) - i) as Element of NAT by NAT_1: 21;

        i in ( dom (f + g)) by A2, B2, FINSEQ_3: 29;

        

        then ((f + g) . i) = ((f . i) + (((k + i) |-> x) . i)) by VALUED_1:def 1

        .= ((f . i) + x);

        hence thesis by B1, VALUED_1:def 2;

      end;

      hence thesis by A0, FINSEQ_3: 29, A2, FINSEQ_2: 9;

    end;

    theorem :: NEWTON04:29

    

     SFX: for f be FinSequence of COMPLEX , x be Complex holds ( Sum (f + x)) = (( Sum f) + (x * ( len f)))

    proof

      let f be FinSequence of COMPLEX , x be Complex;

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

      set k = ( len f), g = (( len f) |-> x);

      (f null {} ) is k -element;

      then

      reconsider f as k -element FinSequence of COMPLEX ;

      reconsider h = (f + x) as FinSequence of COMPLEX by RVSUM_1: 146;

      ( dom f) = ( dom (f + x)) by VALUED_1:def 2;

      then ( len f) = ( len (f + x)) by FINSEQ_3: 29;

      then (h null {} ) is k -element;

      then

      reconsider h as k -element FinSequence of COMPLEX ;

      ( Sum (f + x)) = ( Sum (f + g)) by SL

      .= (( Sum f) + ( Sum (( len f) |-> x))) by RVSUM_2: 40

      .= (( Sum f) + (( len f) * x)) by RVSUM_2: 36;

      hence thesis;

    end;

    theorem :: NEWTON04:30

    for f be complex-valued FinSequence, x be Complex holds ( Sum (f - x)) = (( Sum f) - (x * ( len f)))

    proof

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

      reconsider f as FinSequence of COMPLEX by RVSUM_1: 146;

      ( Sum (f + ( - x))) = (( Sum f) + (( - x) * ( len f))) by SFX;

      hence thesis by VALUED_1:def 3;

    end;

    theorem :: NEWTON04:31

    for f be FinSequence of REAL , g be nonnegative-yielding FinSequence of REAL st (for x be Nat holds (f . x) >= (g . x)) holds f is nonnegative-yielding

    proof

      let f be FinSequence of REAL , g be nonnegative-yielding FinSequence of REAL such that

       A1: for x be Nat holds (f . x) >= (g . x);

      for r be Real st r in ( rng f) holds r >= 0

      proof

        let r be Real such that

         B0: r in ( rng f);

        consider k be object such that

         B1: k in ( dom f) & r = (f . k) by B0, FUNCT_1:def 3;

        reconsider k as Nat by B1;

        (g . k) >= 0 ;

        hence thesis by B1, A1;

      end;

      hence thesis by PARTFUN3:def 4;

    end;

    theorem :: NEWTON04:32

    

     NYS: for f,g be FinSequence of REAL st (for x be Nat holds (f . x) >= (g . x)) holds ( Sum f) >= ( Sum g)

    proof

      let f,g be FinSequence of REAL such that

       A0: for x be Nat holds (f . x) >= (g . x);

      per cases ;

        suppose ( len f) <= ( len g);

        then ( len f) = ( min (( len f),( len g))) by XXREAL_0:def 9;

        then

         B1: ( Sum (f | ( len f))) >= ( Sum (g | ( len f))) by A0, LmFG;

        for r be Real st r in ( rng (g /^ ( len f))) holds r <= 0

        proof

          let r be Real such that

           C1: r in ( rng (g /^ ( len f)));

          consider k be object such that

           C2: k in ( dom (g /^ ( len f))) & r = ((g /^ ( len f)) . k) by C1, FUNCT_1:def 3;

          reconsider k as non zero Nat by C2, FINSEQ_3: 25;

          

           C4: (( len f) + k) in ( dom g) by C2, FINSEQ_5: 26;

          r = ((g /^ ( len f)) /. k) by C2, PARTFUN1:def 6

          .= (g /. (( len f) + k)) by C2, FINSEQ_5: 27

          .= (g . (( len f) + k)) by PARTFUN1:def 6, C4;

          then r <= (f . (( len f) + k)) by A0;

          hence thesis;

        end;

        then

        reconsider h = (g /^ ( len f)) as nonpositive-yielding FinSequence of REAL by PARTFUN3:def 3;

        

         C5: ( Sum g) = ( Sum ((g | ( len f)) ^ (g /^ ( len f)))) by RFINSEQ: 8

        .= (( Sum (g | ( len f))) + ( Sum (g /^ ( len f)))) by RVSUM_1: 75;

        ( Sum h) <= 0 ;

        then (( Sum (g | ( len f))) + 0 ) >= (( Sum (g | ( len f))) + ( Sum (g /^ ( len f)))) by XREAL_1: 6;

        hence thesis by B1, C5, XXREAL_0: 2;

      end;

        suppose ( len f) > ( len g);

        then ( len g) = ( min (( len f),( len g))) by XXREAL_0:def 9;

        then

         B1: ( Sum (f | ( len g))) >= ( Sum (g | ( len g))) by A0, LmFG;

        for r be Real st r in ( rng (f /^ ( len g))) holds r >= 0

        proof

          let r be Real such that

           C1: r in ( rng (f /^ ( len g)));

          consider k be object such that

           C2: k in ( dom (f /^ ( len g))) & r = ((f /^ ( len g)) . k) by C1, FUNCT_1:def 3;

          reconsider k as non zero Nat by C2, FINSEQ_3: 25;

          

           C4: (( len g) + k) in ( dom f) by C2, FINSEQ_5: 26;

          r = ((f /^ ( len g)) /. k) by C2, PARTFUN1:def 6

          .= (f /. (( len g) + k)) by C2, FINSEQ_5: 27

          .= (f . (( len g) + k)) by PARTFUN1:def 6, C4;

          then r >= (g . (( len g) + k)) by A0;

          hence thesis;

        end;

        then

        reconsider h = (f /^ ( len g)) as nonnegative-yielding FinSequence of REAL by PARTFUN3:def 4;

        

         C5: ( Sum f) = ( Sum ((f | ( len g)) ^ (f /^ ( len g)))) by RFINSEQ: 8

        .= (( Sum (f | ( len g))) + ( Sum (f /^ ( len g)))) by RVSUM_1: 75;

        ( Sum h) >= 0 ;

        then (( Sum (f | ( len g))) + 0 ) <= (( Sum (f | ( len g))) + ( Sum (f /^ ( len g)))) by XREAL_1: 6;

        hence thesis by B1, C5, XXREAL_0: 2;

      end;

    end;

    theorem :: NEWTON04:33

    

     S1: for f be FinSequence of COMPLEX holds ( Sum (f | 1 qua Nat)) = (f . 1 qua Nat)

    proof

      let f be FinSequence of COMPLEX ;

      per cases ;

        suppose not f is empty;

        then (f | 1) = <*(f . 1)*> by FINSEQ_5: 20;

        hence thesis;

      end;

        suppose

         B1: f is empty;

        

        then ( Sum (f | 1)) = 0 by RVSUM_2: 29

        .= (f . 1) by B1;

        hence thesis;

      end;

    end;

    theorem :: NEWTON04:34

    

     S2: for f be FinSequence of COMPLEX , n be Nat holds ( Sum ((f /^ n) | 1)) = (f . (n + 1))

    proof

      let f be FinSequence of COMPLEX , n be Nat;

      per cases ;

        suppose

         A1: 1 in ( dom (f /^ n));

        ( Sum ((f /^ n) | 1)) = ((f /^ n) . 1) by S1

        .= (f . (n + 1)) by A1, FINSEQ_7: 4;

        hence thesis;

      end;

        suppose not 1 in ( dom (f /^ n));

        then

         A1: (f /^ n) is empty by FINSEQ_5: 6;

        

        then 0 = ( len (f /^ n))

        .= (( len f) -' n) by RFINSEQ: 29;

        then ( len f) = n or ( 0 + n) >= ((( len f) - n) + n) by XREAL_0:def 2, XREAL_1: 6;

        then (( len f) + 0 ) < (n + 1) by XREAL_1: 8;

        then

         A2: not (n + 1) in ( dom f) by FINSEQ_3: 25;

        ( Sum ((f /^ n) | 1)) = 0 by A1, RVSUM_2: 29

        .= (f . (n + 1)) by A2, FUNCT_1:def 2;

        hence thesis;

      end;

    end;

    theorem :: NEWTON04:35

    

     FINSEQ681: for f be FinSequence, a,b be Nat holds ((f /^ a) /^ b) = (f /^ (a + b))

    proof

      let f be FinSequence, a,b be Nat;

      ex D be non empty set st f is FinSequence of D by Th0;

      hence thesis by FINSEQ_6: 81;

    end;

    theorem :: NEWTON04:36

    for f be FinSequence of COMPLEX holds f = (((f | i) ^ ((f /^ i) | 1 qua Nat)) ^ (f /^ (i + 1)))

    proof

      let f be FinSequence of COMPLEX ;

      f = ((f | i) ^ (f /^ i)) by RFINSEQ: 8

      .= ((f | i) ^ (((f /^ i) | 1) ^ ((f /^ i) /^ 1))) by RFINSEQ: 8

      .= (((f | i) ^ ((f /^ i) | 1)) ^ ((f /^ i) /^ 1)) by FINSEQ_1: 32

      .= (((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))) by FINSEQ681;

      hence thesis;

    end;

    theorem :: NEWTON04:37

    

     SUM: for f be FinSequence of COMPLEX holds ( Sum f) = ((( Sum (f | i)) + (f . (i + 1))) + ( Sum (f /^ (i + 1))))

    proof

      let f be FinSequence of COMPLEX ;

      set f1 = (f | i), f2 = (f /^ i), k = 1, f4 = (f2 /^ k);

      ( Sum f) = ( Sum (f1 ^ f2)) by RFINSEQ: 8

      .= (( Sum (f | i)) + ( Sum f2)) by RVSUM_2: 32

      .= (( Sum (f | i)) + ( Sum ((f2 | k) ^ (f2 /^ k)))) by RFINSEQ: 8

      .= (( Sum (f | i)) + (( Sum (f2 | k)) + ( Sum (f2 /^ k)))) by RVSUM_2: 32

      .= (( Sum (f | i)) + (( Sum (f2 | k)) + ( Sum (f /^ (i + k))))) by FINSEQ681

      .= ((( Sum (f | i)) + ( Sum (f2 | k))) + ( Sum (f /^ (i + k))));

      hence thesis by S2;

    end;

    theorem :: NEWTON04:38

    

     FINSEQ74: for f be FinSequence, i be non zero Nat holds (f . (n + i)) = ((f /^ n) . i)

    proof

      let f be FinSequence, i be non zero Nat;

      consider D be non empty set such that

       A0: f is FinSequence of D by Th0;

      reconsider f as FinSequence of D by A0;

      per cases ;

        suppose

         B1: not i in ( dom (f /^ n));

        

         B2: ((f /^ n) . i) = 0 by B1, FUNCT_1:def 2;

        (n + i) > ( len f)

        proof

          i >= 1 by NAT_1: 14;

          then i > ( len (f /^ n)) by B1, FINSEQ_3: 25;

          then

           C1: i > (( len f) -' n) by RFINSEQ: 29;

          per cases ;

            suppose

             D1: ( len f) < n;

            (n + i) >= (n + 0 ) by XREAL_1: 6;

            hence thesis by D1, XXREAL_0: 2;

          end;

            suppose ( len f) >= n;

            then (( len f) - n) >= (n - n) by XREAL_1: 9;

            then (( len f) -' n) = (( len f) - n) by XREAL_0:def 2;

            then (i + n) > ((( len f) - n) + n) by C1, XREAL_1: 6;

            hence thesis;

          end;

        end;

        then not (n + i) in ( dom f) by FINSEQ_3: 25;

        hence thesis by B2, FUNCT_1:def 2;

      end;

        suppose i in ( dom (f /^ n));

        hence thesis by FINSEQ_7: 4;

      end;

    end;

    theorem :: NEWTON04:39

    

     NYS1: for f,g be FinSequence of REAL st (for x be Nat holds (f . x) >= (g . x) & ex i st (f . (i + 1)) > (g . (i + 1))) holds ( Sum f) > ( Sum g)

    proof

      let f,g be FinSequence of REAL such that

       A1: for x be Nat holds (f . x) >= (g . x) & ex i be Nat st (f . (i + 1)) > (g . (i + 1));

      consider i be Nat such that

       A2: (f . (i + 1)) > (g . (i + 1)) by A1;

      f is FinSequence of COMPLEX by RVSUM_1: 146;

      then

       A5: ( Sum f) = ((( Sum (f | i)) + (f . (i + 1))) + ( Sum (f /^ (i + 1)))) by SUM;

      g is FinSequence of COMPLEX by RVSUM_1: 146;

      then

       A6: ( Sum g) = ((( Sum (g | i)) + (g . (i + 1))) + ( Sum (g /^ (i + 1)))) by SUM;

      for x be Nat holds ((f | i) . x) >= ((g | i) . x) & ((f /^ (i + 1)) . x) >= ((g /^ (i + 1)) . x)

      proof

        let x be Nat;

        

         B0: i >= x implies ((f | i) . x) = (f . x) & ((g | i) . x) = (g . x) by FINSEQ_3: 112;

        ( len (f | i)) <= i & ( len (g | i)) <= i by FINSEQ_5: 17;

        then i < x implies ( len (f | i)) < x & ( len (g | i)) < x by XXREAL_0: 2;

        then i < x implies not x in ( dom (f | i)) & not x in ( dom (g | i)) by FINSEQ_3: 25;

        then

         B2: i < x implies ((f | i) . x) = 0 & 0 = ((g | i) . x) by FUNCT_1:def 2;

        x <> 0 implies ((f . ((i + 1) + x)) = ((f /^ (i + 1)) . x) & (g . ((i + 1) + x)) = ((g /^ (i + 1)) . x)) by FINSEQ74;

        hence thesis by A1, B0, B2;

      end;

      then ( Sum (f | i)) >= ( Sum (g | i)) & ( Sum (f /^ (i + 1))) >= ( Sum (g /^ (i + 1))) by NYS;

      then (( Sum (f | i)) + ( Sum (f /^ (i + 1)))) >= (( Sum (g | i)) + ( Sum (g /^ (i + 1)))) by XREAL_1: 7;

      then

       A7: ((( Sum (f | i)) + ( Sum (f /^ (i + 1)))) + (f . (i + 1))) >= ((( Sum (g | i)) + ( Sum (g /^ (i + 1)))) + (f . (i + 1))) by XREAL_1: 6;

      ((( Sum (g | i)) + ( Sum (g /^ (i + 1)))) + (f . (i + 1))) > ((( Sum (g | i)) + ( Sum (g /^ (i + 1)))) + (g . (i + 1))) by A2, XREAL_1: 6;

      hence thesis by A5, A6, A7, XXREAL_0: 2;

    end;

    theorem :: NEWTON04:40

    for f,g be nonnegative-yielding FinSequence of REAL holds (( Sum f) * ( Sum g)) >= ( Sum (f (#) g))

    proof

      let f,g be nonnegative-yielding FinSequence of REAL ;

      

       A1: (f (#) g) is FinSequence of REAL & (( Sum f) * g) is FinSequence of REAL by NEWTON02: 103;

      now

        let i be Nat;

        (( Sum f) * (g . i)) = ((( Sum f) (#) g) . i) by VALUED_1: 6;

        hence ((f (#) g) . i) <= ((( Sum f) * g) . i) by FS;

      end;

      then ( Sum (f (#) g)) <= ( Sum (( Sum f) * g)) by A1, NYS;

      hence thesis by RVSUM_1: 87;

    end;

    theorem :: NEWTON04:41

    for a be Complex, f be complex-valued FinSequence holds ((( len f) |-> a) (#) f) = (a (#) f)

    proof

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

      ( len (( len f) |-> a)) = ( len f);

      then ( dom (( len f) |-> a)) = ( dom f) by FINSEQ_3: 29;

      then

       A1: (( dom (( len f) |-> a)) /\ ( dom f)) = ( dom (a (#) f)) by VALUED_1:def 5;

      then

       A2: ( dom ((( len f) |-> a) (#) f)) = ( dom (a (#) f)) by VALUED_1:def 4;

      for x be object st x in ( dom ((( len f) |-> a) (#) f)) holds (((( len f) |-> a) (#) f) . x) = ((a (#) f) . x)

      proof

        let x be object such that

         B1: x in ( dom ((( len f) |-> a) (#) f));

        reconsider x as non zero Nat by B1, FINSEQ_3: 25;

        ( len (( len f) |-> a)) >= x >= 1 by A1, A2, B1, FINSEQ_3: 25;

        then ex k be Nat st ( len f) = (x + k) by NAT_1: 10;

        then

        reconsider k = (( len f) - x) as Nat;

        (((( len f) |-> a) (#) f) . x) = ((((x + k) |-> a) . x) * (f . x)) by B1, VALUED_1:def 4

        .= ((a (#) f) . x) by A2, B1, VALUED_1:def 5;

        hence thesis;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: NEWTON04:42

    

     AMP: for a,b be Complex holds (a (#) <*b*>) = <*(a * b)*>

    proof

      let a,b be Complex;

      

       A1: ( dom <*(a * b)*>) = ( Seg 1) & ( dom <*b*>) = ( Seg 1) by FINSEQ_1:def 8;

      for x be object st x in ( Seg 1) holds ( <*(a * b)*> . x) = (a * ( <*b*> . x))

      proof

        let x be object;

        assume x in ( Seg 1);

        then x = 1 by FINSEQ_1: 2, TARSKI:def 1;

        hence thesis;

      end;

      hence thesis by A1, VALUED_1:def 5;

    end;

    theorem :: NEWTON04:43

    

     ADP: for a be Complex, f,g be complex-valued FinSequence holds (a (#) (f ^ g)) = ((a (#) f) ^ (a (#) g))

    proof

      let a be Complex, f,g be complex-valued FinSequence;

      

       A0: ( dom (a (#) (f ^ g))) = ( dom (f ^ g)) & ( dom (a (#) f)) = ( dom f) & ( dom (a (#) g)) = ( dom g) by VALUED_1:def 5;

      then

       A1: ( len (a (#) (f ^ g))) = ( len (f ^ g)) & ( len (a (#) f)) = ( len f) & ( len (a (#) g)) = ( len g) by FINSEQ_3: 29;

      

      then ( len (a (#) (f ^ g))) = (( len (a (#) f)) + ( len (a (#) g))) by FINSEQ_1: 22

      .= ( len ((a (#) f) ^ (a (#) g))) by FINSEQ_1: 22;

      then

       A2: ( dom (a (#) (f ^ g))) = ( dom ((a (#) f) ^ (a (#) g))) by FINSEQ_3: 29;

      for x be object st x in ( dom (a (#) (f ^ g))) holds ((a (#) (f ^ g)) . x) = (((a (#) f) ^ (a (#) g)) . x)

      proof

        let x be object such that

         B1: x in ( dom (a (#) (f ^ g)));

        per cases ;

          suppose

           C1: x in ( dom f);

          then

           C2: x in ( dom (a (#) f)) by VALUED_1:def 5;

          

          then (((a (#) f) ^ (a (#) g)) . x) = ((a (#) f) . x) by FINSEQ_1:def 7

          .= (a * (f . x)) by C2, VALUED_1:def 5

          .= (a * ((f ^ g) . x)) by C1, FINSEQ_1:def 7

          .= ((a (#) (f ^ g)) . x) by B1, VALUED_1:def 5;

          hence thesis;

        end;

          suppose

           C0: not x in ( dom f);

          x in ( dom (f ^ g)) by VALUED_1:def 5, B1;

          then

          consider n be Nat such that

           C2: n in ( dom g) & x = (( len f) + n) by C0, FINSEQ_1: 25;

          (((a (#) f) ^ (a (#) g)) . (( len f) + n)) = ((a (#) g) . n) by A0, A1, C2, FINSEQ_1:def 7

          .= (a * (g . n)) by A0, C2, VALUED_1:def 5

          .= (a * ((f ^ g) . (( len f) + n))) by C2, FINSEQ_1:def 7

          .= ((a (#) (f ^ g)) . x) by C2, B1, VALUED_1:def 5;

          hence thesis by C2;

        end;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: NEWTON04:44

    

     CREV: for a be Complex, f,g be complex-valued FinSequence st g = ( Rev f) holds ( Rev (a (#) f)) = (a (#) g)

    proof

      let a be Complex, f,g be complex-valued FinSequence such that

       A1: g = ( Rev f);

      set h = (a (#) f), h1 = (a (#) g), h2 = ( Rev h);

      

       A2: ( dom h1) = ( dom g) & ( dom h) = ( dom f) by VALUED_1:def 5;

      

       A4: ( dom ( Rev h)) = ( dom h) & ( dom ( Rev f)) = ( dom f) by FINSEQ_5: 57;

      then

       A5: ( len h1) = ( len h2) & ( len h2) = ( len f) & ( len f) = ( len h) & ( len g) = ( len f) by A1, A2, FINSEQ_3: 29;

      reconsider h1 as ( len f) -element complex-valued FinSequence by A5;

      for x be object st x in ( dom h1) holds (h1 . x) = (h2 . x)

      proof

        let x be object such that

         B1: x in ( dom h1);

        reconsider x as Nat by B1;

        

         B3: 1 <= x <= ( len f) by B1, A1, A2, A4, FINSEQ_3: 25;

        then

        reconsider k = (( len f) - x) as Element of NAT by NAT_1: 21;

        set l = (k + 1);

        

         B4: ( 0 + 1) <= (k + 1) & (k + 1) <= (k + x) by B3, XREAL_1: 6;

        (( Rev h) . x) = (h . ((( len h) - x) + 1)) by B1, A1, A2, A4, FINSEQ_5:def 3

        .= ((a (#) f) . l) by A2, FINSEQ_3: 29

        .= (a * (( Rev ( Rev f)) . l)) by A2, B4, FINSEQ_3: 25, VALUED_1:def 5

        .= (a * (g . ((( len g) - l) + 1))) by A1, A4, B4, FINSEQ_3: 25, FINSEQ_5:def 3

        .= (a * (g . x)) by A5;

        hence thesis by B1, VALUED_1:def 5;

      end;

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

    end;

    definition

      let a,b be Real;

      let n be natural Number;

      :: NEWTON04:def1

      func (a,b) Subnomial n -> FinSequence of REAL equals (((a,b) In_Power n) /" ( Newton_Coeff n));

      correctness by NEWTON02: 103;

    end

    theorem :: NEWTON04:45

    

     DOMN: for a,b be Real, n be Nat holds ( len ((a,b) In_Power n)) = ( len ( Newton_Coeff n)) & ( len ((a,b) Subnomial n)) = ( len ( Newton_Coeff n)) & ( len ((a,b) In_Power n)) = ( len ((a,b) Subnomial n)) & ( dom ((a,b) In_Power n)) = ( dom ( Newton_Coeff n)) & ( dom ((a,b) Subnomial n)) = ( dom ( Newton_Coeff n)) & ( dom ((a,b) In_Power n)) = ( dom ((a,b) Subnomial n))

    proof

      let a,b be Real, n be Nat;

      ( len ((a,b) In_Power ((n + 1) - 1))) = ( len ( Newton_Coeff n));

      then

       A2: ( dom ((a,b) In_Power n)) = ( dom ( Newton_Coeff n)) by FINSEQ_3: 29;

      ( dom (((a,b) In_Power n) /" ( Newton_Coeff n))) = (( dom ((a,b) In_Power n)) /\ ( dom ( Newton_Coeff n))) by VALUED_1: 16;

      hence thesis by A2, FINSEQ_3: 29;

    end;

    registration

      let a,b be Real, n be Nat;

      reduce ( len ((a,b) Subnomial ((n + 1) - 1))) to (n + 1);

      reducibility

      proof

        ( len ((a,b) Subnomial ((n + 1) - 1))) = ( len ( Newton_Coeff ((n + 1) - 1))) by DOMN;

        hence thesis;

      end;

      cluster ((a,b) Subnomial n) -> (n + 1) -element;

      coherence

      proof

        (((a,b) Subnomial ((n + 1) - 1)) null n) is (n + 1) -element;

        hence thesis;

      end;

    end

    registration

      let a,b be Integer;

      let n,m be Nat;

      cluster (((a,b) In_Power n) . m) -> integer;

      coherence

      proof

        per cases ;

          suppose

           A0: m in ( dom ((a,b) In_Power n));

          then

          consider k such that

           A1: m = (1 + k) by NAT_1: 10, FINSEQ_3: 25;

          ( len ((a,b) In_Power n)) = (n + 1) by NEWTON:def 4;

          then n >= k by A0, FINSEQ_3: 25, A1, XREAL_1: 6;

          then

          consider l such that

           A2: n = (k + l) by NAT_1: 10;

          k = (m - 1) & l = (n - k) by A1, A2;

          then (((a,b) In_Power n) . m) = (((n choose k) * (a |^ l)) * (b |^ k)) by A0, NEWTON:def 4;

          hence thesis;

        end;

          suppose not m in ( dom ((a,b) In_Power n));

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let a,b be Integer;

      let n be Nat;

      cluster ((a,b) In_Power n) -> INT -valued;

      coherence

      proof

        for k st k in ( dom ((a,b) In_Power n)) holds (((a,b) In_Power n) . k) in INT by INT_1:def 2;

        hence thesis by FINSEQ_2: 12;

      end;

    end

    theorem :: NEWTON04:46

    

     NIS: for a,b be Integer, k be Nat st k in ( dom ( Newton_Coeff n)) holds (( Newton_Coeff n) . k) divides (((a,b) In_Power n) . k)

    proof

      let a,b be Integer, k be Nat such that

       A0: k in ( dom ( Newton_Coeff n));

      

       A0a: k >= 1 by A0, FINSEQ_3: 25;

      then

      reconsider m = (k - 1) as Nat;

      

       A1: (n + 1) = ( len ((a,b) In_Power n)) by NEWTON:def 4;

      ( len ( Newton_Coeff n)) = (n + 1) by NEWTON:def 5;

      then

       A1a: (n + 1) >= (m + 1) by A0, FINSEQ_3: 25;

      then

      consider l such that

       A2: n = (m + l) by XREAL_1: 6, NAT_1: 10;

      

       A3: (( Newton_Coeff n) . k) = (n choose m) by A0, NEWTON:def 5;

      

       A4: k in ( dom ((a,b) In_Power n)) by A0a, A1, A1a, FINSEQ_3: 25;

      l = (n - m) by A2;

      

      then (((a,b) In_Power n) . k) = (((n choose m) * (a |^ l)) * (b |^ m)) by A4, NEWTON:def 4

      .= ((( Newton_Coeff n) . k) * ((a |^ l) * (b |^ m))) by A3;

      hence thesis;

    end;

    registration

      let l,k be Nat;

      cluster ((l + k) choose k) -> positive;

      coherence

      proof

        reconsider n = (l + k) as Nat;

        l = (n - k) & n >= k by NAT_1: 11;

        then (n choose k) = ((n ! ) / ((k ! ) * (l ! ))) by NEWTON:def 3;

        hence thesis;

      end;

    end

    registration

      let l be Nat, k be non zero Nat;

      cluster (l choose (l + k)) -> zero;

      coherence

      proof

        (l + 0 ) < (l + k) by XREAL_1: 6;

        hence thesis by NEWTON:def 3;

      end;

      cluster (( Newton_Coeff l) . ((l + k) + 1)) -> zero;

      coherence

      proof

        ( len ( Newton_Coeff l)) = (l + 1) & ((l + 1) + 0 ) < ((l + 1) + k) by XREAL_1: 6, NEWTON:def 5;

        hence thesis;

      end;

    end

    registration

      let l be Nat, k be Nat;

      cluster (( Newton_Coeff (l + k)) . (k + 1)) -> positive;

      coherence

      proof

        ((k + 1) + l) >= ((k + 1) + 0 ) & (k + 1) >= ( 0 + 1) by XREAL_1: 6;

        then ( len ( Newton_Coeff (l + k))) >= (k + 1) & (k + 1) >= 1 by NEWTON:def 5;

        then (k + 1) in ( dom ( Newton_Coeff (l + k))) by FINSEQ_3: 25;

        then (( Newton_Coeff (l + k)) . (k + 1)) = ((l + k) choose ((k + 1) - 1)) by NEWTON:def 5;

        hence thesis;

      end;

    end

    theorem :: NEWTON04:47

    

     D1: for k,l be Nat holds k in ( dom ( Newton_Coeff l)) implies (( Newton_Coeff l) . k) is non zero

    proof

      let k,l be Nat;

      assume k in ( dom ( Newton_Coeff l));

      then

       A1: ( len ( Newton_Coeff l)) = (l + 1) & ( len ( Newton_Coeff l)) >= k & k >= 1 by FINSEQ_3: 25, NEWTON:def 5;

      then

      reconsider i = (k - 1) as Nat;

      consider m be Nat such that

       A2: (l + 1) = (k + m) by A1, NAT_1: 10;

      (( Newton_Coeff (m + i)) . (i + 1)) is non zero;

      hence thesis by A2;

    end;

    registration

      let a,b be Integer;

      let m,n be Nat;

      cluster (((a,b) Subnomial n) . m) -> integer;

      coherence

      proof

        per cases ;

          suppose

           A0: m in ( dom ( Newton_Coeff n));

          then (( Newton_Coeff n) . m) divides (((a,b) In_Power n) . m) by NIS;

          then

          consider x be Integer such that

           A2: (((a,b) In_Power n) . m) = ((( Newton_Coeff n) . m) * x);

          (( Newton_Coeff n) . m) <> 0 by A0, D1;

          then x = ((((a,b) In_Power n) . m) / (( Newton_Coeff n) . m)) by A2, XCMPLX_1: 89;

          hence thesis by VALUED_1: 17;

        end;

          suppose not m in ( dom ( Newton_Coeff n));

          then (( Newton_Coeff n) . m) = 0 by FUNCT_1:def 2;

          then 0 = ((((a,b) In_Power n) . m) / (( Newton_Coeff n) . m)) by XCMPLX_1: 49;

          hence thesis by VALUED_1: 17;

        end;

      end;

    end

    registration

      let a,b be Integer;

      let n be Nat;

      cluster ((a,b) Subnomial n) -> INT -valued;

      coherence

      proof

        for k st k in ( dom ((a,b) Subnomial n)) holds (((a,b) Subnomial n) . k) in INT by INT_1:def 2;

        hence thesis by FINSEQ_2: 12;

      end;

    end

    

     LmS1: for a,b be Real, n be Nat holds for i,l,m be Nat st i in ( dom ((a,b) Subnomial n)) & m = (i - 1) & l = (n - m) holds (((a,b) Subnomial n) . i) = ((a |^ l) * (b |^ m))

    proof

      let a,b be Real, n be Nat;

      let i,l,m be Nat such that

       A1: i in ( dom ((a,b) Subnomial n)) & m = (i - 1) & l = (n - m);

      ( dom ( Newton_Coeff n)) = ( dom ((a,b) Subnomial n)) & ( dom ( Newton_Coeff n)) = ( dom ((a,b) In_Power n)) by DOMN;

      then

       A2: (((a,b) In_Power n) . i) = (((n choose m) * (a |^ l)) * (b |^ m)) & (( Newton_Coeff n) . i) = (n choose m) by A1, NEWTON:def 4, NEWTON:def 5;

      (((a,b) Subnomial n) . i) = ((((m + l) choose m) * ((a |^ l) * (b |^ m))) / ((m + l) choose m)) by A1, A2, VALUED_1: 17

      .= ((a |^ l) * (b |^ m)) by XCMPLX_1: 89;

      hence thesis;

    end;

    definition

      let a,b be Real, n be Nat;

      :: original: Subnomial

      redefine

      :: NEWTON04:def2

      func (a,b) Subnomial n -> FinSequence of REAL means

      : Def2: ( len it ) = (n + 1) & for i,l,m be Nat st i in ( dom it ) & m = (i - 1) & l = (n - m) holds (it . i) = ((a |^ l) * (b |^ m));

      compatibility

      proof

        let f be FinSequence of REAL ;

        

         L1: ( len ((a,b) Subnomial n)) = ( len ((a,b) Subnomial ((n + 1) - 1)))

        .= (n + 1);

        

         L2: ( len f) = ( len ((a,b) Subnomial n)) iff ( dom f) = ( dom ((a,b) Subnomial n)) by FINSEQ_3: 29;

        (( len f) = ( len ((a,b) Subnomial n)) & for i,l,m be Nat st i in ( dom ((a,b) Subnomial n)) & m = (i - 1) & l = (n - m) holds (f . i) = ((a |^ l) * (b |^ m))) implies f = ((a,b) Subnomial n)

        proof

          assume

           A3: (( len f) = ( len ((a,b) Subnomial n)) & for i,l,m be Nat st i in ( dom ((a,b) Subnomial n)) & m = (i - 1) & l = (n - m) holds (f . i) = ((a |^ l) * (b |^ m)));

          

           A4: (( dom f) = ( dom ((a,b) Subnomial n)) & for i,l,m be Nat st i in ( dom ((a,b) Subnomial n)) & m = (i - 1) & l = (n - m) holds (f . i) = ((a |^ l) * (b |^ m))) by A3, FINSEQ_3: 29;

          for i be Nat st i in ( dom ((a,b) Subnomial n)) holds (f . i) = (((a,b) Subnomial n) . i)

          proof

            let i be Nat such that

             B2: i in ( dom ((a,b) Subnomial n));

            reconsider m = (i - 1) as Nat by B2, FINSEQ_3: 26;

            ( len ((a,b) Subnomial ((n + 1) - 1))) = (n + 1);

            then ((n + 1) - (m + 1)) is Element of NAT by FINSEQ_3: 26, B2;

            then

            reconsider l = (n - m) as Nat;

            (f . i) = ((a |^ l) * (b |^ m)) by A3, B2;

            hence thesis by LmS1, B2;

          end;

          hence thesis by A4, FINSEQ_1: 13;

        end;

        hence thesis by L1, L2, LmS1;

      end;

      coherence ;

    end

    registration

      let a,b be positive Real, k,l be Nat;

      cluster (((a,b) Subnomial (k + l)) . (k + 1)) -> positive;

      coherence

      proof

        (1 + 0 ) <= (1 + k) & ((k + 1) + 0 ) <= ((k + 1) + l) by XREAL_1: 6;

        then 1 <= (k + 1) <= ( len ((a,b) Subnomial (((k + l) + 1) - 1)));

        then k = ((k + 1) - 1) & l = ((k + l) - k) & (k + 1) in ( dom ((a,b) Subnomial (k + l))) by FINSEQ_3: 25;

        then (((a,b) Subnomial (k + l)) . (k + 1)) = ((a |^ l) * (b |^ k)) by Def2;

        hence thesis;

      end;

    end

    registration

      let a,b be positive Real, n be Nat;

      cluster ( Sum ((a,b) Subnomial n)) -> positive;

      coherence

      proof

        

         A1: for i be Nat st i in ( dom ((a,b) Subnomial n)) holds 0 <= (((a,b) Subnomial n) . i)

        proof

          let i be Nat such that

           B1: i in ( dom ((a,b) Subnomial n));

          

           B2: 1 <= i <= ( len ((a,b) Subnomial ((n + 1) - 1))) by B1, FINSEQ_3: 25;

          then

          reconsider s = ((n + 1) - i) as Element of NAT by NAT_1: 21;

          reconsider l = (i - 1) as Nat by B2;

          (((a,b) Subnomial (l + s)) . (l + 1)) > 0 ;

          hence thesis;

        end;

        ( len ((a,b) Subnomial ((n + 1) - 1))) >= 1 by NAT_1: 14;

        then 1 in ( dom ((a,b) Subnomial ((n + 1) - 1))) & 0 < (((a,b) Subnomial ( 0 + n)) . ( 0 + 1)) by FINSEQ_3: 25;

        hence thesis by A1, RVSUM_1: 85;

      end;

    end

    registration

      let k be Nat, n be non zero Nat;

      cluster ((( 0 , 0 ) In_Power n) . k) -> zero;

      coherence

      proof

        per cases ;

          suppose

           A1: k in ( dom (( 0 , 0 ) In_Power n));

          then

           A2: 1 <= k <= ( len (( 0 , 0 ) In_Power ((n + 1) - 1))) by FINSEQ_3: 25;

          then

          reconsider m = (k - 1) as Nat;

          ex l be Nat st (n + 1) = ((m + 1) + l) by A2, NAT_1: 10;

          then

          reconsider l = (n - m) as Nat;

          m = 0 implies l >= 1 by NAT_1: 14;

          then

           A3: m < 1 implies ( 0 |^ l) = 0 by NAT_1: 14, NEWTON: 11;

          

           A4: m >= 1 implies ( 0 |^ m) = 0 by NEWTON: 11;

          ((( 0 , 0 ) In_Power ((n + 1) - 1)) . k) = (((n choose m) * ( 0 |^ l)) * ( 0 |^ m)) by A1, NEWTON:def 4;

          hence thesis by A3, A4;

        end;

          suppose not k in ( dom (( 0 , 0 ) In_Power n));

          hence thesis by FUNCT_1:def 2;

        end;

      end;

      cluster ((( 0 , 0 ) Subnomial n) . k) -> zero;

      coherence

      proof

        ((( 0 , 0 ) Subnomial n) . k) = (((( 0 , 0 ) In_Power n) . k) / (( Newton_Coeff n) . k)) by VALUED_1: 17;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster (( 0 , 0 ) In_Power n) -> empty-yielding;

      coherence

      proof

        for x be set st x in ( rng (( 0 , 0 ) In_Power n)) holds x = {}

        proof

          let x be set;

          assume x in ( rng (( 0 , 0 ) In_Power n));

          then ex k be object st k in ( dom (( 0 , 0 ) In_Power n)) & ((( 0 , 0 ) In_Power n) . k) = x by FUNCT_1:def 3;

          hence thesis;

        end;

        hence thesis by RELAT_1: 149;

      end;

      cluster (( 0 , 0 ) Subnomial n) -> empty-yielding;

      coherence

      proof

        for x be set st x in ( rng (( 0 , 0 ) Subnomial n)) holds x = {}

        proof

          let x be set;

          assume x in ( rng (( 0 , 0 ) Subnomial n));

          then ex k be object st k in ( dom (( 0 , 0 ) Subnomial n)) & ((( 0 , 0 ) Subnomial n) . k) = x by FUNCT_1:def 3;

          hence thesis;

        end;

        hence thesis by RELAT_1: 149;

      end;

    end

    registration

      let f be empty-yielding FinSequence of COMPLEX ;

      cluster ( Sum f) -> zero;

      coherence

      proof

        f = (( len f) |-> 0 );

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      reduce (( Newton_Coeff n) . 1) to 1;

      correctness

      proof

        (( Newton_Coeff n) . 1) = (((1,1) In_Power n) . 1) by NEWTON: 31

        .= (1 |^ n) by NEWTON: 28;

        hence thesis;

      end;

      reduce (( Newton_Coeff n) . (n + 1)) to 1;

      reducibility

      proof

        (( Newton_Coeff n) . (n + 1)) = (((1,1) In_Power n) . (n + 1)) by NEWTON: 31

        .= (1 |^ n) by NEWTON: 29;

        hence thesis;

      end;

    end

    theorem :: NEWTON04:48

    

     NS: for a,b be Real, n be Nat holds ((((a,b) In_Power n) . 1) = (((a,b) Subnomial n) . 1)) & ((((a,b) In_Power n) . (n + 1)) = (((a,b) Subnomial n) . (n + 1)))

    proof

      let a,b be Real, n be Nat;

      

       A1: (((a,b) Subnomial n) . 1) = ((((a,b) In_Power n) . 1) / (( Newton_Coeff n) . 1)) by VALUED_1: 17;

      (((a,b) Subnomial n) . (n + 1)) = ((((a,b) In_Power n) . (n + 1)) / (( Newton_Coeff n) . (n + 1))) by VALUED_1: 17;

      hence thesis by A1;

    end;

    theorem :: NEWTON04:49

    

     RS: for a,b be Real holds ((a,b) Subnomial (n + 1)) = ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>)

    proof

      let a,b be Real;

      

       A0: ((a,b) Subnomial n) is FinSequence of COMPLEX by RVSUM_1: 146;

      

       A0a: ( len ((a,b) Subnomial n)) = ( len (a * ((a,b) Subnomial n))) by COMPLSP2: 3;

      

       A2: ( len ((a,b) Subnomial (((n + 1) + 1) - 1))) = ((n + 1) + 1) & ( len ((a,b) Subnomial ((n + 1) - 1))) = (n + 1);

      

      then

       A3: ( len ((a,b) Subnomial (n + 1))) = (( len ((a,b) Subnomial n)) + ( len <*(b |^ (n + 1))*>)) by FINSEQ_1: 39

      .= (( len (a * ((a,b) Subnomial n))) + ( len <*(b |^ (n + 1))*>)) by COMPLSP2: 3

      .= ( len ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>)) by FINSEQ_1: 22;

      for k be Nat st 1 <= k <= ( len ((a,b) Subnomial (n + 1))) holds (((a,b) Subnomial (n + 1)) . k) = (((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k)

      proof

        let k be Nat such that

         B0: 1 <= k <= ( len ((a,b) Subnomial (n + 1)));

        reconsider m = (k - 1) as Nat by B0;

        per cases ;

          suppose

           C1: k in ( dom ((a,b) Subnomial n));

          then

           C2: 1 <= k <= ( len ((a,b) Subnomial n)) by FINSEQ_3: 25;

          then (m + 1) <= (n + 1) by Def2;

          then

          reconsider l = (n - m) as Element of NAT by XREAL_1: 6, NAT_1: 21;

          

           C3: (l + 1) = ((n + 1) - m);

          k in ( dom ((a,b) Subnomial (n + 1))) by B0, FINSEQ_3: 25;

          

          then (((a,b) Subnomial (n + 1)) . k) = ((a |^ (l + 1)) * (b |^ m)) by Def2, C3

          .= ((a * (a |^ l)) * (b |^ m)) by NEWTON: 6

          .= (a * ((a |^ l) * (b |^ m)))

          .= (a * (((a,b) Subnomial n) . k)) by C1, Def2

          .= ((a * ((a,b) Subnomial n)) . k) by A0, COMPLSP2: 16

          .= (((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . k) by A0a, C2, FINSEQ_1: 64;

          hence thesis;

        end;

          suppose not k in ( dom ((a,b) Subnomial n));

          then not k <= (n + 1) by B0, A2, FINSEQ_3: 25;

          then k >= ((n + 1) + 1) by INT_1: 7;

          then

           C1: k = ((n + 1) + 1) by B0, A2, XXREAL_0: 1;

          ( len (a * ((a,b) Subnomial n))) = (n + 1) by A2, NEWTON: 2;

          then (((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) . ((n + 1) + 1)) = (((a,b) In_Power (n + 1)) . ((n + 1) + 1)) by NEWTON: 29;

          hence thesis by NS, C1;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: NEWTON04:50

    

     LS: for a,b be Real holds ((a,b) Subnomial (n + 1)) = ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))

    proof

      let a,b be Real;

      

       A2: ( len ((a,b) Subnomial (((n + 1) + 1) - 1))) = ((n + 1) + 1) & ( len ((a,b) Subnomial ((n + 1) - 1))) = (n + 1);

      

      then

       A3: ( len ((a,b) Subnomial (n + 1))) = (( len <*(a |^ (n + 1))*>) + ( len ((a,b) Subnomial n))) by FINSEQ_1: 39

      .= (( len <*(a |^ (n + 1))*>) + ( len (b * ((a,b) Subnomial n)))) by NEWTON: 2

      .= ( len ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))) by FINSEQ_1: 22;

      for k be Nat st 1 <= k <= ( len ((a,b) Subnomial (n + 1))) holds (((a,b) Subnomial (n + 1)) . k) = (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . k)

      proof

        let k be Nat such that

         B0: 1 <= k <= ( len ((a,b) Subnomial (n + 1)));

        per cases by B0, XXREAL_0: 1;

          suppose k > 1;

          then k >= (1 + 1) by NAT_1: 13;

          then

          reconsider m = (k - 2) as Element of NAT by NAT_1: 21;

          

           C2: (n + 2) >= (m + 2) by A2, B0;

          then

          reconsider l = (n - m) as Element of NAT by XREAL_1: 6, NAT_1: 21;

          

           C3: l = ((n + 1) - (m + 1));

          m <= n by C2, XREAL_1: 6;

          then

           C3a: ( 0 + 1) <= (m + 1) <= (n + 1) by XREAL_1: 6;

          then

           C4: (m + 1) in ( dom ((a,b) Subnomial n)) by A2, FINSEQ_3: 25;

          

           C5: m = ((m + 1) - 1) & l = (n - m);

          

           C6: 1 <= (m + 1) <= ( len (b * ((a,b) Subnomial n))) by C3a, A2, NEWTON: 2;

          (m + 1) = (k - 1) & k in ( dom ((a,b) Subnomial (n + 1))) by B0, FINSEQ_3: 25;

          

          then (((a,b) Subnomial (n + 1)) . k) = ((a |^ l) * (b |^ (m + 1))) by Def2, C3

          .= ((a |^ l) * (b * (b |^ m))) by NEWTON: 6

          .= (b * ((a |^ l) * (b |^ m)))

          .= (b * (((a,b) Subnomial n) . (m + 1))) by C4, C5, Def2

          .= ((b * ((a,b) Subnomial n)) . (m + 1)) by RVSUM_1: 45

          .= (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . (( len <*(a |^ (n + 1))*>) + (m + 1))) by C6, FINSEQ_1: 65

          .= (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . ((m + 1) + 1)) by FINSEQ_1: 39;

          hence thesis;

        end;

          suppose

           C1: k = 1;

          (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . 1) = (((a,b) In_Power (n + 1)) . 1) by NEWTON: 28;

          hence thesis by NS, C1;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: NEWTON04:51

    

     SumS: for a,b be Real, n be Nat holds ((a |^ (n + 1)) - (b |^ (n + 1))) = ((a - b) * ( Sum ((a,b) Subnomial n)))

    proof

      let a,b be Real, n be Nat;

      

       A1: ( Sum ((a,b) Subnomial (n + 1))) = ( Sum ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>)) by RS

      .= (( Sum (a * ((a,b) Subnomial n))) + (b |^ (n + 1))) by RVSUM_2: 31

      .= ((a * ( Sum ((a,b) Subnomial n))) + (b |^ (n + 1))) by RVSUM_2: 38;

      ( Sum ((a,b) Subnomial (n + 1))) = ( Sum ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))) by LS

      .= ((a |^ (n + 1)) + ( Sum (b * ((a,b) Subnomial n)))) by RVSUM_2: 33

      .= ((b * ( Sum ((a,b) Subnomial n))) + (a |^ (n + 1))) by RVSUM_2: 38;

      hence thesis by A1;

    end;

    theorem :: NEWTON04:52

    for a be Real, n be non zero Nat holds (a |^ n) = ( Sum ((a, 0 ) Subnomial n))

    proof

      let a be Real, n be non zero Nat;

      per cases ;

        suppose

         A1: a is zero;

        then for i be Element of NAT st i in ( dom ((a, 0 ) Subnomial n)) holds (((a, 0 ) Subnomial n) . i) = 0 ;

        hence thesis by A1, PRVECT_2: 3;

      end;

        suppose

         A2: a is non zero;

        ((a |^ (n + 1)) - ( 0 |^ (n + 1))) = ((a - 0 ) * ( Sum ((a, 0 ) Subnomial n))) by SumS;

        then (a * (a |^ n)) = (a * ( Sum ((a, 0 ) Subnomial n))) by NEWTON: 6;

        hence thesis by A2, XCMPLX_1: 5;

      end;

    end;

    theorem :: NEWTON04:53

    for a be Real, n be Nat holds (a |^ (n + 1)) = ((( Sum ((a,1) Subnomial n)) * (a - 1)) + 1)

    proof

      let a be Real, n be Nat;

      ((a |^ (n + 1)) - (1 |^ (n + 1))) = ((a - 1) * ( Sum ((a,1) Subnomial n))) by SumS;

      hence thesis;

    end;

    theorem :: NEWTON04:54

    

     STT: for a,b,c,d be Real, n be Nat, x be object st x in ( dom (((a * b),(c * d)) Subnomial n)) holds ((((a * b),(c * d)) Subnomial n) . x) = ((((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x))

    proof

      let a,b,c,d be Real, n be Nat, x be object such that

       B1: x in ( dom (((a * b),(c * d)) Subnomial n));

      ( len (((a * b),(c * d)) Subnomial ((n + 1) - 1))) = ( len ((a,d) Subnomial ((n + 1) - 1))) & ( len (((a * b),(c * d)) Subnomial ((n + 1) - 1))) = ( len ((b,c) Subnomial ((n + 1) - 1)));

      then

       A0: ( dom (((a * b),(c * d)) Subnomial n)) = ( dom ((a,d) Subnomial n)) & ( dom (((a * b),(c * d)) Subnomial n)) = ( dom ((b,c) Subnomial n)) by FINSEQ_3: 29;

      reconsider x as positive Nat by B1, FINSEQ_3: 25;

      set m = (x - 1);

      ( len (((a * b),(c * d)) Subnomial ((n + 1) - 1))) >= x by B1, FINSEQ_3: 25;

      then

      consider k be Nat such that

       B2: (n + 1) = (x + k) by NAT_1: 10;

      

       B3: n = (m + k) & k = (n - m) by B2;

      

      then ((((a * b),(c * d)) Subnomial (m + k)) . (m + 1)) = (((a * b) |^ k) * ((c * d) |^ m)) by B1, Def2

      .= (((a |^ k) * (b |^ k)) * ((c * d) |^ m)) by NEWTON: 7

      .= (((a |^ k) * (b |^ k)) * ((c |^ m) * (d |^ m))) by NEWTON: 7

      .= (((a |^ k) * (d |^ m)) * ((b |^ k) * (c |^ m)))

      .= ((((a,d) Subnomial (m + k)) . (m + 1)) * ((b |^ k) * (c |^ m))) by A0, B1, B3, Def2

      .= ((((a,d) Subnomial (m + k)) . (m + 1)) * (((b,c) Subnomial (m + k)) . (m + 1))) by A0, B1, B3, Def2;

      hence thesis by B2;

    end;

    theorem :: NEWTON04:55

    

     ST: for a,b,c,d be Real, n be Nat holds (((a * b),(c * d)) Subnomial n) = (((a,d) Subnomial n) (#) ((b,c) Subnomial n))

    proof

      let a,b,c,d be Real, n be Nat;

      ( len (((a * b),(c * d)) Subnomial ((n + 1) - 1))) = ( len ((a,d) Subnomial ((n + 1) - 1))) & ( len (((a * b),(c * d)) Subnomial ((n + 1) - 1))) = ( len ((b,c) Subnomial ((n + 1) - 1)));

      then ( dom (((a * b),(c * d)) Subnomial n)) = ( dom ((a,d) Subnomial n)) & ( dom (((a * b),(c * d)) Subnomial n)) = ( dom ((b,c) Subnomial n)) by FINSEQ_3: 29;

      then

       A1: ( dom (((a * b),(c * d)) Subnomial n)) = (( dom ((a,d) Subnomial n)) /\ ( dom ((b,c) Subnomial n)));

      for x be object st x in ( dom (((a * b),(c * d)) Subnomial n)) holds ((((a * b),(c * d)) Subnomial n) . x) = ((((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)) by STT;

      hence thesis by A1, VALUED_1:def 4;

    end;

    theorem :: NEWTON04:56

    

     DAB: for a,b be Real, n be Nat holds ((a,b) Subnomial n) = (((a,1) Subnomial n) (#) ((1,b) Subnomial n))

    proof

      let a,b be Real, n be Nat;

      (((a * 1),(b * 1)) Subnomial n) = (((a,1) Subnomial n) (#) ((1,b) Subnomial n)) by ST;

      hence thesis;

    end;

    theorem :: NEWTON04:57

    

     INS: for a,b be Real, n be Nat holds ((a,b) In_Power n) = (( Newton_Coeff n) (#) ((a,b) Subnomial n))

    proof

      let a,b be Real, n be Nat;

      

       A0a: ( dom ((a,b) In_Power n)) = ( dom ( Newton_Coeff n)) by DOMN;

      then

       A0: ( dom ((a,b) In_Power n)) = (( dom ( Newton_Coeff n)) /\ ( dom ((a,b) In_Power n)));

      then

       A1: ( dom ((a,b) In_Power n)) = ( dom ((a,b) Subnomial n)) by VALUED_1: 16;

      for c be object st c in ( dom ((a,b) In_Power n)) holds (((a,b) In_Power n) . c) = ((( Newton_Coeff n) . c) * (((a,b) Subnomial n) . c))

      proof

        let c be object such that

         B1: c in ( dom ((a,b) In_Power n));

        reconsider c as positive Nat by B1, FINSEQ_3: 25;

        set m = (c - 1);

        c <= ( len ( Newton_Coeff ((n + 1) - 1))) by B1, A0a, FINSEQ_3: 25;

        then

        consider k be Nat such that

         B2: (n + 1) = (c + k) by NAT_1: 10;

        

         B3: n = (m + k) & k = (n - m) by B2;

        ((( Newton_Coeff (m + k)) . (m + 1)) * (((a,b) Subnomial (m + k)) . (m + 1))) = (((m + k) choose m) * (((a,b) Subnomial (m + k)) . (m + 1))) by B2, B1, A0a, NEWTON:def 5

        .= (((m + k) choose m) * ((a |^ k) * (b |^ m))) by B1, A1, B3, Def2

        .= ((((m + k) choose m) * (a |^ k)) * (b |^ m))

        .= (((a,b) In_Power (m + k)) . (m + 1)) by NEWTON:def 4, B1, B3;

        hence thesis by B2;

      end;

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

    end;

    theorem :: NEWTON04:58

    for a,b be Real, n be Nat holds ((a,b) In_Power n) = (((a,1) In_Power n) (#) ((1,b) Subnomial n)) & ((a,b) In_Power n) = (((a,1) Subnomial n) (#) ((1,b) In_Power n))

    proof

      let a,b be Real, n be Nat;

      

       A1: ((a,b) In_Power n) = (( Newton_Coeff n) (#) ((a,b) Subnomial n)) by INS

      .= (( Newton_Coeff n) (#) (((a,1) Subnomial n) (#) ((1,b) Subnomial n))) by DAB;

      (( Newton_Coeff n) (#) ((a,1) Subnomial n)) = ((a,1) In_Power n) & (( Newton_Coeff n) (#) ((1,b) Subnomial n)) = ((1,b) In_Power n) by INS;

      hence thesis by A1, F123;

    end;

    theorem :: NEWTON04:59

    for a,b,c,d be Real, n be Nat holds (((a * b),(c * d)) In_Power n) = ((( Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n))

    proof

      let a,b,c,d be Real, n be Nat;

      (((a * b),(c * d)) In_Power n) = (( Newton_Coeff n) (#) (((a * b),(c * d)) Subnomial n)) by INS

      .= (( Newton_Coeff n) (#) (((a,c) Subnomial n) (#) ((b,d) Subnomial n))) by ST;

      hence thesis by RFUNCT_1: 9;

    end;

    theorem :: NEWTON04:60

    

     CONST: for a be Real, n,i be Nat st i in ( dom ((a,a) Subnomial n)) holds (((a,a) Subnomial n) . i) = (a |^ n)

    proof

      let a be Real, n,i be Nat such that

       A1: i in ( dom ((a,a) Subnomial n));

      

       A2: 1 <= i <= ( len ((a,a) Subnomial ((n + 1) - 1))) by A1, FINSEQ_3: 25;

      then

      reconsider k = (i - 1) as Nat;

      (n + 1) >= (k + 1) by A2;

      then

      reconsider l = (n - k) as Element of NAT by XREAL_1: 6, NAT_1: 21;

      ((a |^ k) * (a |^ l)) = (a |^ (k + l)) by NEWTON: 8;

      hence thesis by A1, Def2;

    end;

    theorem :: NEWTON04:61

    

     CONST1: for n be Nat, a be Real holds ((a,a) Subnomial n) = ((n + 1) |-> (a |^ n))

    proof

      let n be Nat, a be Real;

      

       A1: for j be Nat holds (((a,a) Subnomial n) . j) = (((n + 1) |-> (a |^ n)) . j)

      proof

        let j be Nat;

        j <> 0 implies (((a,a) Subnomial n) . j) = (((n + 1) |-> (a |^ n)) . j)

        proof

          assume j <> 0 ;

          then

          reconsider i = (j - 1) as Nat;

          per cases ;

            suppose ex k be Nat st n = (i + k);

            then

            reconsider k = (n - i) as Nat;

            set l = (i + 1);

            ( 0 + 1) <= (i + 1) & ((i + 1) + 0 ) <= ((i + 1) + k) by XREAL_1: 6;

            then 1 <= (i + 1) <= ( len ((a,a) Subnomial ((n + 1) - 1)));

            then (i + 1) in ( dom ((a,a) Subnomial (i + k))) by FINSEQ_3: 25;

            then (((a,a) Subnomial (i + k)) . (i + 1)) = (a |^ n) & (((k + (i + 1)) |-> (a |^ n)) . (i + 1)) = (a |^ n) by CONST;

            hence thesis;

          end;

            suppose not ex k be Nat st n = (i + k);

            then (i + 1) > (n + 1) by XREAL_1: 6, NAT_1: 10;

            then (i + 1) > ( len ((a,a) Subnomial n)) & (i + 1) > ( len ((n + 1) |-> (a |^ n))) = (n + 1) by Def2;

            then not (i + 1) in ( dom ((a,a) Subnomial n)) & not (i + 1) in ( dom ((n + 1) |-> (a |^ n))) by FINSEQ_3: 25;

            then (((a,a) Subnomial n) . (i + 1)) = 0 & (((n + 1) |-> (a |^ n)) . (i + 1)) = 0 by FUNCT_1:def 2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      ( len ((a,a) Subnomial ((n + 1) - 1))) = ( len ((n + 1) |-> (a |^ n)));

      hence thesis by A1;

    end;

    theorem :: NEWTON04:62

    

     PRA: for n be Nat, a be Real holds ( Product ((a,a) Subnomial n)) = (a |^ (n * (n + 1)))

    proof

      let n be Nat, a be Real;

      set f = ((n + 1) |-> (a |^ n)), h = ( the_value_of f), i = ( len f);

      ( Product ((a,a) Subnomial n)) = ( Product f) by CONST1

      .= (h |^ i) by RVSUM_3: 8

      .= (a |^ (n * (n + 1))) by NEWTON: 9;

      hence thesis;

    end;

    theorem :: NEWTON04:63

    

     PRN: for n be Nat, f,g be n -element complex-valued FinSequence holds ( Product (f (#) g)) = (( Product f) * ( Product g))

    proof

      let n be Nat, f,g be n -element complex-valued FinSequence;

      reconsider f as FinSequence of COMPLEX by RVSUM_1: 146;

      reconsider g as FinSequence of COMPLEX by RVSUM_1: 146;

      ( Product (f (#) g)) = (( Product f) * ( Product g)) by RVSUM_2: 48;

      hence thesis;

    end;

    theorem :: NEWTON04:64

    

     SAB: for a,b be Real, n be Nat holds ((a,b) Subnomial n) = ( Rev ((b,a) Subnomial n))

    proof

      let a,b be Real, n be Nat;

      

       A1: ( dom ((a,b) Subnomial n)) = ( dom ( Newton_Coeff n)) & ( dom ((b,a) Subnomial n)) = ( dom ( Newton_Coeff n)) by DOMN;

      then

       A2: ( dom ((a,b) Subnomial n)) = ( dom ( Rev ((b,a) Subnomial n))) by FINSEQ_5: 57;

      for i be object st i in ( dom ((a,b) Subnomial n)) holds (((a,b) Subnomial n) . i) = (( Rev ((b,a) Subnomial n)) . i)

      proof

        let i be object such that

         B1: i in ( dom ((a,b) Subnomial n));

        reconsider i as Nat by B1;

        reconsider m = (i - 1) as Nat by B1, FINSEQ_3: 26;

        (( len ((a,b) Subnomial ((n + 1) - 1))) - (m + 1)) is Element of NAT by B1, FINSEQ_3: 26;

        then

        reconsider l = (n - m) as Nat;

        set k = (l + 1);

        

         B2: i in ( dom ( Rev ((b,a) Subnomial ((n + 1) - 1)))) by A1, FINSEQ_5: 57, B1;

        (k + i) = (( len ((b,a) Subnomial ((n + 1) - 1))) + 1)

        .= (( len ( Rev ((b,a) Subnomial ((n + 1) - 1)))) + 1) by FINSEQ_5:def 3;

        then

         B3: k in ( dom ( Rev ( Rev ((b,a) Subnomial ((n + 1) - 1))))) by B2, FINSEQ_5: 59;

        

         B4: l = (k - 1);

        

         B5: m = (n - l);

        (((a,b) Subnomial n) . i) = ((a |^ l) * (b |^ m)) by B1, Def2

        .= (((b,a) Subnomial n) . ((( len ((b,a) Subnomial ((n + 1) - 1))) - i) + 1)) by B3, B4, B5, Def2

        .= (( Rev ((b,a) Subnomial n)) . i) by FINSEQ_5: 58, A1, B1;

        hence thesis;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    registration

      let n be Nat, i be Nat;

      reduce (((1,1) Subnomial (n + i)) . (i + 1)) to 1;

      reducibility

      proof

        

         A1: (1 + 0 ) <= (1 + i) & ((i + 1) + 0 ) <= ((i + 1) + n) by XREAL_1: 6;

        ( len ((1,1) Subnomial (((n + i) + 1) - 1))) = ((n + i) + 1);

        then (i + 1) in ( dom ((1,1) Subnomial (n + i))) by A1, FINSEQ_3: 25;

        then (((1,1) Subnomial (n + i)) . (i + 1)) = (1 |^ (n + i)) by CONST;

        hence thesis;

      end;

    end

    registration

      let n be Nat, i be non zero Nat;

      reduce (((1,( - 1)) Subnomial ((2 * i) + n)) . (2 * i)) to ( - 1);

      reducibility

      proof

        

         A1: ( len ((1,( - 1)) Subnomial ((((2 * i) + n) + 1) - 1))) = (((2 * i) + n) + 1);

        (i + i) >= (1 + 0 ) & ((2 * i) + (n + 1)) >= ((2 * i) + 0 ) by XREAL_1: 6, NAT_1: 14;

        then

         A2: (2 * i) in ( dom ((1,( - 1)) Subnomial ((2 * i) + n))) by A1, FINSEQ_3: 25;

        reconsider k = ((2 * i) - 1) as odd Nat;

        (n + 1) = (((2 * i) + n) - k);

        

        then (((1,( - 1)) Subnomial (n + (2 * i))) . (2 * i)) = ((1 |^ (n + 1)) * (( - 1) |^ k)) by A2, Def2

        .= (1 * ( - 1));

        hence thesis;

      end;

    end

    registration

      let n be Nat, i be odd Nat;

      reduce (((1,( - 1)) Subnomial (n + i)) . i) to 1;

      reducibility

      proof

        

         A1: ( len ((1,( - 1)) Subnomial (((n + i) + 1) - 1))) = ((n + i) + 1);

        i >= 1 & (i + (n + 1)) >= (i + 0 ) by XREAL_1: 6, NAT_1: 14;

        then

         A2: i in ( dom ((1,( - 1)) Subnomial (i + n))) by A1, FINSEQ_3: 25;

        reconsider k = (i - 1) as even Nat;

        (n + 1) = ((i + n) - k);

        

        then (((1,( - 1)) Subnomial (n + i)) . i) = ((1 |^ (n + 1)) * (( - 1) |^ k)) by A2, Def2

        .= (1 * 1);

        hence thesis;

      end;

    end

    registration

      let a be Real, n be Nat;

      cluster (n |-> a) -> constant;

      coherence

      proof

        for i,j be object st i in ( dom (n |-> a)) & j in ( dom (n |-> a)) holds ((n |-> a) . i) = ((n |-> a) . j)

        proof

          let i,j be object such that

           A1: i in ( dom (n |-> a)) & j in ( dom (n |-> a));

          reconsider i as Nat by A1;

          reconsider j as Nat by A1;

          ( dom (n |-> a)) = ( Seg ( len (n |-> a))) by FINSEQ_1:def 3;

          then ((n |-> a) . i) = a & ((n |-> a) . j) = a by A1, FINSEQ_2: 57;

          hence thesis;

        end;

        hence thesis by FUNCT_1:def 10;

      end;

      cluster ((a,a) Subnomial n) -> constant;

      coherence

      proof

        ((a,a) Subnomial n) = ((n + 1) |-> (a |^ n)) by CONST1;

        hence thesis;

      end;

    end

    registration

      let a,b be non negative Real;

      let n,k be Nat;

      cluster (((a,b) In_Power n) . k) -> non negative;

      coherence

      proof

        per cases ;

          suppose

           A1: k in ( dom ((a,b) In_Power n));

          then k >= 1 by FINSEQ_3: 25;

          then

          reconsider l = (k - 1) as Nat;

          ( len ((a,b) In_Power n)) >= (l + 1) by FINSEQ_3: 25, A1;

          then (n + 1) >= (l + 1) by NEWTON:def 4;

          then

          reconsider m = (n - l) as Element of NAT by XREAL_1: 6, NAT_1: 21;

          (((a,b) In_Power n) . k) = (((n choose l) * (a |^ m)) * (b |^ l)) by A1, NEWTON:def 4;

          hence thesis;

        end;

          suppose not k in ( dom ((a,b) In_Power n));

          hence thesis by FUNCT_1:def 2;

        end;

      end;

      cluster (((a,b) Subnomial n) . k) -> non negative;

      coherence

      proof

        (((a,b) Subnomial n) . k) = ((((a,b) In_Power n) . k) / (( Newton_Coeff n) . k)) by VALUED_1: 17;

        hence thesis;

      end;

    end

    theorem :: NEWTON04:65

    

     SAA: for a be Real, n be Nat holds ( Sum ((a,a) Subnomial n)) = ((n + 1) * (a |^ n))

    proof

      let a be Real, n be Nat;

      

       A1: (n + 1) = ( len ((a,a) Subnomial ((n + 1) - 1)));

      (n + 1) >= ( 0 + 1) by XREAL_1: 6;

      then

       A2: (n + 1) in ( dom ((a,a) Subnomial n)) by A1, FINSEQ_3: 25;

      (n + 1) is set & (n + 1) in ( dom ((a,a) Subnomial n)) & (((a,a) Subnomial n) . (n + 1)) = (a |^ n) by A2, CONST;

      then ( the_value_of ((a,a) Subnomial n)) = (a |^ n) by FUNCT_1:def 12;

      hence thesis by A1, RVSUM_3: 7;

    end;

    theorem :: NEWTON04:66

    

     ES: for a be Real, n be even Nat holds ( Sum ((a,( - a)) Subnomial n)) = (a |^ n)

    proof

      let a be Real, n be even Nat;

      per cases ;

        suppose

         A1: a is zero;

        per cases ;

          suppose

           B1: n = 0 ;

          ( Sum ((a,( - a)) Subnomial n)) = (( 0 + 1) * (a |^ n)) by A1, B1, SAA;

          hence thesis;

        end;

          suppose

           B1: n > 0 ;

          ((a,( - a)) Subnomial n) = (( len (( 0 , 0 ) Subnomial ((n + 1) - 1))) |-> 0 ) by B1, A1;

          hence thesis by A1, B1, NAT_1: 14, NEWTON: 11;

        end;

      end;

        suppose

         A1: not a is zero;

        ((a - ( - a)) * ( Sum ((a,( - a)) Subnomial n))) = ((a |^ (n + 1)) - ((( - 1) * a) |^ (n + 1))) by SumS

        .= ((a |^ (n + 1)) - ((( - 1) |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON: 7

        .= (2 * (a |^ (n + 1)))

        .= (2 * (a * (a |^ n))) by NEWTON: 6

        .= ((2 * a) * (a |^ n));

        hence thesis by A1, XCMPLX_1: 5;

      end;

    end;

    registration

      let n be even Nat;

      reduce ( Sum ((1,( - 1)) Subnomial n)) to 1;

      reducibility

      proof

        ( Sum ((1,( - 1)) Subnomial n)) = (1 |^ n) by ES;

        hence thesis;

      end;

    end

    registration

      let a be Real, n be odd Nat;

      cluster ( Sum ((a,( - a)) Subnomial n)) -> zero;

      coherence

      proof

        per cases ;

          suppose a is zero;

          then ((a,( - a)) Subnomial n) = (( len (( 0 , 0 ) Subnomial ((n + 1) - 1))) |-> 0 );

          hence thesis;

        end;

          suppose not a is zero;

          then

           A1: (2 * a) <> 0 ;

          ((a - ( - a)) * ( Sum ((a,( - a)) Subnomial n))) = ((a |^ (n + 1)) - ((( - 1) * a) |^ (n + 1))) by SumS

          .= ((a |^ (n + 1)) - ((( - 1) |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON: 7

          .= ((a |^ (n + 1)) - (1 * (a |^ (n + 1))));

          hence thesis by A1;

        end;

      end;

    end

    registration

      let n be Nat;

      reduce ( Sum ((1,1) Subnomial ((n + 1) - 1))) to (n + 1);

      reducibility

      proof

        ( Sum ((1,1) Subnomial n)) = ((n + 1) * (1 |^ n)) by SAA;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( Sum ( Newton_Coeff n)) -> non zero;

      coherence

      proof

        set f = ( Newton_Coeff n);

         0 in REAL by XREAL_0:def 1;

        then

        reconsider g = (n |-> 0 ) as FinSequence of REAL by FINSEQ_2: 63;

        

         A1: for x be Nat holds (f . x) >= ((n |-> 0 ) . x);

        (f . ( 0 + 1)) > (g . ( 0 + 1));

        then ( Sum f) > ( Sum (n |-> 0 )) by A1, NYS1;

        hence thesis;

      end;

    end

    registration

      let a,b be non negative Real, n be Nat;

      cluster ((a,b) Subnomial n) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng ((a,b) Subnomial n)) holds r >= 0

        proof

          let r be Real such that

           B1: r in ( rng ((a,b) Subnomial n));

          ex k be object st k in ( dom ((a,b) Subnomial n)) & r = (((a,b) Subnomial n) . k) by B1, FUNCT_1:def 3;

          hence thesis;

        end;

        hence thesis by PARTFUN3:def 4;

      end;

      cluster ((a,b) In_Power n) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng ((a,b) In_Power n)) holds r >= 0

        proof

          let r be Real such that

           B1: r in ( rng ((a,b) In_Power n));

          ex k be object st k in ( dom ((a,b) In_Power n)) & r = (((a,b) In_Power n) . k) by B1, FUNCT_1:def 3;

          hence thesis;

        end;

        hence thesis by PARTFUN3:def 4;

      end;

      cluster ( Sum ((a,b) Subnomial n)) -> non negative;

      coherence ;

      cluster ( Sum ((a,b) In_Power n)) -> non negative;

      coherence ;

    end

    theorem :: NEWTON04:67

    

     SFE: for a,b be Real holds (((a,b) Subnomial n),((b,a) Subnomial n)) are_fiberwise_equipotent

    proof

      let a,b be Real;

      (((a,b) Subnomial n),( Rev ((a,b) Subnomial n))) are_fiberwise_equipotent by FFE;

      hence thesis by SAB;

    end;

    theorem :: NEWTON04:68

    for a,b be Real holds ( Product ((a,b) Subnomial n)) = ( Product ((b,a) Subnomial n)) by SFE, RVSUM_3: 4;

    theorem :: NEWTON04:69

    for a be non negative Real holds ( Product ((a,1) Subnomial n)) = (a |^ ((n + 1) choose 2))

    proof

      let a be non negative Real;

      set l = (a |^ (n choose 2)), f = ((a,1) Subnomial n), g = ((1,a) Subnomial n);

      

       A1: (((n + 1) choose 2) * 2) = (((n * (n + 1)) / 2) * 2) by NUMPOLY1: 72

      .= (n * (n + 1));

      

       A2: ((a |^ ((n + 1) choose 2)) |^ 2) = (a |^ (((n + 1) choose 2) * 2)) by NEWTON: 9

      .= ( Product (((a * 1),(a * 1)) Subnomial n)) by A1, PRA

      .= ( Product (f (#) g)) by ST

      .= (( Product f) * ( Product g)) by PRN

      .= (( Product f) * ( Product f)) by SFE, RVSUM_3: 4

      .= (( Product f) |^ 2) by NEWTON: 81;

      (a |^ ((n + 1) choose 2)) = ( sqrt (( Product f) |^ 2)) by A2

      .= ( Product f);

      hence thesis;

    end;

    theorem :: NEWTON04:70

    

     ES: ((n ! ) * (k ! )) <= ((n + k) ! )

    proof

      set s = ((n + k) choose n), l = (n + k);

      k = (l - n) & (n + k) >= (n + 0 ) by XREAL_1: 6;

      

      then

       A2: (s * ((n ! ) * (k ! ))) = ((((n + k) ! ) / ((n ! ) * (k ! ))) * ((n ! ) * (k ! ))) by NEWTON:def 3

      .= ((n + k) ! ) by XCMPLX_1: 87;

      (s * ((n ! ) * (k ! ))) >= (1 * ((n ! ) * (k ! ))) by XREAL_1: 64, NAT_1: 14;

      hence thesis by A2;

    end;

    theorem :: NEWTON04:71

    

     NCK: ((n + k) choose k) = 1 iff n = 0 or k = 0

    proof

      

       A1: n <> 0 & k <> 0 implies ((n + k) choose k) <> 1

      proof

        assume n <> 0 & k <> 0 ;

        then

        reconsider m = (n - 1), l = (k - 1) as Nat;

        ((m + k) choose k) >= 1 & ((n + l) choose l) >= 1 by NAT_1: 14;

        then

         B2: (((k + m) choose k) + ((l + n) choose l)) >= (1 + 1) by XREAL_1: 7;

        (((m + k) + 1) choose (l + 1)) = (((m + k) choose k) + ((n + l) choose l)) by NEWTON: 22;

        hence thesis by B2;

      end;

      n = 0 or k = 0 implies ((n + k) choose (k * 1)) = 1;

      hence thesis by A1;

    end;

    theorem :: NEWTON04:72

    

     EZ: ((n ! ) * (k ! )) = ((n + k) ! ) iff (n = 0 or k = 0 )

    proof

      n = ((n + k) - k) & (n + k) >= ( 0 + k) by XREAL_1: 6;

      

      then (((n + k) choose (k * 1)) * ((n ! ) * (k ! ))) = ((((n + k) ! ) / ((n ! ) * (k ! ))) * ((n ! ) * (k ! ))) by NEWTON:def 3

      .= ((n + k) ! ) by XCMPLX_1: 87;

      hence thesis by NCK, XCMPLX_1: 7;

    end;

    registration

      let n,k be non zero Nat;

      cluster (((n + k) ! ) - ((n ! ) * (k ! ))) -> positive;

      coherence

      proof

        ((n ! ) * (k ! )) <= ((n + k) ! ) by ES;

        then ((n ! ) * (k ! )) < ((n + k) ! ) by EZ, XXREAL_0: 1;

        then (((n ! ) * (k ! )) - ((n ! ) * (k ! ))) < (((n + k) ! ) - ((n ! ) * (k ! ))) by XREAL_1: 9;

        then (((n + k) ! ) - ((n ! ) * (k ! ))) > 0 ;

        hence thesis;

      end;

    end

    theorem :: NEWTON04:73

    for a be Real holds ( Sum ((a,a) Subnomial n)) = (( Sum ((1,1) Subnomial n)) * ( Sum ((a, 0 ) In_Power n)))

    proof

      let a be Real;

      (( Sum ((1,1) Subnomial n)) * ( Sum ((a, 0 ) In_Power ((n + 1) - 1)))) = ((n + 1) * ((a + 0 ) |^ n)) by NEWTON: 30;

      hence thesis by SAA;

    end;

    theorem :: NEWTON04:74

    for a,b,c be Real holds ( Sum (((a + b),c) In_Power n)) = ( Sum ((a,(b + c)) In_Power n))

    proof

      let a,b,c be Real;

      ( Sum (((a + b),c) In_Power n)) = (((a + b) + c) |^ n) by NEWTON: 30

      .= ((a + (b + c)) |^ n)

      .= ( Sum ((a,(b + c)) In_Power n)) by NEWTON: 30;

      hence thesis;

    end;

    theorem :: NEWTON04:75

    

     NCI: (( Newton_Coeff n) . (i + 1)) = (n choose i)

    proof

      per cases ;

        suppose

         B1: (i + 1) in ( dom ( Newton_Coeff n));

        then 1 <= (i + 1) <= ( len ( Newton_Coeff n)) by FINSEQ_3: 25;

        then 1 <= (i + 1) <= (n + 1) by NEWTON:def 5;

        then

        reconsider k = ((n + 1) - (i + 1)) as Element of NAT by NAT_1: 21;

        n = (i + k) & i = ((i + 1) - 1);

        hence thesis by B1, NEWTON:def 5;

      end;

        suppose

         B1: not (i + 1) in ( dom ( Newton_Coeff n));

        then not 1 <= (i + 1) <= ( len ( Newton_Coeff n)) by FINSEQ_3: 25;

        then not ( 0 + 1) <= (i + 1) <= (n + 1) by NEWTON:def 5;

        then not 0 <= i <= n by XREAL_1: 6;

        then (n choose i) = 0 by NEWTON:def 3;

        hence thesis by B1, FUNCT_1:def 2;

      end;

    end;

    theorem :: NEWTON04:76

    ((2 * n) choose n) = (((2 * n) ! ) / ((n ! ) |^ 2))

    proof

      

       A1: n = ((2 * n) - n);

      (n + n) >= (n + 0 ) by XREAL_1: 6;

      then ((2 * n) choose n) = (((2 * n) ! ) / ((n ! ) * (n ! ))) by A1, NEWTON:def 3;

      hence thesis by NEWTON: 81;

    end;

    theorem :: NEWTON04:77

    (( Newton_Coeff ((2 * n) + 1)) . (n + 1)) = (( Newton_Coeff ((2 * n) + 1)) . (n + 2))

    proof

      reconsider k = ((2 * n) + 1) as Nat;

      

       A0: ((n + 1) + n) >= ((n + 1) + 0 ) & (n + (n + 1)) >= (n + 0 ) by XREAL_1: 6;

      

       A2: ( len ( Newton_Coeff ((2 * n) + 1))) = (((2 * n) + 1) + 1) by NEWTON:def 5;

      (1 + (n + 1)) >= (1 + 0 ) & ((n + 2) + n) >= ((n + 2) + 0 ) by XREAL_1: 6;

      then

       A4: (n + 2) in ( dom ( Newton_Coeff ((2 * n) + 1))) & (n + 1) = ((n + 2) - 1) by A2, FINSEQ_3: 25;

      (((2 * n) + 1) - n) = (n + 1);

      then

      reconsider l = (k - n) as Nat;

      (( Newton_Coeff ((2 * n) + 1)) . (n + 1)) = (((2 * n) + 1) choose n) by NCI

      .= (k choose l) by A0, NEWTON: 20

      .= (( Newton_Coeff ((2 * n) + 1)) . (n + 2)) by A4, NEWTON:def 5;

      hence thesis;

    end;

    theorem :: NEWTON04:78

    for a be non zero Integer st 1 <= k <= n holds a divides (((a,b) Subnomial n) . k)

    proof

      let a be non zero Integer;

      

       A0: ( len ((a,b) Subnomial n)) = (n + 1) by Def2;

      assume

       A1: 1 <= k <= n;

      then

      reconsider m = (k - 1) as Nat;

      ((k - 1) + 1) > ((k - 1) + 0 ) by XREAL_1: 6;

      then

      consider l be Nat such that

       A2: n = (m + l) by A1, XXREAL_0: 2, NAT_1: 10;

      (m + l) >= (m + 1) by A1, A2;

      then l >= 1 by XREAL_1: 6;

      then

      reconsider s = (l - 1) as Nat;

      

       A4: l = (n - m) by A2;

      (k + 0 ) <= (n + 1) by XREAL_1: 7, A1;

      then k in ( dom ((a,b) Subnomial n)) by A0, A1, FINSEQ_3: 25;

      

      then (((a,b) Subnomial n) . k) = ((a |^ (s + 1)) * (b |^ m)) by Def2, A4

      .= ((a * (a |^ s)) * (b |^ m)) by NEWTON: 6

      .= (a * ((a |^ s) * (b |^ m)));

      hence thesis;

    end;

    theorem :: NEWTON04:79

    

     DIS: for a,b be Integer holds (a * b) divides ((((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i))

    proof

      let a,b be Integer;

      per cases ;

        suppose

         A1: i in ( dom ((a,b) In_Power ((n + 1) - 1)));

        then

         A1a: i in ( dom ((a,b) Subnomial ((n + 1) - 1))) by DOMN;

        then

         A1b: 1 <= i <= ( len ((a,b) Subnomial ((n + 1) - 1))) by FINSEQ_3: 25;

        then

         A1c: (1 - 1) <= (i - 1) <= n by XREAL_1: 9;

        reconsider m = (i - 1) as Nat by A1b;

        (n - m) >= (m - m) by A1c, XREAL_1: 9;

        then

        reconsider l = (n - m) as Nat by INT_1: 3;

        

         A2: (((a,b) In_Power n) . i) = (((n choose m) * (a |^ l)) * (b |^ m)) by A1, NEWTON:def 4;

        

         A3: ((((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)) = ((((n choose m) * (a |^ l)) * (b |^ m)) - ((a |^ l) * (b |^ m))) by A1a, Def2, A2

        .= (((n choose m) - 1) * ((a |^ l) * (b |^ m)));

        per cases ;

          suppose m = 0 or m = n;

          then (n choose m) = 1 by NEWTON: 19, NEWTON: 21;

          hence thesis by A3, INT_2: 12;

        end;

          suppose m > 0 & m <> n;

          then 0 < m < n by A1c, XXREAL_0: 1;

          then m > 0 & (n - m) > (m - m) by XREAL_1: 9;

          then a divides (a |^ l) & b divides (b |^ m) by NEWTON02: 14;

          then (a * b) divides ((a |^ l) * (b |^ m)) by NEWTON02: 2;

          hence thesis by A3, INT_2: 2;

        end;

      end;

        suppose

         A1: not i in ( dom ((a,b) In_Power ((n + 1) - 1)));

        then not i in ( dom ((a,b) Subnomial ((n + 1) - 1))) by DOMN;

        then (((a,b) In_Power n) . i) = 0 & (((a,b) Subnomial n) . i) = 0 by A1, FUNCT_1:def 2;

        hence thesis by INT_2: 12;

      end;

    end;

    theorem :: NEWTON04:80

    

     INT436: for f be INT -valued FinSequence, a be Integer st (for n be Nat st n in ( dom f) holds a divides (f . n)) holds a divides ( Sum f)

    proof

      let f be INT -valued FinSequence, a be Integer such that

       A1: for n be Nat st n in ( dom f) holds a divides (f . n);

      reconsider f1 = f as FinSequence of REAL by NEWTON02: 103;

      (f1 . ( min_p f1)) in INT by INT_1:def 2;

      then

      reconsider k = ( min f1) as Integer by RFINSEQ2:def 4;

      reconsider f2 = f as FinSequence of COMPLEX by NEWTON02: 103;

      reconsider g = (f2 - k) as FinSequence of INT by NEWTON02: 103;

      reconsider g as FinSequence of NAT by NEWTON02: 103;

       |.a.| in INT & |.a.| >= 0 by INT_1:def 2;

      then

      reconsider l = |.a.| as Nat;

      

       A1a: a divides k

      proof

        per cases ;

          suppose

           B1: ( min_p f1) in ( dom f1);

          reconsider x = ( min_p f1) as Nat;

          a divides (f . x) by B1, A1;

          hence thesis by RFINSEQ2:def 4;

        end;

          suppose not ( min_p f1) in ( dom f1);

          

          then 0 = (f1 . ( min_p f1)) by FUNCT_1:def 2

          .= k by RFINSEQ2:def 4;

          hence thesis by INT_2: 12;

        end;

      end;

      m in ( dom g) implies l divides (g . m)

      proof

        assume

         B1: m in ( dom g);

        

         B2: m in ( dom (f2 + ( - k))) by B1, VALUED_1:def 3;

        then m in ( dom f) by VALUED_1:def 2;

        then a divides (f . m) & a divides ( - k) by A1, A1a, INT_2: 10;

        then a divides ((f . m) + ( - k)) by WSIERP_1: 4;

        then a divides ((f + ( - k)) . m) by B2, VALUED_1:def 2;

        then a divides ((f - k) . m) by VALUED_1:def 3;

        hence thesis by WSIERP_1: 13;

      end;

      then

       A2: a divides ( Sum g) by INT_4: 36, WSIERP_1: 13;

      

       A3: a divides (k * ( len g)) by A1a, INT_2: 2;

      reconsider g as FinSequence of COMPLEX by NEWTON02: 103;

      ( Sum (g + k)) = (( Sum g) + (k * ( len g))) by SFX;

      hence thesis by A2, A3, WSIERP_1: 4;

    end;

    theorem :: NEWTON04:81

    for a,b be Integer holds ((a * b) * (a - b)) divides (((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1))))

    proof

      let a,b be Integer;

      

       A0: ( len ((a,b) In_Power ((n + 1) - 1))) = (n + 1) & ( len ((a,b) Subnomial ((n + 1) - 1))) = (n + 1);

      reconsider R1 = ((a,b) In_Power n) as Element of ((n + 1) -tuples_on REAL ) by A0, FINSEQ_2: 92;

      reconsider R2 = ((a,b) Subnomial n) as Element of ((n + 1) -tuples_on REAL ) by A0, FINSEQ_2: 92;

      

       A1: ( Sum (((a,b) In_Power n) - ((a,b) Subnomial n))) = ( Sum (R1 - R2))

      .= (( Sum ((a,b) In_Power n)) - ( Sum ((a,b) Subnomial n))) by RVSUM_1: 90;

      reconsider f = (((a,b) In_Power n) - ((a,b) Subnomial n)) as INT -valued FinSequence;

      for i be Nat st i in ( dom f) holds (a * b) divides ((((a,b) In_Power n) - ((a,b) Subnomial n)) . i)

      proof

        let i be Nat such that

         B1: i in ( dom f);

        (a * b) divides ((((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)) by DIS;

        hence thesis by B1, VALUED_1: 13;

      end;

      then

       A2: (a * b) divides ( Sum (((a,b) In_Power n) - ((a,b) Subnomial n))) by INT436;

      (((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1)))) = (((a - b) * ((a + b) |^ n)) - ((a - b) * ( Sum ((a,b) Subnomial n)))) by SumS

      .= (((a - b) * ( Sum ((a,b) In_Power n))) - ((a - b) * ( Sum ((a,b) Subnomial n)))) by NEWTON: 30

      .= ((a - b) * (( Sum ((a,b) In_Power n)) - ( Sum ((a,b) Subnomial n))));

      hence thesis by A1, A2, NEWTON02: 2;

    end;

    theorem :: NEWTON04:82

    

     ILS: for a,b be non negative Real holds (((a,b) In_Power n) . i) >= (((a,b) Subnomial n) . i)

    proof

      let a,b be non negative Real;

      per cases ;

        suppose i in ( dom ( Newton_Coeff n));

        then (( Newton_Coeff n) . i) <> 0 by D1;

        then ((( Newton_Coeff n) . i) * (((a,b) Subnomial n) . i)) >= (1 * (((a,b) Subnomial n) . i)) by NAT_1: 14, XREAL_1: 64;

        then ((( Newton_Coeff n) (#) ((a,b) Subnomial n)) . i) >= (((a,b) Subnomial n) . i) by VALUED_1: 5;

        hence thesis by INS;

      end;

        suppose not i in ( dom ( Newton_Coeff n));

        then not i in (( dom ((a,b) In_Power n)) /\ ( dom ( Newton_Coeff n)));

        then not i in ( dom ((a,b) Subnomial n)) by VALUED_1: 16;

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: NEWTON04:83

    

     SST: for a,b be non negative Real holds ((a + b) |^ n) >= ( Sum ((a,b) Subnomial n))

    proof

      let a,b be non negative Real;

      for i be Nat holds (((a,b) In_Power n) . i) >= (((a,b) Subnomial n) . i) by ILS;

      then ( Sum ((a,b) In_Power n)) >= ( Sum ((a,b) Subnomial n)) by NYS;

      hence thesis by NEWTON: 30;

    end;

    theorem :: NEWTON04:84

    

     SLT: for a,b be non negative Real, n be non zero Nat holds ((a |^ n) + (b |^ n)) <= ( Sum ((a,b) Subnomial n))

    proof

      let a,b be non negative Real, n be non zero Nat;

      reconsider f = ((a,b) Subnomial n) as nonnegative-yielding FinSequence of REAL ;

      ( len f) = (n + 1) by Def2;

      then

       A1: ( Sum f) = ((( Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))) by NEWTON02: 115;

      

       A2: (((a,b) Subnomial n) . 1) = (((a,b) In_Power n) . 1) by NS

      .= (a |^ n) by NEWTON: 28;

      

       A3: (((a,b) Subnomial n) . (n + 1)) = (((a,b) In_Power n) . (n + 1)) by NS

      .= (b |^ n) by NEWTON: 29;

      (( Sum ((f | n) /^ 1)) + ((a |^ n) + (b |^ n))) >= ( 0 + ((a |^ n) + (b |^ n))) by XREAL_1: 6;

      hence thesis by A1, A2, A3;

    end;

    

     PLT: for a,b be non negative Real, n be non zero Nat holds (a * (((a + b) + b) |^ n)) >= (((a + b) |^ (n + 1)) - (b |^ (n + 1))) >= (a * (((a + b) |^ n) + (b |^ n)))

    proof

      let a,b be non negative Real, n be non zero Nat;

      (((a + b) - b) * ( Sum (((a + b),b) Subnomial n))) = (((a + b) |^ (n + 1)) - (b |^ (n + 1))) by SumS;

      hence thesis by SST, SLT, XREAL_1: 64;

    end;

    theorem :: NEWTON04:85

    for a,b be non negative Real, n be non zero Nat holds ((a * ((a + (2 * b)) |^ n)) + (b |^ (n + 1))) >= ((a + b) |^ (n + 1))

    proof

      let a,b be non negative Real, n be non zero Nat;

      ((a * (((a + b) + b) |^ n)) + (b |^ (n + 1))) >= ((((a + b) |^ (n + 1)) - (b |^ (n + 1))) + (b |^ (n + 1))) by PLT, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: NEWTON04:86

    for a,b be non negative Real, n be non zero Nat holds ((a * ((a + b) |^ n)) + ((a + b) * (b |^ n))) <= ((a + b) |^ (n + 1))

    proof

      let a,b be non negative Real, n be non zero Nat;

      ((a * (((a + b) |^ n) + (b |^ n))) + (b * (b |^ n))) <= ((((a + b) |^ (n + 1)) - (b |^ (n + 1))) + (b * (b |^ n))) by PLT, XREAL_1: 6;

      then ((a * ((a + b) |^ n)) + ((a + b) * (b |^ n))) <= ((((a + b) |^ (n + 1)) - (b |^ (n + 1))) + (b |^ (n + 1))) by NEWTON: 6;

      hence thesis;

    end;

    theorem :: NEWTON04:87

    

     SSI: for a,b be positive Real, n be non zero Nat holds ( Sum ((a,b) Subnomial (n + 1))) < ( Sum ((a,b) In_Power (n + 1)))

    proof

      let a,b be positive Real, n be non zero Nat;

      

       A1: for i be Nat holds (((a,b) Subnomial (n + 1)) . i) <= (((a,b) In_Power (n + 1)) . i) by ILS;

      reconsider h = ((a,b) Subnomial (n + 1)) as nonnegative-yielding FinSequence of REAL ;

      reconsider g = ((a,b) In_Power (n + 1)) as nonnegative-yielding FinSequence of REAL ;

      (1 + 0 ) < (1 + n) by XREAL_1: 6;

      then (1 * (((a,b) Subnomial (n + 1)) . (n + 1))) < ((( Newton_Coeff (n + 1)) . (n + 1)) * (((a,b) Subnomial (n + 1)) . (n + 1))) by XREAL_1: 68;

      then (((a,b) Subnomial (n + 1)) . (n + 1)) < ((( Newton_Coeff (n + 1)) (#) ((a,b) Subnomial (n + 1))) . (n + 1)) by VALUED_1: 5;

      then (((a,b) Subnomial (n + 1)) . (n + 1)) < (((a,b) In_Power (n + 1)) . (n + 1)) by INS;

      hence thesis by A1, NYS1;

    end;

    theorem :: NEWTON04:88

    for a,b be positive Real, n be non zero Nat holds ( Sum (((a + b), 0 ) Subnomial (n + 1))) > ( Sum ((a,b) Subnomial (n + 1)))

    proof

      let a,b be positive Real, n be non zero Nat;

      (((a + b) - 0 ) * ( Sum (((a + b), 0 ) Subnomial (n + 1)))) = (((a + b) |^ ((n + 1) + 1)) - ( 0 |^ ((n + 1) + 1))) by SumS;

      then ((a + b) * ( Sum (((a + b), 0 ) Subnomial (n + 1)))) = ((a + b) * ((a + b) |^ (n + 1))) by NEWTON: 6;

      then ( Sum (((a + b), 0 ) Subnomial (n + 1))) = ((a + b) |^ (n + 1)) by XCMPLX_1: 5;

      then ( Sum (((a + b), 0 ) Subnomial (n + 1))) = ( Sum ((a,b) In_Power (n + 1))) by NEWTON: 30;

      hence thesis by SSI;

    end;

    theorem :: NEWTON04:89

    for a,b be Real, n,i be Nat holds (((a,b) Subnomial n) . i) <= ((( |.a.|, |.b.|) Subnomial n) . i)

    proof

      let a,b be Real, n,i be Nat;

      reconsider f = (( |.a.|, |.b.|) Subnomial n) as nonnegative-yielding FinSequence of REAL ;

      per cases ;

        suppose not i in ( dom ((a,b) Subnomial n));

        hence thesis by FUNCT_1:def 2;

      end;

        suppose

         A0: i in ( dom ((a,b) Subnomial n));

        then

         A1: 1 <= i <= ( len ((a,b) Subnomial ((n + 1) - 1))) by FINSEQ_3: 25;

        then

        reconsider l = (i - 1) as Nat;

        ex k be Nat st (n + 1) = ((l + 1) + k) by A1, NAT_1: 10;

        then

        reconsider k = ((n + 1) - (l + 1)) as Nat;

        

         A2: k = (n - l) & l = (i - 1);

        

         A3: ( |.a.| |^ k) = |.(a |^ k).| & ( |.b.| |^ l) = |.(b |^ l).| by TAYLOR_2: 1;

        

         A4: ( dom ((a,b) Subnomial n)) = ( dom ( Newton_Coeff n)) by DOMN

        .= ( dom (( |.a.|, |.b.|) Subnomial n)) by DOMN;

         |.((a |^ k) * (b |^ l)).| >= ((a |^ k) * (b |^ l)) by ABSVALUE: 4;

        then ( |.(a |^ k).| * |.(b |^ l).|) >= ((a |^ k) * (b |^ l)) by COMPLEX1: 65;

        then (( |.a.| |^ k) * ( |.b.| |^ l)) >= (((a,b) Subnomial (l + k)) . (l + 1)) by A0, A2, A3, LmS1;

        hence thesis by A0, A2, A4, LmS1;

      end;

    end;

    theorem :: NEWTON04:90

    for a be Real, n be Nat, i be odd Nat holds (((a,( - a)) Subnomial (n + i)) . i) = (a |^ (n + i))

    proof

      let a be Real, n be Nat, i be odd Nat;

      

       A1: ( len ((a,a) Subnomial (((n + i) + 1) - 1))) = ((n + i) + 1) & ( len ((a,( - a)) Subnomial (((n + i) + 1) - 1))) = ((n + i) + 1);

      i >= 1 & (i + (n + 1)) >= (i + 0 ) by XREAL_1: 6, NAT_1: 14;

      then

       A2: i in ( dom ((a,a) Subnomial (i + n))) & i in ( dom ((a,( - a)) Subnomial (i + n))) by A1, FINSEQ_3: 25;

      

      then ((((a * 1),(( - 1) * a)) Subnomial (n + i)) . i) = ((((a,a) Subnomial (n + i)) . i) * (((1,( - 1)) Subnomial (n + i)) . i)) by STT

      .= (a |^ (n + i)) by A2, CONST;

      hence thesis;

    end;

    theorem :: NEWTON04:91

    for a be Real, n be Nat, i be non zero Nat holds (((a,( - a)) Subnomial (n + (2 * i))) . (2 * i)) = ( - (a |^ (n + (2 * i))))

    proof

      let a be Real, n be Nat, i be non zero Nat;

      

       A1: ( len ((a,a) Subnomial (((n + (2 * i)) + 1) - 1))) = ((n + (2 * i)) + 1) & ( len ((a,( - a)) Subnomial (((n + (2 * i)) + 1) - 1))) = ((n + (2 * i)) + 1);

      (2 * i) >= 1 & ((2 * i) + (n + 1)) >= ((2 * i) + 0 ) by XREAL_1: 6, NAT_1: 14;

      then

       A2: (2 * i) in ( dom ((a,a) Subnomial ((2 * i) + n))) & (2 * i) in ( dom ((a,( - a)) Subnomial ((2 * i) + n))) by A1, FINSEQ_3: 25;

      

      then ((((a * 1),(( - 1) * a)) Subnomial (n + (2 * i))) . (2 * i)) = ((((a,a) Subnomial (n + (2 * i))) . (2 * i)) * (((1,( - 1)) Subnomial (n + (2 * i))) . (2 * i))) by STT

      .= ((a |^ (n + (2 * i))) * ( - 1)) by A2, CONST;

      hence thesis;

    end;

    theorem :: NEWTON04:92

    

     SAN: for a,b be Real, n be Nat holds ((a,b) Subnomial (n + 1)) = ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))

    proof

      let a,b be Real, n be Nat;

      

       A0: ( dom ((a,b) Subnomial n)) = ( dom (b * ((a,b) Subnomial n))) by VALUED_1:def 5;

      

       A1: ( dom ((a,b) Subnomial (n + 1))) = ( dom ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))))

      proof

        ( len ((a,b) Subnomial (((n + 1) + 1) - 1))) = (1 + ( len ((a,b) Subnomial ((n + 1) - 1))))

        .= ((1 * ( len <*(a |^ (n + 1))*>)) + ( len ((a,b) Subnomial n)))

        .= (( len <*(a |^ (n + 1))*>) + ( len (b * ((a,b) Subnomial n)))) by A0, FINSEQ_3: 29

        .= ( len ( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n)))) by FINSEQ_1: 22;

        hence thesis by FINSEQ_3: 29;

      end;

      for i be object st i in ( dom ((a,b) Subnomial (n + 1))) holds (((a,b) Subnomial (n + 1)) . i) = (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . i)

      proof

        let i be object such that

         B1: i in ( dom ((a,b) Subnomial (n + 1)));

        reconsider i as non zero Nat by B1, FINSEQ_3: 25;

        

         B2: 1 <= i <= ( len ((a,b) Subnomial (((n + 1) + 1) - 1))) by B1, FINSEQ_3: 25;

        reconsider j = (i - 1) as Nat;

        

         B3: (j + 1) <= ((n + 1) + 1) by B2;

        then ex k be Nat st (n + 1) = (j + k) by XREAL_1: 6, NAT_1: 10;

        then

        reconsider k = ((n + 1) - j) as Nat;

        set m = (n + 1);

        per cases ;

          suppose

           C1: j = 0 ;

          then

           C2: (( len ((a,b) Subnomial ((m + 1) - 1))) - 1) = m & j = (1 - 1) & (m - j) = m;

          (1 + 0 ) <= (1 + m) by XREAL_1: 6;

          then 1 <= ( len ((a,b) Subnomial ((m + 1) - 1)));

          then 1 in ( dom ((a,b) Subnomial m)) by FINSEQ_3: 25;

          

          then (((a,b) Subnomial m) . 1) = ((a |^ (n + 1)) * (1 * (b |^ 0 ))) by C2, Def2

          .= (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . 1);

          hence thesis by C1;

        end;

          suppose

           C0: j > 0 ;

          then ( len ((a,b) Subnomial ((n + 1) - 1))) >= j >= ( 0 + 1) by B3, XREAL_1: 6, NAT_1: 13;

          then

           C1: j in ( dom ((a,b) Subnomial ((n + 1) - 1))) by FINSEQ_3: 25;

          then

           C2: j in ( dom (b * ((a,b) Subnomial ((n + 1) - 1)))) by VALUED_1:def 5;

          then

           C3: ( len (b * ((a,b) Subnomial ((n + 1) - 1)))) >= j >= 1 by FINSEQ_3: 25;

          reconsider x = (j - 1) as Nat by C0;

          

           C5: n = (x + k) & k = (n - x);

          (1 * ( len <*(a |^ (n + 1))*>)) = 1;

          

          then (( <*(a |^ (n + 1))*> ^ (b * ((a,b) Subnomial n))) . (1 + j)) = ((b * ((a,b) Subnomial n)) . j) by C3, FINSEQ_1: 65

          .= (b * (((a,b) Subnomial ((n + 1) - 1)) . j)) by C2, VALUED_1:def 5

          .= (b * ((a |^ k) * (b |^ x))) by C1, C5, Def2

          .= ((a |^ k) * (b * (b |^ x)))

          .= ((a |^ k) * (b |^ (x + 1))) by NEWTON: 6

          .= (((a,b) Subnomial (((n + 1) + 1) - 1)) . i) by B1, Def2;

          hence thesis;

        end;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: NEWTON04:93

    for a,b be Real, n be Nat holds ((a,b) Subnomial (n + 2)) = (( <*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>)

    proof

      let a,b be Real, n be Nat;

      reconsider f = ((b,a) Subnomial n) as complex-valued FinSequence;

      

       A0: ( Rev ((b,a) Subnomial (n + 1))) = ( Rev ( <*(b |^ (n + 1))*> ^ (a * ((b,a) Subnomial n)))) by SAN

      .= (( Rev (a * ((b,a) Subnomial n))) ^ ( Rev <*(b |^ (n + 1))*>)) by FINSEQ_5: 64

      .= ((a * ( Rev ((b,a) Subnomial n))) ^ ( Rev <*(b |^ (n + 1))*>)) by CREV

      .= ((a * ((a,b) Subnomial n)) ^ <*(b |^ (n + 1))*>) by SAB;

      ((a,b) Subnomial ((n + 1) + 1)) = ( <*(a |^ (n + 2))*> ^ (b * ((a,b) Subnomial (n + 1)))) by SAN

      .= ( <*(a |^ (n + 2))*> ^ (b * ( Rev ((b,a) Subnomial (n + 1))))) by SAB

      .= ( <*(a |^ (n + 2))*> ^ ((b * (a * ((a,b) Subnomial n))) ^ (b * <*(b |^ (n + 1))*>))) by A0, ADP

      .= (( <*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ (b * <*(b |^ (n + 1))*>)) by FINSEQ_1: 32

      .= (( <*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ <*(b * (b |^ (n + 1)))*>) by AMP

      .= (( <*(a |^ (n + 2))*> ^ (b * (a * ((a,b) Subnomial n)))) ^ <*(b |^ ((n + 1) + 1))*>) by NEWTON: 6

      .= (( <*(a |^ (n + 2))*> ^ ((b * a) * ((a,b) Subnomial n))) ^ <*(b |^ ((n + 1) + 1))*>) by VALUED_2: 16;

      hence thesis;

    end;