flexary1.miz



    begin

    reserve x,y for object,

D,D1,D2 for non empty set,

i,j,k,m,n for Nat,

f,g for FinSequence of (D * ),

f1 for FinSequence of (D1 * ),

f2 for FinSequence of (D2 * );

    

     Lm1: f = {} implies ((D -concatenation ) "**" f) = {}

    proof

      assume

       A1: f = {} ;

      (D -concatenation ) is having_a_unity by MONOID_0: 67;

      

      then ((D -concatenation ) "**" f) = ( the_unity_wrt (D -concatenation )) by A1, FINSOP_1:def 1

      .= {} by MONOID_0: 67;

      hence thesis;

    end;

    theorem :: FLEXARY1:1

    

     Th1: for F be Function-yielding Function, a be object holds a in ( Values F) iff ex x, y st x in ( dom F) & y in ( dom (F . x)) & a = ((F . x) . y)

    proof

      let F be Function-yielding Function, a be object;

      

       A1: ( Values F) = ( Union ( rngs F)) by MATRIX_0:def 9

      .= ( union ( rng ( rngs F))) by CARD_3:def 4;

      

       A2: ( dom ( rngs F)) = ( dom F) by FUNCT_6:def 3;

      thus a in ( Values F) implies ex x,y be object st x in ( dom F) & y in ( dom (F . x)) & a = ((F . x) . y)

      proof

        assume a in ( Values F);

        then

        consider y be set such that

         A3: a in y & y in ( rng ( rngs F)) by A1, TARSKI:def 4;

        consider z be object such that

         A4: z in ( dom ( rngs F)) & (( rngs F) . z) = y by A3, FUNCT_1:def 3;

        y = ( rng (F . z)) by A2, A4, FUNCT_6:def 3;

        then ex x be object st x in ( dom (F . z)) & a = ((F . z) . x) by A3, FUNCT_1:def 3;

        hence thesis by A2, A4;

      end;

      given x,y be object such that

       A5: x in ( dom F) & y in ( dom (F . x)) & a = ((F . x) . y);

      (( rngs F) . x) = ( rng (F . x)) by A5, FUNCT_6:def 3;

      then

       A6: ( rng (F . x)) in ( rng ( rngs F)) by A5, A2, FUNCT_1:def 3;

      a in ( rng (F . x)) by A5, FUNCT_1:def 3;

      hence thesis by A6, TARSKI:def 4, A1;

    end;

    theorem :: FLEXARY1:2

    

     Th2: for D be set, f,g be FinSequence of (D * ) holds ( Values (f ^ g)) = (( Values f) \/ ( Values g))

    proof

      let D be set, f,g be FinSequence of (D * );

      set F = (f ^ g);

      

       A1: ( Values f) c= ( Values F)

      proof

        let a be object;

        assume a in ( Values f);

        then

        consider x,y be object such that

         A2: x in ( dom f) & y in ( dom (f . x)) & a = ((f . x) . y) by Th1;

        reconsider x as Nat by A2;

        

         A3: ( dom f) c= ( dom F) by FINSEQ_1: 26;

        (f . x) = (F . x) by A2, FINSEQ_1:def 7;

        hence thesis by A3, A2, Th1;

      end;

      

       A4: ( Values g) c= ( Values F)

      proof

        let a be object;

        assume a in ( Values g);

        then

        consider x,y be object such that

         A5: x in ( dom g) & y in ( dom (g . x)) & a = ((g . x) . y) by Th1;

        reconsider x as Nat by A5;

        (( len f) + x) in ( dom F) & (F . (( len f) + x)) = (g . x) by A5, FINSEQ_1: 28, FINSEQ_1:def 7;

        hence thesis by A5, Th1;

      end;

      ( Values F) c= (( Values f) \/ ( Values g))

      proof

        let a be object;

        assume a in ( Values F);

        then

        consider x,y be object such that

         A6: x in ( dom F) & y in ( dom (F . x)) & a = ((F . x) . y) by Th1;

        reconsider x as Nat by A6;

        per cases by A6, FINSEQ_1: 25;

          suppose

           A7: x in ( dom f);

          then (f . x) = (F . x) by FINSEQ_1:def 7;

          then a in ( Values f) by Th1, A6, A7;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose ex k st k in ( dom g) & x = (( len f) + k);

          then

          consider k such that

           A8: k in ( dom g) & x = (( len f) + k);

          (F . x) = (g . k) by A8, FINSEQ_1:def 7;

          then a in ( Values g) by Th1, A6, A8;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis by A1, A4, XBOOLE_1: 8;

    end;

    theorem :: FLEXARY1:3

    

     Th3: ((D -concatenation ) "**" (f ^ g)) = (((D -concatenation ) "**" f) ^ ((D -concatenation ) "**" g))

    proof

      set DC = (D -concatenation );

      reconsider df = (DC "**" f), dg = (DC "**" g) as Element of (D *+^ ) by MONOID_0:def 34;

      

      thus (DC "**" (f ^ g)) = (DC . ((DC "**" f),(DC "**" g))) by MONOID_0: 67, FINSOP_1: 5

      .= (the multF of (D *+^ ) . ((DC "**" f),(DC "**" g))) by MONOID_0:def 36

      .= (df * dg) by ALGSTR_0:def 18

      .= ((DC "**" f) ^ (DC "**" g)) by MONOID_0:def 34;

    end;

    theorem :: FLEXARY1:4

    ( rng ((D -concatenation ) "**" f)) = ( Values f)

    proof

      set DC = (D -concatenation );

      defpred P[ Nat] means for f be FinSequence of (D * ) st ( len f) = $1 holds ( rng (DC "**" f)) = ( Values f);

      

       A1: P[ 0 ]

      proof

        let f be FinSequence of (D * ) such that

         A2: ( len f) = 0 ;

        

         A3: f = {} by A2;

        then (DC "**" f) = {} by Lm1;

        then

         A4: ( rng (DC "**" f)) = {} ;

        assume ( rng (DC "**" f)) <> ( Values f);

        then

        consider a be object such that

         A5: a in ( Values f) by A4, XBOOLE_0:def 1;

        ex x,y be object st x in ( dom f) & y in ( dom (f . x)) & a = ((f . x) . y) by A5, Th1;

        hence thesis by A3;

      end;

      

       A6: P[i] implies P[(i + 1)]

      proof

        assume

         A7: P[i];

        set i1 = (i + 1);

        let f1 be FinSequence of (D * ) such that

         A8: ( len f1) = i1;

        consider f be FinSequence of (D * ), d be Element of (D * ) such that

         A9: f1 = (f ^ <*d*>) by FINSEQ_2: 19, A8;

        (( len f) + 1) = ( len f1) by A9, FINSEQ_2: 16;

        then

         A10: ( rng (DC "**" f)) = ( Values f) by A8, A7;

        (DC "**" f1) = ((DC "**" f) ^ (DC "**" <*d*>)) by Th3, A9

        .= ((DC "**" f) ^ d) by FINSOP_1: 11;

        then

         A11: ( rng (DC "**" f1)) = (( rng (DC "**" f)) \/ ( rng d)) by FINSEQ_1: 31;

        

         A12: ( rngs <*d*>) = <*( rng d)*> by FINSEQ_3: 132;

        ( rng <*( rng d)*>) = {( rng d)} by FINSEQ_1: 38;

        then ( union ( rng <*( rng d)*>)) = ( rng d) by ZFMISC_1: 25;

        then ( Union ( rngs <*d*>)) = ( rng d) by CARD_3:def 4, A12;

        then ( Values <*d*>) = ( rng d) by MATRIX_0:def 9;

        hence thesis by Th2, A9, A10, A11;

      end;

      

       A13: P[i] from NAT_1:sch 2( A1, A6);

       P[( len f)] by A13;

      hence thesis;

    end;

    theorem :: FLEXARY1:5

    f1 = f2 implies ((D1 -concatenation ) "**" f1) = ((D2 -concatenation ) "**" f2)

    proof

      set CC = (D2 -concatenation );

      set NC = (D1 -concatenation );

      defpred P[ Nat] means for fn be FinSequence of (D1 * ), fc be FinSequence of (D2 * ) st $1 = ( len fn) & fn = fc holds (NC "**" fn) = (CC "**" fc);

      

       A1: P[ 0 ]

      proof

        let fn be FinSequence of (D1 * ), fc be FinSequence of (D2 * );

        assume 0 = ( len fn) & fn = fc;

        then fn = {} & fc = {} ;

        then (NC "**" fn) = {} & (CC "**" fc) = {} by Lm1;

        hence thesis;

      end;

      

       A2: P[i] implies P[(i + 1)]

      proof

        assume

         A3: P[i];

        set i1 = (i + 1);

        let fn be FinSequence of (D1 * ), fc be FinSequence of (D2 * );

        assume

         A4: i1 = ( len fn) & fn = fc;

        then

        consider f1 be FinSequence of (D1 * ), d1 be Element of (D1 * ) such that

         A5: fn = (f1 ^ <*d1*>) by FINSEQ_2: 19;

        consider f2 be FinSequence of (D2 * ), d2 be Element of (D2 * ) such that

         A6: fc = (f2 ^ <*d2*>) by FINSEQ_2: 19, A4;

        

         A7: (( len f1) + 1) = ( len fn) by A5, FINSEQ_2: 16;

        

         A8: (CC "**" fc) = ((CC "**" f2) ^ (CC "**" <*d2*>)) by Th3, A6

        .= ((CC "**" f2) ^ d2) by FINSOP_1: 11;

        

         A9: (NC "**" fn) = ((NC "**" f1) ^ (NC "**" <*d1*>)) by Th3, A5

        .= ((NC "**" f1) ^ d1) by FINSOP_1: 11;

        f1 = f2 & d1 = d2 by A5, A6, A4, FINSEQ_2: 17;

        hence thesis by A3, A7, A4, A8, A9;

      end;

       P[i] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FLEXARY1:6

    i in ( dom ((D -concatenation ) "**" f)) iff ex n, k st (n + 1) in ( dom f) & k in ( dom (f . (n + 1))) & i = (k + ( len ((D -concatenation ) "**" (f | n))))

    proof

      set DC = (D -concatenation );

      defpred P[ Nat] means for i holds for f be FinSequence of (D * ) st ( len f) = $1 holds i in ( dom (DC "**" f)) iff ex n, k st (n + 1) in ( dom f) & k in ( dom (f . (n + 1))) & i = (k + ( len (DC "**" (f | n))));

      

       A1: P[ 0 ]

      proof

        let i;

        let f be FinSequence of (D * );

        assume ( len f) = 0 ;

        then f = {} ;

        hence thesis by Lm1;

      end;

      

       A2: P[j] implies P[(j + 1)]

      proof

        assume

         A3: P[j];

        set j1 = (j + 1);

        let i;

        let f1 be FinSequence of (D * ) such that

         A4: ( len f1) = j1;

        consider f be FinSequence of (D * ), d be Element of (D * ) such that

         A5: f1 = (f ^ <*d*>) by FINSEQ_2: 19, A4;

        

         A6: (( len f) + 1) = ( len f1) by A5, FINSEQ_2: 16;

        

         A7: (DC "**" f1) = ((DC "**" f) ^ (DC "**" <*d*>)) by Th3, A5

        .= ((DC "**" f) ^ d) by FINSOP_1: 11;

        

         A8: ( dom f) c= ( dom f1) by A5, FINSEQ_1: 26;

        thus i in ( dom (DC "**" f1)) implies ex n, k st (n + 1) in ( dom f1) & k in ( dom (f1 . (n + 1))) & i = (k + ( len (DC "**" (f1 | n))))

        proof

          assume

           A9: i in ( dom (DC "**" f1));

          per cases by A9, A7, FINSEQ_1: 25;

            suppose i in ( dom (DC "**" f));

            then

            consider n, k such that

             A10: (n + 1) in ( dom f) & k in ( dom (f . (n + 1))) & i = (k + ( len (DC "**" (f | n)))) by A6, A4, A3;

            take n, k;

            thus (n + 1) in ( dom f1) & k in ( dom (f1 . (n + 1))) by A10, A5, A8, FINSEQ_1:def 7;

            1 <= (n + 1) & (n + 1) <= ( len f) by A10, FINSEQ_3: 25;

            then n <= ( len f) by NAT_1: 13;

            hence thesis by FINSEQ_5: 22, A5, A10;

          end;

            suppose ex l be Nat st l in ( dom d) & i = (( len (DC "**" f)) + l);

            then

            consider l be Nat such that

             A11: l in ( dom d) & i = (l + ( len (DC "**" f)));

            take n = ( len f), l;

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

            hence thesis by FINSEQ_1: 42, FINSEQ_5: 23, A5, A11, A6, FINSEQ_3: 25;

          end;

        end;

        given n, k such that

         A12: (n + 1) in ( dom f1) & k in ( dom (f1 . (n + 1))) & i = (k + ( len (DC "**" (f1 | n))));

        per cases by A12, A5, FINSEQ_1: 25;

          suppose

           A13: (n + 1) in ( dom f);

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

          then

           A14: n < ( len f) by NAT_1: 13;

          

           A15: k in ( dom (f . (n + 1))) by A13, A5, FINSEQ_1:def 7, A12;

          i = (k + ( len (DC "**" (f | n)))) by A12, A14, A5, FINSEQ_5: 22;

          then

           A16: i in ( dom (DC "**" f)) by A15, A13, A6, A4, A3;

          ( dom (DC "**" f)) c= ( dom (DC "**" f1)) by A7, FINSEQ_1: 26;

          hence i in ( dom (DC "**" f1)) by A16;

        end;

          suppose ex j st j in ( dom <*d*>) & (n + 1) = (( len f) + j);

          then

          consider j such that

           A17: j in ( dom <*d*>) & (n + 1) = (( len f) + j);

          ( dom <*d*>) = ( Seg 1) & ( Seg 1) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then j = 1 by A17, TARSKI:def 1;

          then (f1 . (n + 1)) = d & (f1 | n) = f by A17, FINSEQ_5: 23, A5, FINSEQ_1: 42;

          hence i in ( dom (DC "**" f1)) by A12, FINSEQ_1: 28, A7;

        end;

      end;

       P[j] from NAT_1:sch 2( A1, A2);

      then P[( len f)];

      hence thesis;

    end;

    theorem :: FLEXARY1:7

    i in ( dom ((D -concatenation ) "**" f)) implies (((D -concatenation ) "**" f) . i) = (((D -concatenation ) "**" (f ^ g)) . i) & (((D -concatenation ) "**" f) . i) = (((D -concatenation ) "**" (g ^ f)) . (i + ( len ((D -concatenation ) "**" g))))

    proof

      set DC = (D -concatenation );

      assume

       A1: i in ( dom (DC "**" f));

      

       A2: (DC "**" (f ^ g)) = ((DC "**" f) ^ (DC "**" g)) by Th3;

      (DC "**" (g ^ f)) = ((DC "**" g) ^ (DC "**" f)) by Th3;

      hence thesis by A2, A1, FINSEQ_1:def 7;

    end;

    theorem :: FLEXARY1:8

    k in ( dom (f . (n + 1))) implies ((f . (n + 1)) . k) = (((D -concatenation ) "**" f) . (k + ( len ((D -concatenation ) "**" (f | n)))))

    proof

      set DC = (D -concatenation );

      set n1 = (n + 1);

      assume

       A1: k in ( dom (f . n1));

      then (f . n1) <> {} ;

      then

       A2: n1 in ( dom f) by FUNCT_1:def 2;

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

      then

       A3: (f | n1) = ((f | n) ^ <*(f /. n1)*>) by FINSEQ_5: 82;

      

       A4: (f . n1) = (f /. n1) by A2, PARTFUN1:def 6;

      consider q be FinSequence such that

       A5: f = ((f | n1) ^ q) by FINSEQ_1: 80;

      reconsider q as FinSequence of (D * ) by A5, FINSEQ_1: 36;

      

       A6: (DC "**" (f | n1)) = ((DC "**" (f | n)) ^ (DC "**" <*(f /. n1)*>)) by A3, Th3

      .= ((DC "**" (f | n)) ^ (f /. n1)) by FINSOP_1: 11;

      then

       A7: ((DC "**" (f | n1)) . (k + ( len (DC "**" (f | n))))) = ((f . n1) . k) by A4, A1, FINSEQ_1:def 7;

      

       A8: (k + ( len (DC "**" (f | n)))) in ( dom (DC "**" (f | n1))) by A6, A4, A1, FINSEQ_1: 28;

      (DC "**" f) = ((DC "**" (f | n1)) ^ (DC "**" q)) by A5, Th3;

      hence thesis by A8, FINSEQ_1:def 7, A7;

    end;

    begin

    reserve f for complex-valued Function,

g,h for complex-valued FinSequence;

    definition

      let k, n;

      let f,g be complex-valued Function;

      :: FLEXARY1:def1

      func (f,k) +...+ (g,n) -> complex number means

      : Def1: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) implies it = ( Sum (h | ((n -' k) + 1))) if f = g & k <= n

      otherwise it = 0 ;

      existence

      proof

        per cases ;

          suppose f <> g or n < k;

          hence thesis;

        end;

          suppose f = g & n >= k;

          deffunc P( Nat) = (f . ((k + $1) - 1));

          set kn = ((n -' k) + 1);

          consider p be FinSequence such that

           A1: ( len p) = kn & for i st i in ( dom p) holds (p . i) = P(i) from FINSEQ_1:sch 2;

          ( rng p) c= COMPLEX

          proof

            let y be object;

            assume y in ( rng p);

            then

            consider x be object such that

             A2: x in ( dom p) & (p . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A2;

            (p . x) = (f . ((k + x) - 1)) by A2, A1;

            hence thesis by A2, XCMPLX_0:def 2;

          end;

          then

          reconsider p as complex-valued FinSequence by VALUED_0:def 1;

          reconsider S = ( Sum p) as complex number by TARSKI: 1;

          

           A3: ( Sum (p | kn)) = S by A1, FINSEQ_1: 58;

          (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) implies ( Sum (p | kn)) = ( Sum (h | kn))

          proof

            assume

             A4: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k));

            defpred P[ Nat] means $1 <= kn implies ( Sum (h | $1)) = ( Sum (p | $1));

            

             A5: P[ 0 ];

            

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

            proof

              let i;

              set i1 = (i + 1);

              assume

               A7: P[i];

              assume

               A8: i1 <= kn;

              

               A9: 1 <= i1 by NAT_1: 11;

              then (p | i1) = ((p | i) ^ <*(p . i1)*>) by FINSEQ_5: 10, A1, A8, FINSEQ_3: 25;

              then

               A10: ( Sum (p | i1)) = (( Sum (p | i)) + (p . i1)) by RVSUM_2: 31;

              

               A11: (p . i1) = (f . ((k + i1) - 1)) by A1, A9, A8, FINSEQ_3: 25;

              i <= (n -' k) by A8, XREAL_1: 6;

              then

               A12: (f . (k + i)) = (h . (1 + i)) by A4;

              per cases ;

                suppose i1 <= ( len h);

                then i1 in ( dom h) by NAT_1: 11, FINSEQ_3: 25;

                then (h | i1) = ((h | i) ^ <*(h . i1)*>) by FINSEQ_5: 10;

                hence thesis by RVSUM_2: 31, A8, NAT_1: 13, A7, A10, A11, A12;

              end;

                suppose

                 A13: i1 > ( len h);

                then not i1 in ( dom h) by FINSEQ_3: 25;

                then

                 A14: (h . i1) = 0 by FUNCT_1:def 2;

                (h | i) = h by A13, NAT_1: 13, FINSEQ_1: 58;

                hence thesis by A8, NAT_1: 13, A7, A10, A11, A12, A13, FINSEQ_1: 58, A14;

              end;

            end;

            for i holds P[i] from NAT_1:sch 2( A5, A6);

            hence thesis;

          end;

          hence thesis by A3;

        end;

      end;

      uniqueness

      proof

        now

          assume f = g;

          let C1,C2 be complex number such that

           A15: ((h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k))) implies C1 = ( Sum (h | ((n -' k) + 1))) and

           A16: ((h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k))) implies C2 = ( Sum (h | ((n -' k) + 1)));

          deffunc P( Nat) = (f . ((k + $1) - 1));

          set nk = ((n -' k) + 1);

          consider p be FinSequence such that

           A17: ( len p) = nk & for i st i in ( dom p) holds (p . i) = P(i) from FINSEQ_1:sch 2;

          ( rng p) c= COMPLEX

          proof

            let y be object;

            assume y in ( rng p);

            then

            consider x be object such that

             A18: x in ( dom p) & (p . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A18;

            (p . x) = (f . ((k + x) - 1)) by A18, A17;

            hence thesis by A18, XCMPLX_0:def 2;

          end;

          then

          reconsider p as complex-valued FinSequence by VALUED_0:def 1;

          (p . ( 0 + 1)) = (f . ( 0 + k)) & ... & (p . ((n -' k) + 1)) = (f . ((n -' k) + k))

          proof

            let i;

            assume 0 <= i & i <= (n -' k);

            then 1 <= (i + 1) & (i + 1) <= nk by NAT_1: 11, XREAL_1: 6;

            then (p . (i + 1)) = (f . ((k + (i + 1)) - 1)) by A17, FINSEQ_3: 25;

            hence (p . (i + 1)) = (f . (i + k));

          end;

          then C1 = ( Sum (p | ((n -' k) + 1))) & C2 = ( Sum (p | ((n -' k) + 1))) by A15, A16;

          hence C1 = C2;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: FLEXARY1:9

    

     Th9: k <= n implies ex h st ((f,k) +...+ (f,n)) = ( Sum h) & ( len h) = ((n -' k) + 1) & ((h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)))

    proof

      assume

       A1: k <= n;

      deffunc P( Nat) = (f . ((k + $1) - 1));

      set nk = ((n -' k) + 1);

      consider p be FinSequence such that

       A2: ( len p) = nk & for i st i in ( dom p) holds (p . i) = P(i) from FINSEQ_1:sch 2;

      ( rng p) c= COMPLEX

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A4: x in ( dom p) & (p . x) = y by FUNCT_1:def 3;

        reconsider x as Nat by A4;

        (p . x) = (f . ((k + x) - 1)) by A4, A2;

        hence thesis by A4, XCMPLX_0:def 2;

      end;

      then

      reconsider p as complex-valued FinSequence by VALUED_0:def 1;

      

       A5: (p . (1 + 0 )) = (f . (k + 0 )) & ... & (p . (1 + (n -' k))) = (f . (k + (n -' k)))

      proof

        let i;

        assume 0 <= i & i <= (n -' k);

        then 1 <= (i + 1) & (i + 1) <= nk by NAT_1: 11, XREAL_1: 6;

        then (p . (i + 1)) = (f . ((k + (i + 1)) - 1)) by A2, FINSEQ_3: 25;

        hence (p . (1 + i)) = (f . (k + i));

      end;

      then ((f,k) +...+ (f,n)) = ( Sum (p | ((n -' k) + 1))) by A1, Def1;

      then ( Sum p) = ((f,k) +...+ (f,n)) by FINSEQ_1: 58, A2;

      hence thesis by A2, A5;

    end;

    theorem :: FLEXARY1:10

    

     Th10: ((f,k) +...+ (f,n)) <> 0 implies ex i st k <= i & i <= n & i in ( dom f)

    proof

      assume

       A1: ((f,k) +...+ (f,n)) <> 0 ;

      then

       A2: n >= k by Def1;

      then

      consider h such that

       A3: ((f,k) +...+ (f,n)) = ( Sum h) and

       A4: ( len h) = ((n -' k) + 1) and

       A5: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) by Th9;

      assume

       A6: for i st k <= i & i <= n holds not i in ( dom f);

      ((n -' k) + 1) >= 1 by NAT_1: 11;

      then 1 in ( dom h) by A4, FINSEQ_3: 25;

      then

       A7: (h . 1) in ( rng h) by FUNCT_1:def 3;

      ( rng h) c= { 0 }

      proof

        let y be object;

        assume y in ( rng h);

        then

        consider x be object such that

         A8: x in ( dom h) & (h . x) = y by FUNCT_1:def 3;

        reconsider x as Nat by A8;

        1 <= x & x <= ( len h) by A8, FINSEQ_3: 25;

        then

        reconsider x1 = (x - 1) as Nat;

        (x1 + 1) = x;

        then

         A9: x1 <= (n -' k) by A8, FINSEQ_3: 25, A4, XREAL_1: 6;

        then

         A10: (h . (x1 + 1)) = (f . (x1 + k)) by A5;

        (n -' k) = (n - k) by A2, XREAL_1: 233;

        then k <= (x1 + k) & (x1 + k) <= ((n -' k) + k) & ((n -' k) + k) = n by A9, XREAL_1: 6, NAT_1: 11;

        then not (x1 + k) in ( dom f) by A6;

        then (f . (x1 + k)) = 0 by FUNCT_1:def 2;

        hence thesis by A10, A8, TARSKI:def 1;

      end;

      then h = (( dom h) --> 0 ) by A7, ZFMISC_1: 33, FUNCOP_1: 9;

      then h = (( len h) |-> 0 ) by FINSEQ_1:def 3;

      hence thesis by RVSUM_1: 81, A3, A1;

    end;

    theorem :: FLEXARY1:11

    

     Th11: ((f,k) +...+ (f,k)) = (f . k)

    proof

      consider h be complex-valued FinSequence such that

       A1: ((f,k) +...+ (f,k)) = ( Sum h) & ( len h) = ((k -' k) + 1) & ((h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((k -' k) + 1)) = (f . ((k -' k) + k))) by Th9;

      ((k -' k) + 1) = ( 0 + 1) by XREAL_1: 232;

      then h = <*(h . 1)*> by A1, FINSEQ_1: 40;

      then ( Sum h) = (h . 1) by RVSUM_2: 30;

      hence thesis by A1;

    end;

    theorem :: FLEXARY1:12

    

     Th12: k <= (n + 1) implies ((f,k) +...+ (f,(n + 1))) = (((f,k) +...+ (f,n)) + (f . (n + 1)))

    proof

      set n1 = (n + 1);

      assume

       A1: k <= n1;

      per cases by A1, NAT_1: 8;

        suppose

         A2: k = n1;

        then k > n by NAT_1: 13;

        then ((f,k) +...+ (f,n)) = 0 & ((f,k) +...+ (f,(n + 1))) = (f . k) by A2, Th11, Def1;

        hence thesis by A2;

      end;

        suppose

         A3: k <= n;

        then

        consider h be complex-valued FinSequence such that

         A4: ((f,k) +...+ (f,n)) = ( Sum h) & ( len h) = ((n -' k) + 1) and

         A5: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) by Th9;

        

         A6: (n1 -' k) = ((n -' k) + 1) by A3, NAT_D: 38;

        set fn = (f . n1);

        reconsider fn as Complex;

        set h1 = (h ^ <*fn*>);

        

         A7: ( len h1) = ((n1 -' k) + 1) by A6, A4, FINSEQ_2: 16;

        (h1 . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h1 . ((n1 -' k) + 1)) = (f . ((n1 -' k) + k))

        proof

          let i;

          set i1 = (i + 1);

          assume

           A8: 0 <= i & i <= (n1 -' k);

          per cases by A8, A6, NAT_1: 8;

            suppose

             A9: i <= (n -' k);

            then 1 <= i1 & i1 <= ( len h) by NAT_1: 11, A4, XREAL_1: 6;

            then i1 in ( dom h) by FINSEQ_3: 25;

            then (h1 . i1) = (h . i1) by FINSEQ_1:def 7;

            hence thesis by A5, A9;

          end;

            suppose

             A10: i = ((n -' k) + 1);

            ((n1 -' k) + k) = ((n1 - k) + k) by NAT_D: 37, A3;

            hence thesis by A10, A4, FINSEQ_1: 42, A6;

          end;

        end;

        

        then ((f,k) +...+ (f,n1)) = ( Sum (h1 | ((n1 -' k) + 1))) by A1, Def1

        .= ( Sum h1) by A7, FINSEQ_1: 58;

        hence thesis by A4, RVSUM_2: 31;

      end;

    end;

    theorem :: FLEXARY1:13

    

     Th13: k <= n implies ((f,k) +...+ (f,n)) = ((f . k) + ((f,(k + 1)) +...+ (f,n)))

    proof

      set k1 = (k + 1);

      assume

       A1: k <= n;

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: k = n;

        then

         A3: (k + 1) > n by NAT_1: 13;

        

        thus ((f,k) +...+ (f,n)) = ((f . k) + 0 ) by A2, Th11

        .= ((f . k) + ((f,(k + 1)) +...+ (f,n))) by A3, Def1;

      end;

        suppose

         A4: k < n;

        then k1 <= n by NAT_1: 13;

        then

        consider h be complex-valued FinSequence such that

         A5: ((f,k1) +...+ (f,n)) = ( Sum h) & ( len h) = ((n -' k1) + 1) and

         A6: (h . ( 0 + 1)) = (f . ( 0 + k1)) & ... & (h . ((n -' k1) + 1)) = (f . ((n -' k1) + k1)) by Th9;

        reconsider fk = (f . k) as Complex;

        set h1 = ( <*fk*> ^ h);

        

         A7: ((n -' k1) + 1) = (n -' k) by A4, NAT_D: 59;

        

         A8: ( len <*fk*>) = 1 by FINSEQ_1: 39;

        then ( len h1) = ((n -' k) + 1) by FINSEQ_1: 22, A7, A5;

        then

         A9: (h1 | ((n -' k) + 1)) = h1 by FINSEQ_1: 58;

        (h1 . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h1 . ((n -' k) + 1)) = (f . ((n -' k) + k))

        proof

          let i;

          set i1 = (i + 1);

          assume

           A10: 0 <= i & i <= (n -' k);

          per cases ;

            suppose i = 0 ;

            hence thesis by FINSEQ_1: 41;

          end;

            suppose

             A11: i > 0 ;

            then

            reconsider ii = (i - 1) as Nat;

            (ii + 1) <= ((n -' k1) + 1) by A4, NAT_D: 59, A10;

            then ii <= (n -' k1) by XREAL_1: 6;

            then

             A12: (h . (ii + 1)) = (f . (ii + k1)) by A6;

            i >= 1 by NAT_1: 14, A11;

            then i in ( dom h) by A5, A7, A10, FINSEQ_3: 25;

            hence thesis by A8, FINSEQ_1:def 7, A12;

          end;

        end;

        

        hence ((f,k) +...+ (f,n)) = ( Sum h1) by Def1, A4, A9

        .= ((f . k) + ((f,(k + 1)) +...+ (f,n))) by RVSUM_2: 33, A5;

      end;

    end;

    theorem :: FLEXARY1:14

    

     Th14: k <= m & m <= n implies (((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n))) = ((f,k) +...+ (f,n))

    proof

      assume

       A1: k <= m & m <= n;

      defpred P[ Nat] means (((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,(m + $1)))) = ((f,k) +...+ (f,(m + $1)));

      

       A2: P[ 0 ]

      proof

        (m + 1) > (m + 0 ) by NAT_1: 13;

        then ((f,(m + 1)) +...+ (f,(m + 0 ))) = 0 by Def1;

        hence thesis;

      end;

      

       A3: P[i] implies P[(i + 1)]

      proof

        assume

         A4: P[i];

        

         A5: (m + 1) <= ((m + 1) + i) by NAT_1: 11;

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

        

        hence ((f,k) +...+ (f,(m + (i + 1)))) = (((f,k) +...+ (f,(m + i))) + (f . ((m + i) + 1))) by A1, XXREAL_0: 2, Th12

        .= (((f,k) +...+ (f,m)) + (((f,(m + 1)) +...+ (f,(m + i))) + (f . ((m + i) + 1)))) by A4

        .= (((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,(m + (i + 1))))) by Th12, A5;

      end;

      

       A6: P[i] from NAT_1:sch 2( A2, A3);

      reconsider nm = (n - m) as Nat by A1, NAT_1: 21;

       P[nm] by A6;

      hence thesis;

    end;

    theorem :: FLEXARY1:15

    

     Th15: k > ( len h) implies ((h,k) +...+ (h,n)) = 0

    proof

      assume

       A1: k > ( len h);

      per cases ;

        suppose k > n;

        hence thesis by Def1;

      end;

        suppose k <= n;

        then

        consider w be complex-valued FinSequence such that

         A2: ((h,k) +...+ (h,n)) = ( Sum w) & ( len w) = ((n -' k) + 1) and

         A3: (w . ( 0 + 1)) = (h . ( 0 + k)) & ... & (w . ((n -' k) + 1)) = (h . ((n -' k) + k)) by Th9;

        set nk = ((n -' k) + 1), nk0 = (nk |-> 0 qua Real);

        now

          let i such that

           A4: 1 <= i & i <= nk;

          reconsider i1 = (i - 1) as Nat by A4;

          (i1 + 1) = i;

          then i1 <= (n -' k) by A4, XREAL_1: 6;

          then

           A5: (w . (i1 + 1)) = (h . (i1 + k)) by A3;

          (i1 + k) > ( 0 + ( len h)) by A1, XREAL_1: 8;

          then not (i1 + k) in ( dom h) by FINSEQ_3: 25;

          hence (w . i) = (nk0 . i) by FUNCT_1:def 2, A5;

        end;

        then w = (nk |-> 0 ) by CARD_1:def 7, A2;

        then ( Sum w) = (nk * 0 ) by RVSUM_1: 80;

        hence thesis by A2;

      end;

    end;

    theorem :: FLEXARY1:16

    

     Th16: n >= ( len h) implies ((h,k) +...+ (h,n)) = ((h,k) +...+ (h,( len h)))

    proof

      assume

       A1: n >= ( len h);

      per cases ;

        suppose k > ( len h);

        then ((h,k) +...+ (h,( len h))) = 0 & ((h,k) +...+ (h,n)) = 0 by Th15;

        hence thesis;

      end;

        suppose

         A2: k <= ( len h);

        defpred P[ Nat] means ((h,k) +...+ (h,(( len h) + $1))) = ((h,k) +...+ (h,( len h)));

        

         A3: P[ 0 ];

        

         A4: P[i] implies P[(i + 1)]

        proof

          set i1 = (i + 1);

          assume

           A5: P[i];

          (( len h) + i1) > (( len h) + 0 ) by XREAL_1: 6;

          then

           A6: not (( len h) + i1) in ( dom h) by FINSEQ_3: 25;

          

           A7: ( len h) <= (( len h) + i1) by NAT_1: 11;

          

           A8: (h . (( len h) + i1)) = 0 by A6, FUNCT_1:def 2;

          ((h,k) +...+ (h,((( len h) + i) + 1))) = (((h,k) +...+ (h,(( len h) + i))) + (h . ((( len h) + i) + 1))) by Th12, A7, XXREAL_0: 2, A2;

          hence thesis by A8, A5;

        end;

        

         A9: P[i] from NAT_1:sch 2( A3, A4);

        reconsider nl = (n - ( len h)) as Nat by A1, NAT_1: 21;

         P[nl] by A9;

        hence thesis;

      end;

    end;

    theorem :: FLEXARY1:17

    

     Th17: ((h, 0 ) +...+ (h,k)) = ((h,1) +...+ (h,k))

    proof

       not 0 in ( dom h) by FINSEQ_3: 25;

      then

       A1: (h . 0 ) = 0 by FUNCT_1:def 2;

      ((h, 0 ) +...+ (h,k)) = ((h . 0 ) + ((h,( 0 + 1)) +...+ (h,k))) by Th13;

      hence thesis by A1;

    end;

    theorem :: FLEXARY1:18

    

     Th18: ((h,1) +...+ (h,( len h))) = ( Sum h)

    proof

      set L = ( len h);

      per cases ;

        suppose

         A1: L >= 1;

        then

        consider w be complex-valued FinSequence such that

         A2: ((h,1) +...+ (h,L)) = ( Sum w) & ( len w) = ((L -' 1) + 1) and

         A3: (w . ( 0 + 1)) = (h . ( 0 + 1)) & ... & (w . ((L -' 1) + 1)) = (h . ((L -' 1) + 1)) by Th9;

        

         A4: ((L -' 1) + 1) = ((L - 1) + 1) by A1, NAT_D: 34;

        now

          let i such that

           A5: 1 <= i & i <= L;

          reconsider i1 = (i - 1) as Nat by A5;

          (w . (i1 + 1)) = (h . (i1 + 1)) by A4, A5, XREAL_1: 6, A3;

          hence (h . i) = (w . i);

        end;

        then h = w by A4, A2;

        hence thesis by A2;

      end;

        suppose L < 1;

        then h = ( <*> REAL ) by FINSEQ_1: 20;

        hence thesis by RVSUM_1: 72, Def1;

      end;

    end;

    

     Lm2: k <= n & n <= ( len g) implies (((g ^ h),k) +...+ ((g ^ h),n)) = ((g,k) +...+ (g,n))

    proof

      set gh = (g ^ h);

      assume

       A1: k <= n & n <= ( len g);

      then

      consider w be complex-valued FinSequence such that

       A2: ((gh,k) +...+ (gh,n)) = ( Sum w) & ( len w) = ((n -' k) + 1) and

       A3: (w . ( 0 + 1)) = (gh . ( 0 + k)) & ... & (w . ((n -' k) + 1)) = (gh . ((n -' k) + k)) by Th9;

      

       A4: ((n -' k) + k) = n & (n -' k) = (n - k) by A1, XREAL_1: 235, XREAL_1: 233;

      

       A5: (w | ((n -' k) + 1)) = w by A2, FINSEQ_1: 58;

      (w . ( 0 + 1)) = (g . ( 0 + k)) & ... & (w . ((n -' k) + 1)) = (g . ((n -' k) + k))

      proof

        let i;

        assume

         A6: 0 <= i & i <= (n -' k);

        then

         A7: (i + k) <= n by A4, XREAL_1: 6;

        per cases ;

          suppose

           A8: (i + k) = 0 ;

          then not (i + k) in ( dom g) & not (i + k) in ( dom gh) by FINSEQ_3: 25;

          then (gh . 0 ) = 0 & (g . 0 ) = 0 by A8, FUNCT_1:def 2;

          hence thesis by A3, A8, A6;

        end;

          suppose (i + k) > 0 ;

          then

           A9: (i + k) >= 1 by NAT_1: 14;

          (i + k) <= ( len g) by A1, A7, XXREAL_0: 2;

          then (i + k) in ( dom g) by A9, FINSEQ_3: 25;

          then (g . (i + k)) = (gh . (i + k)) by FINSEQ_1:def 7;

          hence thesis by A3, A6;

        end;

      end;

      hence thesis by A1, Def1, A5, A2;

    end;

    

     Lm3: k <= n & k > ( len g) implies (((g ^ h),k) +...+ ((g ^ h),n)) = ((h,(k -' ( len g))) +...+ (h,(n -' ( len g))))

    proof

      set gh = (g ^ h);

      assume

       A1: k <= n & k > ( len g);

      then

      consider w be complex-valued FinSequence such that

       A2: ((gh,k) +...+ (gh,n)) = ( Sum w) & ( len w) = ((n -' k) + 1) and

       A3: (w . ( 0 + 1)) = (gh . ( 0 + k)) & ... & (w . ((n -' k) + 1)) = (gh . ((n -' k) + k)) by Th9;

      

       A4: ((n -' k) + k) = n & (n -' k) = (n - k) by A1, XREAL_1: 235, XREAL_1: 233;

      

       A5: (w | ((n -' k) + 1)) = w by A2, FINSEQ_1: 58;

      set kL = (k -' ( len g)), nL = (n -' ( len g));

      

       A6: kL = (k - ( len g)) & nL = (n - ( len g)) by A1, XXREAL_0: 2, XREAL_1: 233;

      

       A7: kL <= nL by A1, NAT_D: 42;

      

       A8: (nL -' kL) = (nL - kL) by A1, NAT_D: 42, XREAL_1: 233;

      (w . ( 0 + 1)) = (h . ( 0 + kL)) & ... & (w . ((nL -' kL) + 1)) = (h . ((nL -' kL) + kL))

      proof

        let i;

        assume

         A9: 0 <= i & i <= (nL -' kL);

        then

         A10: (w . (i + 1)) = (gh . (i + k)) by A8, A6, A4, A3;

        kL <> 0 by A1, A6;

        then

         A11: (kL + i) >= (1 + 0 ) by NAT_1: 14;

        per cases ;

          suppose (kL + i) <= ( len h);

          then (kL + i) in ( dom h) by A11, FINSEQ_3: 25;

          then (h . (kL + i)) = (gh . ((kL + i) + ( len g))) by FINSEQ_1:def 7;

          then (h . (kL + i)) = (gh . (i + k)) by A6;

          hence thesis by A9, A8, A6, A4, A3;

        end;

          suppose

           A12: (kL + i) > ( len h);

          then not (kL + i) in ( dom h) by FINSEQ_3: 25;

          then

           A13: (h . (i + kL)) = 0 by FUNCT_1:def 2;

          ((kL + i) + ( len g)) > (( len h) + ( len g)) by A12, XREAL_1: 6;

          then (i + k) > (( len g) + ( len h)) & ( len gh) = (( len g) + ( len h)) by A6, FINSEQ_1: 22;

          then not (i + k) in ( dom gh) by FINSEQ_3: 25;

          hence thesis by FUNCT_1:def 2, A13, A10;

        end;

      end;

      hence thesis by A8, A6, A4, A5, Def1, A7, A2;

    end;

    theorem :: FLEXARY1:19

    (((g ^ h),k) +...+ ((g ^ h),n)) = (((g,k) +...+ (g,n)) + ((h,(k -' ( len g))) +...+ (h,(n -' ( len g)))))

    proof

      set gh = (g ^ h);

      per cases ;

        suppose

         A1: k > n;

        then

         A2: (((g ^ h),k) +...+ ((g ^ h),n)) = 0 & ((g,k) +...+ (g,n)) = 0 by Def1;

        per cases by XXREAL_0: 1;

          suppose (k -' ( len g)) = (n -' ( len g)) & (k -' ( len g)) = 0 ;

          then

           A3: ((h,(k -' ( len g))) +...+ (h,(n -' ( len g)))) = (h . 0 ) by Th11;

           not 0 in ( dom h) by FINSEQ_3: 25;

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

        end;

          suppose

           A4: (k -' ( len g)) = (n -' ( len g)) & (k -' ( len g)) > 0 ;

          then (k -' ( len g)) = (k - ( len g)) & (n -' ( len g)) = (n - ( len g)) by XREAL_0:def 2;

          hence thesis by A1, A4;

        end;

          suppose (n -' ( len g)) < (k -' ( len g));

          hence thesis by Def1, A2;

        end;

          suppose

           A5: (n -' ( len g)) > (k -' ( len g));

          then (n -' ( len g)) = (n - ( len g)) & (n - ( len g)) > 0 & 0 = (( len g) - ( len g)) by XREAL_0:def 2;

          then n > ( len g) by XREAL_1: 6;

          hence thesis by A5, A1, NAT_D: 56;

        end;

      end;

        suppose

         A6: k <= n;

        set w = the complex-valued FinSequence;

        per cases ;

          suppose

           A7: n <= ( len g);

          then k <= ( len g) by A6, XXREAL_0: 2;

          then (n - ( len g)) <= 0 & (k - ( len g)) <= 0 by A7, XREAL_1: 47;

          then (n -' ( len g)) = 0 & (k -' ( len g)) = 0 by XREAL_0:def 2;

          then

           A8: ((h,(k -' ( len g))) +...+ (h,(n -' ( len g)))) = (h . 0 ) by Th11;

           not 0 in ( dom h) by FINSEQ_3: 25;

          then ((h,(k -' ( len g))) +...+ (h,(n -' ( len g)))) = 0 by FUNCT_1:def 2, A8;

          hence thesis by A7, Lm2, A6;

        end;

          suppose

           A9: k > ( len g);

          then ((g,k) +...+ (g,n)) = 0 by Th15;

          hence thesis by Lm3, A9, A6;

        end;

          suppose

           A10: n > ( len g) & k <= ( len g);

          

          then

           A11: (((g ^ h),k) +...+ ((g ^ h),( len g))) = ((g,k) +...+ (g,( len g))) by Lm2

          .= ((g,k) +...+ (g,n)) by Th16, A10;

          (k - ( len g)) <= (( len g) - ( len g)) by A10, XREAL_1: 7;

          then

           A12: (k -' ( len g)) = 0 by XREAL_0:def 2;

          

           A13: ((( len g) + 1) -' ( len g)) = ((( len g) + 1) - ( len g)) by NAT_D: 37;

          (( len g) + 1) > ( len g) & n >= (( len g) + 1) by A10, NAT_1: 13;

          

          then (((g ^ h),(( len g) + 1)) +...+ ((g ^ h),n)) = ((h,((( len g) + 1) -' ( len g))) +...+ (h,(n -' ( len g)))) by Lm3

          .= ((h,(k -' ( len g))) +...+ (h,(n -' ( len g)))) by A13, Th17, A12;

          hence thesis by A10, Th14, A11;

        end;

      end;

    end;

    registration

      let n, k;

      let f be real-valued FinSequence;

      cluster ((f,k) +...+ (f,n)) -> real;

      coherence

      proof

        per cases ;

          suppose k > n;

          hence thesis by Def1;

        end;

          suppose k <= n;

          then

          consider h such that

           A1: ((f,k) +...+ (f,n)) = ( Sum h) & ( len h) = ((n -' k) + 1) and

           A2: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) by Th9;

          ( rng h) c= REAL

          proof

            let y be object;

            assume y in ( rng h);

            then

            consider x be object such that

             A3: x in ( dom h) & (h . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A3;

            1 <= x & x <= ( len h) by A3, FINSEQ_3: 25;

            then

            reconsider x1 = (x - 1) as Nat;

            (x1 + 1) <= ((n -' k) + 1) by A3, FINSEQ_3: 25, A1;

            then x1 <= (n -' k) by XREAL_1: 6;

            then (h . (x1 + 1)) = (f . (x1 + k)) by A2;

            hence thesis by A3, XREAL_0:def 1;

          end;

          then h is real-valued by VALUED_0:def 3;

          hence thesis by A1;

        end;

      end;

    end

    registration

      let n, k;

      let f be natural-valued FinSequence;

      cluster ((f,k) +...+ (f,n)) -> natural;

      coherence

      proof

        per cases ;

          suppose k > n;

          hence thesis by Def1;

        end;

          suppose k <= n;

          then

          consider h such that

           A1: ((f,k) +...+ (f,n)) = ( Sum h) & ( len h) = ((n -' k) + 1) and

           A2: (h . ( 0 + 1)) = (f . ( 0 + k)) & ... & (h . ((n -' k) + 1)) = (f . ((n -' k) + k)) by Th9;

          ( rng h) c= NAT

          proof

            let y be object;

            assume y in ( rng h);

            then

            consider x be object such that

             A3: x in ( dom h) & (h . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A3;

            1 <= x & x <= ( len h) by A3, FINSEQ_3: 25;

            then

            reconsider x1 = (x - 1) as Nat;

            (x1 + 1) <= ((n -' k) + 1) by A3, FINSEQ_3: 25, A1;

            then x1 <= (n -' k) by XREAL_1: 6;

            then

             A4: (h . (x1 + 1)) = (f . (x1 + k)) by A2;

            per cases ;

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

              then y = 0 by A4, FUNCT_1:def 2, A3;

              hence thesis;

            end;

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

              then (f . (x1 + k)) in ( rng f) & ( rng f) c= NAT by FUNCT_1:def 3, VALUED_0:def 6;

              hence thesis by A3, A4;

            end;

          end;

          then

          reconsider H = h as FinSequence of NAT by FINSEQ_1:def 4;

          ( Sum H) is Element of NAT ;

          hence thesis by A1;

        end;

      end;

    end

    definition

      let n;

      let f be complex-valued Function;

      assume

       A1: (( dom f) /\ NAT ) is finite;

      :: FLEXARY1:def2

      func (f,n) +... -> complex number means

      : Def2: for k st for i st i in ( dom f) holds i <= k holds it = ((f,n) +...+ (f,k));

      existence

      proof

        per cases ;

          suppose

           A2: (( dom f) /\ NAT ) = {} ;

          take 0 ;

          let k such that for i st i in ( dom f) holds i <= k;

          for i st n <= i & i <= k holds not i in ( dom f)

          proof

            let i;

            i in NAT by ORDINAL1:def 12;

            hence thesis by A2, XBOOLE_0:def 4;

          end;

          hence thesis by Th10;

        end;

          suppose (( dom f) /\ NAT ) is non empty;

          then

          reconsider F = (( dom f) /\ NAT ) as non empty finite Subset of NAT by A1;

          reconsider m = ( max F) as Nat by TARSKI: 1;

          take t = ((f,n) +...+ (f,m));

          let k such that

           A3: for i st i in ( dom f) holds i <= k;

          m in F by XXREAL_2:def 8;

          then

          reconsider km = (k - m) as Nat by A3, NAT_1: 21;

          per cases ;

            suppose

             A4: n > m;

            ((f,n) +...+ (f,k)) = 0

            proof

              assume ((f,n) +...+ (f,k)) <> 0 ;

              then

              consider i such that

               A5: n <= i & i <= k & i in ( dom f) by Th10;

              i in NAT by ORDINAL1:def 12;

              then i in F by A5, XBOOLE_0:def 4;

              then i <= m by XXREAL_2:def 8;

              hence thesis by A4, XXREAL_0: 2, A5;

            end;

            hence thesis by A4, Def1;

          end;

            suppose

             A6: n <= m;

            defpred P[ Nat] means t = ((f,n) +...+ (f,(m + $1)));

            

             A7: P[ 0 ];

            

             A8: P[i] implies P[(i + 1)]

            proof

              assume

               A9: P[i];

              

               A10: m < ((m + i) + 1) by NAT_1: 11, NAT_1: 13;

              

              then

               A11: ((f,n) +...+ (f,((m + i) + 1))) = (((f,n) +...+ (f,(m + i))) + (f . ((m + i) + 1))) by A6, XXREAL_0: 2, Th12

              .= (t + (f . ((m + i) + 1))) by A9;

               not ((m + i) + 1) in ( dom f)

              proof

                assume ((m + i) + 1) in ( dom f);

                then ((m + i) + 1) in F by XBOOLE_0:def 4;

                hence thesis by XXREAL_2:def 8, A10;

              end;

              then (f . ((m + i) + 1)) = 0 by FUNCT_1:def 2;

              hence thesis by A11;

            end;

             P[i] from NAT_1:sch 2( A7, A8);

            then P[km];

            hence thesis;

          end;

        end;

      end;

      uniqueness

      proof

        let C1,C2 be complex number such that

         A12: for k st for i st i in ( dom f) holds i <= k holds C1 = ((f,n) +...+ (f,k)) and

         A13: for k st for i st i in ( dom f) holds i <= k holds C2 = ((f,n) +...+ (f,k));

        per cases ;

          suppose (( dom f) /\ NAT ) is non empty;

          then

          reconsider F = (( dom f) /\ NAT ) as non empty finite Subset of NAT by A1;

          reconsider m = ( max F) as Nat by TARSKI: 1;

          

           A14: for i st i in ( dom f) holds i <= m

          proof

            let i;

            assume

             A15: i in ( dom f);

            i in NAT by ORDINAL1:def 12;

            then i in F by A15, XBOOLE_0:def 4;

            hence thesis by XXREAL_2:def 8;

          end;

          

          hence C1 = ((f,n) +...+ (f,m)) by A12

          .= C2 by A14, A13;

        end;

          suppose

           A16: (( dom f) /\ NAT ) is empty;

          

           A17: for i st i in ( dom f) holds i <= 1

          proof

            let i;

            assume

             A18: i in ( dom f);

            i in NAT by ORDINAL1:def 12;

            hence thesis by A18, XBOOLE_0:def 4, A16;

          end;

          

          hence C1 = ((f,n) +...+ (f,1)) by A12

          .= C2 by A17, A13;

        end;

      end;

    end

    definition

      let n, h;

      :: original: +...

      redefine

      :: FLEXARY1:def3

      func (h,n) +... -> complex number equals ((h,n) +...+ (h,( len h)));

      coherence ;

      compatibility

      proof

        let c be complex number;

        

         A1: (( dom h) /\ NAT ) = ( dom h) by XBOOLE_1: 28;

        thus c = ((h,n) +... ) implies c = ((h,n) +...+ (h,( len h)))

        proof

          for i st i in ( dom h) holds i <= ( len h) by FINSEQ_3: 25;

          hence thesis by Def2, A1;

        end;

        assume

         A2: c = ((h,n) +...+ (h,( len h)));

        for k st for i st i in ( dom h) holds i <= k holds c = ((h,n) +...+ (h,k))

        proof

          let k such that

           A3: for i st i in ( dom h) holds i <= k;

          now

            per cases by NAT_1: 14;

              suppose ( len h) = 0 ;

              hence ( len h) <= k;

            end;

              suppose ( len h) >= 1;

              then ( len h) in ( dom h) by FINSEQ_3: 25;

              hence ( len h) <= k by A3;

            end;

          end;

          hence thesis by Th16, A2;

        end;

        hence thesis by A1, Def2;

      end;

    end

    registration

      let n be Nat;

      let h be natural-valued FinSequence;

      cluster ((h,n) +... ) -> natural;

      coherence ;

    end

    theorem :: FLEXARY1:20

    

     Th20: for f be finite complex-valued Function holds ((f . n) + ((f,(n + 1)) +... )) = ((f,n) +... )

    proof

      let f be finite complex-valued Function;

       {n} c= NAT by ORDINAL1:def 12;

      then

      reconsider D = ((( dom f) /\ NAT ) \/ {n}) as finite non empty Subset of NAT by XBOOLE_1: 8;

      reconsider m = ( max D) as Nat by TARSKI: 1;

      

       A1: for i st i in ( dom f) holds i <= m

      proof

        let i;

        assume

         A2: i in ( dom f);

        i in NAT by ORDINAL1:def 12;

        then i in (( dom f) /\ NAT ) by A2, XBOOLE_0:def 4;

        then i in D by XBOOLE_0:def 3;

        hence thesis by XXREAL_2:def 8;

      end;

      then

       A3: ((f,(n + 1)) +... ) = ((f,(n + 1)) +...+ (f,m)) by Def2;

      

       A4: ((f,n) +... ) = ((f,n) +...+ (f,m)) by Def2, A1;

      n in {n} by TARSKI:def 1;

      then n in D by XBOOLE_0:def 3;

      then n <= m by XXREAL_2:def 8;

      hence thesis by Th13, A3, A4;

    end;

    theorem :: FLEXARY1:21

    

     Th21: ( Sum h) = ((h,1) +... ) by Th18;

    theorem :: FLEXARY1:22

    

     Th22: ( Sum h) = ((h . 1) + ((h,2) +... ))

    proof

      ( Sum h) = ((h,1) +... ) by Th18

      .= ((h . 1) + ((h,(1 + 1)) +... )) by Th20;

      hence thesis;

    end;

    scheme :: FLEXARY1:sch1

    TT { f,g() -> complex-valued FinSequence , a,b() -> Nat , n,k() -> non zero Nat } :

((f(),a()) +... ) = ((g(),b()) +... )

      provided

       A1: for j holds ((f(),(a() + (j * n()))) +...+ (f(),((a() + (j * n())) + (n() -' 1)))) = ((g(),(b() + (j * k()))) +...+ (g(),((b() + (j * k())) + (k() -' 1))));

      defpred P[ Nat] means ((f(),a()) +...+ (f(),((a() + ($1 * n())) + (n() -' 1)))) = ((g(),b()) +...+ (g(),((b() + ($1 * k())) + (k() -' 1))));

      

       A2: P[ 0 ] by A1;

      

       A3: P[j] implies P[(j + 1)]

      proof

        set j1 = (j + 1);

        

         A4: (((f(),a()) +...+ (f(),((a() + (j * n())) + (n() -' 1)))) + ((f(),(a() + (j1 * n()))) +...+ (f(),((a() + (j1 * n())) + (n() -' 1))))) = ((f(),a()) +...+ (f(),((a() + (j1 * n())) + (n() -' 1))))

        proof

          

           A5: a() <= (a() + ((j * n()) + (n() -' 1))) by NAT_1: 11;

          ((n() -' 1) + 1) = n() by NAT_1: 14, XREAL_1: 235;

          then

           A6: (((a() + (j * n())) + (n() -' 1)) + 1) = (a() + (j1 * n()));

          (a() + (j1 * n())) <= (a() + ((j1 * n()) + (n() -' 1))) by NAT_1: 11, XREAL_1: 6;

          then ((a() + (j * n())) + (n() -' 1)) <= (a() + ((j1 * n()) + (n() -' 1))) by A6, NAT_1: 13;

          hence thesis by Th14, A5, A6;

        end;

        (((g(),b()) +...+ (g(),((b() + (j * k())) + (k() -' 1)))) + ((g(),(b() + (j1 * k()))) +...+ (g(),((b() + (j1 * k())) + (k() -' 1))))) = ((g(),b()) +...+ (g(),((b() + (j1 * k())) + (k() -' 1))))

        proof

          

           A7: b() <= (b() + ((j * k()) + (k() -' 1))) by NAT_1: 11;

          ((k() -' 1) + 1) = k() by NAT_1: 14, XREAL_1: 235;

          then

           A8: (((b() + (j * k())) + (k() -' 1)) + 1) = (b() + (j1 * k()));

          (b() + (j1 * k())) <= (b() + ((j1 * k()) + (k() -' 1))) by NAT_1: 11, XREAL_1: 6;

          then ((b() + (j * k())) + (k() -' 1)) <= (b() + ((j1 * k()) + (k() -' 1))) by A8, NAT_1: 13;

          hence thesis by Th14, A7, A8;

        end;

        hence thesis by A1, A4;

      end;

      

       A9: P[j] from NAT_1:sch 2( A2, A3);

      per cases ;

        suppose

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

        set l = ( len f());

        (l * 1) <= (l * n()) by NAT_1: 14, XREAL_1: 64;

        then l <= ((l * n()) + (a() + (n() -' 1))) by XREAL_1: 38;

        then

         A11: ((f(),a()) +...+ (f(),((a() + (l * n())) + (n() -' 1)))) = ((f(),a()) +... ) by Th16;

        

         A12: (( len g()) * k()) <= (l * k()) by A10, XREAL_1: 64;

        (( len g()) * 1) <= (( len g()) * k()) by NAT_1: 14, XREAL_1: 64;

        then ( len g()) <= (l * k()) by A12, XXREAL_0: 2;

        then ( len g()) <= ((l * k()) + (b() + (k() -' 1))) by XREAL_1: 38;

        then ((g(),b()) +...+ (g(),((b() + (l * k())) + (k() -' 1)))) = ((g(),b()) +...+ (g(),( len g()))) = ((g(),b()) +... ) by Th16;

        hence thesis by A9, A11;

      end;

        suppose

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

        set l = ( len g());

        (l * 1) <= (l * k()) by NAT_1: 14, XREAL_1: 64;

        then l <= ((l * k()) + (b() + (k() -' 1))) by XREAL_1: 38;

        then

         A14: ((g(),b()) +...+ (g(),((b() + (l * k())) + (k() -' 1)))) = ((g(),b()) +... ) by Th16;

        

         A15: (( len f()) * n()) <= (l * n()) by A13, XREAL_1: 64;

        (( len f()) * 1) <= (( len f()) * n()) by NAT_1: 14, XREAL_1: 64;

        then ( len f()) <= (l * n()) by A15, XXREAL_0: 2;

        then ( len f()) <= ((l * n()) + (a() + (n() -' 1))) by XREAL_1: 38;

        then ((f(),a()) +...+ (f(),((a() + (l * n())) + (n() -' 1)))) = ((f(),a()) +... ) by Th16;

        hence thesis by A9, A14;

      end;

    end;

    begin

    definition

      let r be Real;

      let f be real-valued Function;

      :: FLEXARY1:def4

      func r |^ f -> real-valued Function means

      : Def4: ( dom it ) = ( dom f) & for x st x in ( dom f) holds (it . x) = (r to_power (f . x));

      existence

      proof

        deffunc P( object) = (r to_power (f . $1));

        

         A1: for x st x in ( dom f) holds P(x) in REAL by XREAL_0:def 1;

        consider g be Function of ( dom f), REAL such that

         A2: for x st x in ( dom f) holds (g . x) = P(x) from FUNCT_2:sch 2( A1);

        take g;

        thus thesis by A2, FUNCT_2:def 1;

      end;

      uniqueness

      proof

        let F1,F2 be real-valued Function such that

         A3: ( dom F1) = ( dom f) & for x st x in ( dom f) holds (F1 . x) = (r to_power (f . x)) and

         A4: ( dom F2) = ( dom f) & for x st x in ( dom f) holds (F2 . x) = (r to_power (f . x));

        now

          let x;

          assume

           A5: x in ( dom f);

          

          hence (F1 . x) = (r to_power (f . x)) by A3

          .= (F2 . x) by A4, A5;

        end;

        hence thesis by A3, A4;

      end;

    end

    registration

      let n be Nat;

      let f be natural-valued Function;

      cluster (n |^ f) -> natural-valued;

      coherence

      proof

        now

          let x;

          assume x in ( dom (n |^ f));

          then x in ( dom f) by Def4;

          then ((n |^ f) . x) = (n to_power (f . x)) by Def4;

          hence ((n |^ f) . x) is natural;

        end;

        hence thesis by VALUED_0:def 12;

      end;

    end

    registration

      let r be Real;

      let f be real-valued FinSequence;

      cluster (r |^ f) -> FinSequence-like;

      coherence

      proof

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

        hence thesis by Def4;

      end;

      cluster (r |^ f) -> ( len f) -element;

      coherence

      proof

        ( dom f) = ( dom (r |^ f)) by Def4;

        then ( len f) = ( len (r |^ f)) by FINSEQ_3: 29;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let n be Nat;

      let f be one-to-one natural-valued Function;

      cluster ((2 + n) |^ f) -> one-to-one;

      coherence

      proof

        set n2 = (2 + n), F = (n2 |^ f);

        let x1,x2 be object such that

         A1: x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2);

        

         A2: ( dom F) = ( dom f) by Def4;

        then

         A3: (F . x1) = (n2 to_power (f . x1)) & (F . x2) = (n2 to_power (f . x2)) by A1, Def4;

        ((n + 1) + 1) > ( 0 + 1) by XREAL_1: 8;

        then (f . x1) = (f . x2) by A1, A3, PEPIN: 30;

        hence thesis by A1, A2, FUNCT_1:def 4;

      end;

    end

    theorem :: FLEXARY1:23

    

     Th23: for r,s be Real holds (r |^ <*s*>) = <*(r to_power s)*>

    proof

      let r,s be Real;

      

       A1: ( len <*s*>) = 1 by FINSEQ_1: 39;

      ( dom <*s*>) = ( Seg 1) & ( Seg 1) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then 1 in ( dom <*s*>) & ( <*s*> . 1) = s by FINSEQ_1: 40;

      then ((r |^ <*s*>) . 1) = (r to_power s) by Def4;

      hence thesis by A1, CARD_1:def 7, FINSEQ_1: 40;

    end;

    theorem :: FLEXARY1:24

    

     Th24: for r be Real, f,g be real-valued FinSequence holds (r |^ (f ^ g)) = ((r |^ f) ^ (r |^ g))

    proof

      let r be Real, f,g be real-valued FinSequence;

      set fg = (f ^ g), rf = (r |^ f), rg = (r |^ g);

      

       A1: ( len fg) = (( len f) + ( len g)) & ( len (rf ^ rg)) = (( len rf) + ( len rg)) by FINSEQ_1: 22;

      

       A2: ( len rf) = ( len f) & ( len rg) = ( len g) & ( len (r |^ fg)) = ( len fg) by CARD_1:def 7;

      then

       A3: ( dom f) = ( dom rf) & ( dom g) = ( dom rg) by FINSEQ_3: 29;

      for i st 1 <= i & i <= ( len fg) holds ((r |^ fg) . i) = ((rf ^ rg) . i)

      proof

        let i;

        assume 1 <= i & i <= ( len fg);

        then

         A4: i in ( dom fg) by FINSEQ_3: 25;

        then

         A5: ((r |^ fg) . i) = (r to_power (fg . i)) by Def4;

        per cases by A4, FINSEQ_1: 25;

          suppose

           A6: i in ( dom f);

          then (fg . i) = (f . i) & ((rf ^ rg) . i) = (rf . i) by A3, FINSEQ_1:def 7;

          hence thesis by A6, Def4, A5;

        end;

          suppose ex j st j in ( dom g) & i = (( len f) + j);

          then

          consider j such that

           A7: j in ( dom g) & i = (( len f) + j);

          (fg . i) = (g . j) & ((rf ^ rg) . i) = (rg . j) by A3, A7, A2, FINSEQ_1:def 7;

          hence thesis by A7, Def4, A5;

        end;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: FLEXARY1:25

    for f be real-valued Function, g be Function holds ((2 |^ f) * g) = (2 |^ (f * g))

    proof

      let f be real-valued Function, g be Function;

      set 2f = (2 |^ f), fg = (f * g);

      

       A1: ( dom 2f) = ( dom f) & ( dom (2 |^ fg)) = ( dom fg) by Def4;

      

       A2: ( dom (2f * g)) c= ( dom (2 |^ fg))

      proof

        let x;

        assume x in ( dom (2f * g));

        then x in ( dom g) & (g . x) in ( dom 2f) by FUNCT_1: 11;

        hence thesis by A1, FUNCT_1: 11;

      end;

      ( dom (2 |^ fg)) c= ( dom (2f * g))

      proof

        let x;

        assume x in ( dom (2 |^ fg));

        then x in ( dom g) & (g . x) in ( dom f) by A1, FUNCT_1: 11;

        hence thesis by A1, FUNCT_1: 11;

      end;

      then

       A3: ( dom (2 |^ fg)) = ( dom (2f * g)) by A2;

      for x st x in ( dom (2 |^ fg)) holds ((2f * g) . x) = ((2 |^ fg) . x)

      proof

        let x;

        assume

         A4: x in ( dom (2 |^ fg));

        then x in ( dom g) & (g . x) in ( dom f) by A1, FUNCT_1: 11;

        then ((2f * g) . x) = (2f . (g . x)) & (2f . (g . x)) = (2 to_power (f . (g . x))) & (f . (g . x)) = (fg . x) by Def4, FUNCT_1: 13;

        hence thesis by A4, A1, Def4;

      end;

      hence thesis by A3;

    end;

    

     Lm4: for f,g be natural-valued FinSequence st f is increasing & (f | n) = g holds g is increasing

    proof

      let f,g be natural-valued FinSequence;

      assume

       A1: f is increasing & (f | n) = g;

      then

       A2: ( dom g) c= ( dom f) by RELAT_1: 60;

      for e1,e2 be ExtReal st e1 in ( dom g) & e2 in ( dom g) & e1 < e2 holds (g . e1) < (g . e2)

      proof

        let e1,e2 be ExtReal;

        assume

         A3: e1 in ( dom g) & e2 in ( dom g) & e1 < e2;

        then e1 in ( dom f) & e2 in ( dom f) & (g . e1) = (f . e1) & (g . e2) = (f . e2) by A1, A2, FUNCT_1: 47;

        hence thesis by A3, A1, VALUED_0:def 13;

      end;

      hence thesis by VALUED_0:def 13;

    end;

    

     Lm5: for f1,f2 be natural-valued FinSequence st ( len f1) = (i + 1) & (f1 | i) = f2 holds ( Sum (n |^ f1)) = (( Sum (n |^ f2)) + (n |^ (f1 . (i + 1))))

    proof

      let f1,f2 be natural-valued FinSequence such that

       A1: ( len f1) = (i + 1) & (f1 | i) = f2;

      set i1 = (i + 1);

      f1 = ((f1 | i) ^ <*(f1 . i1)*>) by A1, FINSEQ_3: 55;

      

      then (n |^ f1) = ((n |^ f2) ^ (n |^ <*(f1 . i1)*>)) by Th24, A1

      .= ((n |^ f2) ^ <*(n to_power (f1 . i1))*>) by Th23;

      hence thesis by RVSUM_1: 74;

    end;

    theorem :: FLEXARY1:26

    

     Th26: for f be increasing natural-valued FinSequence st n > 1 holds (((n |^ f) . 1) + (((n |^ f),2) +... )) < (2 * (n |^ (f . ( len f))))

    proof

      defpred P[ Nat] means for f be increasing natural-valued FinSequence st n > 1 & (f . ( len f)) <= $1 & f <> {} holds ( Sum (n |^ f)) < (2 * (n |^ (f . ( len f))));

      

       A1: for f be natural-valued FinSequence st n > 1 & ( len f) = 1 holds ( Sum (n |^ f)) < (2 * (n |^ (f . ( len f))))

      proof

        let f be natural-valued FinSequence;

        assume

         A2: n > 1 & ( len f) = 1;

        then

         A3: 1 in ( dom f) by FINSEQ_3: 25;

        (n to_power (f . 1)) > 0 by A2, NEWTON: 83;

        then (1 * (n to_power (f . 1))) < (2 * (n to_power (f . 1))) by XREAL_1: 68;

        then

         A4: ((n |^ f) . 1) < (2 * (n |^ (f . ( len f)))) by A3, Def4, A2;

        (n |^ f) = <*((n |^ f) . 1)*> by CARD_1:def 7, A2, FINSEQ_1: 40;

        hence thesis by RVSUM_1: 73, A4;

      end;

      

       A5: P[ 0 ]

      proof

        let f be increasing natural-valued FinSequence such that

         A6: n > 1 & (f . ( len f)) <= 0 & f <> {} ;

        ( len f) <= 1

        proof

          assume

           A7: ( len f) > 1;

          then 1 in ( dom f) & ( len f) in ( dom f) by FINSEQ_3: 25;

          then (f . 1) < 0 by A7, VALUED_0:def 13, A6;

          hence thesis;

        end;

        then ( len f) = 1 by NAT_1: 25, A6;

        hence thesis by A6, A1;

      end;

      

       A8: P[i] implies P[(i + 1)]

      proof

        assume

         A9: P[i];

        set i1 = (i + 1);

        let f be increasing natural-valued FinSequence such that

         A10: n > 1 & (f . ( len f)) <= i1 & f <> {} ;

        per cases by A10, NAT_1: 8;

          suppose (f . ( len f)) <= i;

          hence thesis by A10, A9;

        end;

          suppose (f . ( len f)) = i1;

          per cases by A10, NAT_1: 25;

            suppose ( len f) = 1;

            hence thesis by A10, A1;

          end;

            suppose

             A11: ( len f) > 1;

            then

            reconsider l1 = (( len f) - 1) as Nat;

            reconsider f1 = (f | l1) as natural-valued FinSequence;

            (l1 + 1) > 1 by A11;

            then

             A12: l1 >= 1 & (l1 + 1) > l1 by NAT_1: 13;

            then

             A13: l1 in ( dom f) & ( len f) in ( dom f) by A11, FINSEQ_3: 25;

            then (f . l1) < (f . ( len f)) by A12, VALUED_0:def 13;

            then (f . l1) < i1 by A10, XXREAL_0: 2;

            then

             A14: (f . l1) <= i by NAT_1: 13;

            ( len f) = (l1 + 1);

            then

             A15: ( Sum (n |^ f)) = (( Sum (n |^ f1)) + (n |^ (f . ( len f)))) by Lm5;

            

             A16: ( len f1) = l1 by A12, FINSEQ_1: 59;

            

             A17: f1 <> {} by A12, FINSEQ_1: 59;

            l1 in ( Seg l1) by A12;

            then

             A18: (f . l1) = (f1 . l1) by FUNCT_1: 49;

            f1 is increasing by Lm4;

            then

             A19: ( Sum (n |^ f1)) < (2 * (n |^ (f . l1))) by A17, A18, A16, A10, A9, A14;

            (1 + (f . l1)) <= (f . ( len f)) by A13, A12, VALUED_0:def 13, NAT_1: 13;

            then

             A20: (n |^ (1 + (f . l1))) <= (n |^ (f . ( len f))) by PREPOWER: 93, A10;

            n >= (1 + 1) by A10, NAT_1: 13;

            then

             A21: (2 * (n |^ (f . l1))) <= (n * (n |^ (f . l1))) by XREAL_1: 64;

            (n |^ (1 + (f . l1))) = (n * (n |^ (f . l1))) by NEWTON: 6;

            then ( Sum (n |^ f1)) < (n |^ (1 + (f . l1))) by XXREAL_0: 2, A19, A21;

            then ( Sum (n |^ f1)) < (n |^ (f . ( len f))) by XXREAL_0: 2, A20;

            then ( Sum (n |^ f)) < ((n |^ (f . ( len f))) + (n |^ (f . ( len f)))) by A15, XREAL_1: 8;

            hence thesis;

          end;

        end;

      end;

      

       A22: P[i] from NAT_1:sch 2( A5, A8);

      let f be increasing natural-valued FinSequence such that

       A23: n > 1;

      

       A24: ( Sum (n |^ f)) = (((n |^ f) . 1) + (((n |^ f),2) +... )) by Th22;

      per cases ;

        suppose f = {} ;

        then

         A25: ( Sum (n |^ f)) = 0 by RVSUM_1: 72;

        (n |^ (f . ( len f))) > 0 by A23, NEWTON: 83;

        hence thesis by A24, A25;

      end;

        suppose f <> {} ;

        hence thesis by A22, A23, A24;

      end;

    end;

    

     Lm6: for f1,f2 be increasing natural-valued FinSequence st n > 1 & ( Sum (n |^ f1)) > 0 & ( Sum (n |^ f1)) = ( Sum (n |^ f2)) holds (f1 . ( len f1)) <= (f2 . ( len f2))

    proof

      let f1,f2 be increasing natural-valued FinSequence such that

       A1: n > 1 & ( Sum (n |^ f1)) > 0 & ( Sum (n |^ f1)) = ( Sum (n |^ f2));

      

       A2: (((n |^ f1),1) +... ) = ( Sum (n |^ f1)) & ( Sum (n |^ f2)) = (((n |^ f2) . 1) + (((n |^ f2),2) +... )) & (((n |^ f2),1) +... ) = ( Sum (n |^ f2)) by Th21, Th22;

      set l1 = ( len f1);

      set l2 = ( len f2);

      

       A3: f1 <> {} by A1, RVSUM_1: 72;

      assume (f1 . l1) > (f2 . l2);

      then (f1 . l1) >= (1 + (f2 . l2)) by NAT_1: 13;

      then

       A4: (n |^ (f1 . l1)) >= (n |^ (1 + (f2 . l2))) by PREPOWER: 93, A1;

      

       A5: ( Sum (n |^ f1)) < (2 * (n |^ (f2 . l2))) by A1, Th26, A2;

      reconsider L1 = (l1 - 1) as Nat by A3;

      reconsider F1 = (f1 | L1) as natural-valued FinSequence;

      

       A6: (((n |^ F1),1) +... ) = ( Sum (n |^ F1)) by Th21;

      (L1 + 1) = l1;

      then ( Sum (n |^ f1)) = (( Sum (n |^ F1)) + (n |^ (f1 . l1))) by Lm5;

      then ( Sum (n |^ f1)) >= ( 0 + (n |^ (f1 . l1))) by A6, XREAL_1: 6;

      then

       A7: (n |^ (f1 . l1)) < (2 * (n |^ (f2 . l2))) by A5, XXREAL_0: 2;

      n >= (1 + 1) by A1, NAT_1: 13;

      then (2 * (n |^ (f2 . l2))) <= (n * (n |^ (f2 . l2))) by XREAL_1: 64;

      then (2 * (n |^ (f2 . l2))) <= (n |^ (1 + (f2 . l2))) by NEWTON: 6;

      hence thesis by A7, XXREAL_0: 2, A4;

    end;

    theorem :: FLEXARY1:27

    

     Th27: for f1,f2 be increasing natural-valued FinSequence st n > 1 & (((n |^ f1) . 1) + (((n |^ f1),2) +... )) = (((n |^ f2) . 1) + (((n |^ f2),2) +... )) holds f1 = f2

    proof

      

       A1: for f be natural-valued FinSequence st n > 1 & ( Sum (n |^ f)) <= 0 holds f = {}

      proof

        let f be natural-valued FinSequence such that

         A2: n > 1 & ( Sum (n |^ f)) <= 0 ;

        assume f <> {} ;

        then

        consider x such that

         A3: x in ( dom f) by XBOOLE_0:def 1;

        reconsider x as Nat by A3;

        

         A4: for i st i in ( dom (n |^ f)) holds 0 <= ((n |^ f) . i);

        ( dom (n |^ f)) = ( dom f) by Def4;

        then

         A5: 0 >= ((n |^ f) . x) by A4, A2, RVSUM_1: 85, A3;

        (n to_power (f . x)) > 0 by A2, NEWTON: 83;

        hence thesis by A5, A3, Def4;

      end;

      defpred P[ Nat] means for f1,f2 be increasing natural-valued FinSequence st n > 1 & ( Sum (n |^ f1)) <= $1 & ( Sum (n |^ f1)) = ( Sum (n |^ f2)) holds f1 = f2;

      

       A6: P[ 0 ]

      proof

        let f1,f2 be increasing natural-valued FinSequence such that

         A7: n > 1 & ( Sum (n |^ f1)) <= 0 & ( Sum (n |^ f1)) = ( Sum (n |^ f2));

        f1 = {} by A7, A1;

        hence thesis by A7, A1;

      end;

      

       A8: P[i] implies P[(i + 1)]

      proof

        assume

         A9: P[i];

        set i1 = (i + 1);

        let f1,f2 be increasing natural-valued FinSequence such that

         A10: n > 1 & ( Sum (n |^ f1)) <= (i + 1) & ( Sum (n |^ f1)) = ( Sum (n |^ f2));

        

         A11: (((n |^ f1),1) +... ) = ( Sum (n |^ f1)) & ( Sum (n |^ f2)) = (((n |^ f2) . 1) + (((n |^ f2),2) +... )) & (((n |^ f2),1) +... ) = ( Sum (n |^ f2)) by Th21, Th22;

        per cases by A11, A10, NAT_1: 8;

          suppose ( Sum (n |^ f1)) <= i;

          hence thesis by A10, A9;

        end;

          suppose

           A12: ( Sum (n |^ f1)) = i1;

          set l1 = ( len f1);

          set l2 = ( len f2);

          

           A13: f1 <> {} by A12, RVSUM_1: 72;

          

           A14: f2 <> {} by A10, A12, RVSUM_1: 72;

          

           A15: (f1 . l1) <= (f2 . l2) by Lm6, A10, A12;

          

           A16: (f1 . l1) >= (f2 . l2) by Lm6, A10, A12;

          then

           A17: (f1 . l1) = (f2 . l2) by A15, XXREAL_0: 1;

          reconsider L1 = (l1 - 1), L2 = (l2 - 1) as Nat by A14, A13;

          reconsider F1 = (f1 | L1), F2 = (f2 | L2) as increasing natural-valued FinSequence by Lm4;

          

           A18: (n |^ (f2 . l2)) = (n |^ (f1 . l1)) by A16, A15, XXREAL_0: 1;

          

           A19: l1 = (L1 + 1) & l2 = (L2 + 1);

          then

           A20: ( Sum (n |^ f1)) = (( Sum (n |^ F1)) + (n |^ (f1 . l1))) & ( Sum (n |^ f2)) = (( Sum (n |^ F2)) + (n |^ (f2 . l2))) by Lm5;

          

           A21: (((n |^ F1),1) +... ) = ( Sum (n |^ F1)) by Th21;

          (n |^ (f1 . l1)) > 0 by PREPOWER: 6, A10;

          then (( Sum (n |^ F1)) + 0 ) < ( Sum (n |^ f1)) by A20, XREAL_1: 8;

          then

           A22: ( Sum (n |^ F1)) <= i by A21, A12, NAT_1: 13;

          f1 = (F1 ^ <*(f1 . l1)*>) & f2 = (F2 ^ <*(f2 . l2)*>) by A19, FINSEQ_3: 55;

          hence thesis by A17, A22, A10, A20, A18, A9;

        end;

      end;

      

       A23: P[i] from NAT_1:sch 2( A6, A8);

      let f1,f2 be increasing natural-valued FinSequence;

      

       A24: (((n |^ f1) . 1) + (((n |^ f1),2) +... )) = ( Sum (n |^ f1)) by Th22;

      (((n |^ f2) . 1) + (((n |^ f2),2) +... )) = ( Sum (n |^ f2)) by Th22;

      hence thesis by A23, A24;

    end;

    theorem :: FLEXARY1:28

    

     Th28: for f be natural-valued Function st n > 1 holds ( Coim ((n |^ f),(n |^ k))) = ( Coim (f,k))

    proof

      let f be natural-valued Function such that

       A1: n > 1;

      thus ( Coim ((n |^ f),(n |^ k))) c= ( Coim (f,k))

      proof

        let x be object;

        assume x in ( Coim ((n |^ f),(n |^ k)));

        then x in ((n |^ f) " {(n |^ k)}) by RELAT_1:def 17;

        then x in ( dom (n |^ f)) & ((n |^ f) . x) in {(n |^ k)} by FUNCT_1:def 7;

        then

         A2: x in ( dom f) & ((n |^ f) . x) = (n |^ k) by TARSKI:def 1, Def4;

        

        then ((n |^ f) . x) = (n to_power (f . x)) by Def4

        .= (n |^ (f . x));

        then k = (f . x) by A2, A1, PEPIN: 30;

        then (f . x) in {k} by TARSKI:def 1;

        then x in (f " {k}) by A2, FUNCT_1:def 7;

        hence thesis by RELAT_1:def 17;

      end;

      let x be object;

      assume x in ( Coim (f,k));

      then x in (f " {k}) by RELAT_1:def 17;

      then

       A3: x in ( dom f) & (f . x) in {k} by FUNCT_1:def 7;

      then

       A4: (f . x) = k & x in ( dom (n |^ f)) by TARSKI:def 1, Def4;

      

      then ((n |^ f) . x) = (n to_power k) by Def4, A3

      .= (n |^ k);

      then ((n |^ f) . x) in {(n |^ k)} by TARSKI:def 1;

      then x in ((n |^ f) " {(n |^ k)}) by FUNCT_1:def 7, A4;

      hence thesis by RELAT_1:def 17;

    end;

    theorem :: FLEXARY1:29

    

     Th29: for f1,f2 be natural-valued Function st n > 1 holds (f1,f2) are_fiberwise_equipotent iff ((n |^ f1),(n |^ f2)) are_fiberwise_equipotent

    proof

      let f1,f2 be natural-valued Function such that

       A1: n > 1;

      set n1 = (n |^ f1), n2 = (n |^ f2);

      thus (f1,f2) are_fiberwise_equipotent implies ((n |^ f1),(n |^ f2)) are_fiberwise_equipotent

      proof

        assume

         A2: (f1,f2) are_fiberwise_equipotent ;

        for x be object holds ( card ( Coim (n1,x))) = ( card ( Coim (n2,x)))

        proof

          let x be object;

          

           A3: ( Coim (n1,x)) = (n1 " {x}) & ( Coim (n2,x)) = (n2 " {x}) by RELAT_1:def 17;

          

           A4: ( dom n1) = ( dom f1) & ( dom n2) = ( dom f2) by Def4;

          per cases ;

            suppose not x in ( rng n1) & not x in ( rng n2);

            then (n1 " {x}) = {} & (n2 " {x}) = {} by FUNCT_1: 72;

            hence thesis by A3;

          end;

            suppose

             A5: x in ( rng n1) & not x in ( rng n2);

            then

            consider y be object such that

             A6: y in ( dom n1) & (n1 . y) = x by FUNCT_1:def 3;

            

             A7: x = (n to_power (f1 . y)) by A6, A4, Def4;

            (f1 . y) in ( rng f1) by A6, A4, FUNCT_1:def 3;

            then (f1 " {(f1 . y)}) <> {} by FUNCT_1: 72;

            then

             A8: ( Coim (f1,(f1 . y))) <> {} by RELAT_1:def 17;

            ( card ( Coim (f1,(f1 . y)))) = ( card ( Coim (f2,(f1 . y)))) by A2, CLASSES1:def 10;

            then ( Coim (f2,(f1 . y))) <> {} by A8;

            then (f2 " {(f1 . y)}) <> {} by RELAT_1:def 17;

            then (f1 . y) in ( rng f2) by FUNCT_1: 72;

            then

            consider z be object such that

             A9: z in ( dom f2) & (f2 . z) = (f1 . y) by FUNCT_1:def 3;

            

             A10: z in ( dom n2) by A9, Def4;

            (n2 . z) = x by A9, Def4, A7;

            hence thesis by A10, FUNCT_1:def 3, A5;

          end;

            suppose

             A11: x in ( rng n2) & not x in ( rng n1);

            then

            consider y be object such that

             A12: y in ( dom n2) & (n2 . y) = x by FUNCT_1:def 3;

            

             A13: x = (n to_power (f2 . y)) by A12, A4, Def4;

            (f2 . y) in ( rng f2) by A12, A4, FUNCT_1:def 3;

            then (f2 " {(f2 . y)}) <> {} by FUNCT_1: 72;

            then

             A14: ( Coim (f2,(f2 . y))) <> {} by RELAT_1:def 17;

            ( card ( Coim (f2,(f2 . y)))) = ( card ( Coim (f1,(f2 . y)))) by A2, CLASSES1:def 10;

            then ( Coim (f1,(f2 . y))) <> {} by A14;

            then (f1 " {(f2 . y)}) <> {} by RELAT_1:def 17;

            then (f2 . y) in ( rng f1) by FUNCT_1: 72;

            then

            consider z be object such that

             A15: z in ( dom f1) & (f1 . z) = (f2 . y) by FUNCT_1:def 3;

            

             A16: z in ( dom n1) by A15, Def4;

            (n1 . z) = x by A15, Def4, A13;

            hence thesis by A16, FUNCT_1:def 3, A11;

          end;

            suppose

             A17: x in ( rng n1) & x in ( rng n2);

            then

            consider y1 be object such that

             A18: y1 in ( dom n1) & (n1 . y1) = x by FUNCT_1:def 3;

            

             A19: x = (n to_power (f1 . y1)) by A18, A4, Def4;

            consider y2 be object such that

             A20: y2 in ( dom n2) & (n2 . y2) = x by A17, FUNCT_1:def 3;

            

             A21: x = (n to_power (f2 . y2)) by A20, A4, Def4;

            then

             A22: (f2 . y2) = (f1 . y1) by A19, A1, PEPIN: 30;

            

             A23: ( Coim (f2,(f2 . y2))) = ( Coim (n2,x)) by A1, Th28, A21;

            ( Coim (f1,(f1 . y1))) = ( Coim (n1,x)) by A1, Th28, A19;

            hence thesis by A22, A2, CLASSES1:def 10, A23;

          end;

        end;

        hence thesis by CLASSES1:def 10;

      end;

      assume

       A24: ((n |^ f1),(n |^ f2)) are_fiberwise_equipotent ;

      for x be object holds ( card ( Coim (f1,x))) = ( card ( Coim (f2,x)))

      proof

        let x be object;

        

         A25: ( Coim (f1,x)) = (f1 " {x}) & ( Coim (f2,x)) = (f2 " {x}) by RELAT_1:def 17;

        

         A26: ( dom n1) = ( dom f1) & ( dom n2) = ( dom f2) by Def4;

        per cases ;

          suppose not x in ( rng f1) & not x in ( rng f2);

          then (f1 " {x}) = {} & (f2 " {x}) = {} by FUNCT_1: 72;

          hence thesis by A25;

        end;

          suppose

           A27: x in ( rng f1) & not x in ( rng f2);

          then

          consider y be object such that

           A28: y in ( dom f1) & (f1 . y) = x by FUNCT_1:def 3;

          (n1 . y) in ( rng n1) by A26, A28, FUNCT_1:def 3;

          then (n1 " {(n1 . y)}) <> {} by FUNCT_1: 72;

          then

           A29: ( Coim (n1,(n1 . y))) <> {} by RELAT_1:def 17;

          ( card ( Coim (n1,(n1 . y)))) = ( card ( Coim (n2,(n1 . y)))) by A24, CLASSES1:def 10;

          then ( Coim (n2,(n1 . y))) <> {} by A29;

          then (n2 " {(n1 . y)}) <> {} by RELAT_1:def 17;

          then (n1 . y) in ( rng n2) by FUNCT_1: 72;

          then

          consider z be object such that

           A30: z in ( dom n2) & (n2 . z) = (n1 . y) by FUNCT_1:def 3;

          (n2 . z) = (n to_power (f2 . z)) & (n1 . y) = (n to_power (f1 . y)) by A28, A30, A26, Def4;

          then (f2 . z) = (f1 . y) by A30, A1, PEPIN: 30;

          hence thesis by A30, A26, A28, FUNCT_1:def 3, A27;

        end;

          suppose

           A31: x in ( rng f2) & not x in ( rng f1);

          then

          consider y be object such that

           A32: y in ( dom f2) & (f2 . y) = x by FUNCT_1:def 3;

          (n2 . y) in ( rng n2) by A26, A32, FUNCT_1:def 3;

          then (n2 " {(n2 . y)}) <> {} by FUNCT_1: 72;

          then

           A33: ( Coim (n2,(n2 . y))) <> {} by RELAT_1:def 17;

          ( card ( Coim (n2,(n2 . y)))) = ( card ( Coim (n1,(n2 . y)))) by A24, CLASSES1:def 10;

          then ( Coim (n1,(n2 . y))) <> {} by A33;

          then (n1 " {(n2 . y)}) <> {} by RELAT_1:def 17;

          then (n2 . y) in ( rng n1) by FUNCT_1: 72;

          then

          consider z be object such that

           A34: z in ( dom n1) & (n1 . z) = (n2 . y) by FUNCT_1:def 3;

          (n1 . z) = (n to_power (f1 . z)) & (n2 . y) = (n to_power (f2 . y)) by A32, A34, A26, Def4;

          then (f1 . z) = (f2 . y) by A34, A1, PEPIN: 30;

          hence thesis by A34, A26, A32, FUNCT_1:def 3, A31;

        end;

          suppose

           A35: x in ( rng f1) & x in ( rng f2);

          then

          consider y1 be object such that

           A36: y1 in ( dom f1) & (f1 . y1) = x by FUNCT_1:def 3;

          

           A37: (n1 . y1) = (n to_power (f1 . y1)) by A36, Def4;

          consider y2 be object such that

           A38: y2 in ( dom f2) & (f2 . y2) = x by A35, FUNCT_1:def 3;

          

           A39: (n2 . y2) = (n to_power (f2 . y2)) by A38, Def4;

          then

           A40: ( card ( Coim (n2,(n2 . y2)))) = ( card ( Coim (n1,(n1 . y1)))) by A37, A38, A36, A24, CLASSES1:def 10;

          ( Coim (f2,(f2 . y2))) = ( Coim (n2,(n2 . y2))) by A1, Th28, A39;

          hence thesis by A1, Th28, A37, A40, A36, A38;

        end;

      end;

      hence thesis by CLASSES1:def 10;

    end;

    theorem :: FLEXARY1:30

    for f1,f2 be one-to-one natural-valued FinSequence st n > 1 & (((n |^ f1) . 1) + (((n |^ f1),2) +... )) = (((n |^ f2) . 1) + (((n |^ f2),2) +... )) holds ( rng f1) = ( rng f2)

    proof

      let f1,f2 be one-to-one natural-valued FinSequence such that

       A1: n > 1 & (((n |^ f1) . 1) + (((n |^ f1),2) +... )) = (((n |^ f2) . 1) + (((n |^ f2),2) +... ));

      

       A2: ( rng f1) c= NAT & ( rng f2) c= NAT by VALUED_0:def 6;

      then

      reconsider F1 = f1, F2 = f2 as FinSequence of REAL by FINSEQ_1:def 4;

      set s1 = ( sort_a F1), s2 = ( sort_a F2);

      

       A3: (F1,s1) are_fiberwise_equipotent & (F2,s2) are_fiberwise_equipotent by RFINSEQ2:def 6;

      

       A4: ( rng s1) = ( rng f1) by RFINSEQ2:def 6, CLASSES1: 75;

      then

       A5: s1 is natural-valued by A2, VALUED_0:def 6;

      ( rng (n |^ F1)) c= REAL ;

      then

       A6: (n |^ F1) is FinSequence of REAL by FINSEQ_1:def 4;

      ( rng (n |^ s1)) c= REAL ;

      then

       A7: (n |^ s1) is FinSequence of REAL by FINSEQ_1:def 4;

      ((n |^ F1),(n |^ s1)) are_fiberwise_equipotent by A3, A1, A5, Th29;

      then

       A8: ( Sum (n |^ F1)) = ( Sum (n |^ s1)) by A6, A7, RFINSEQ: 9;

      

       A9: ( rng s2) = ( rng f2) by RFINSEQ2:def 6, CLASSES1: 75;

      then

       A10: s2 is natural-valued by A2, VALUED_0:def 6;

      ( rng (n |^ F2)) c= REAL ;

      then

       A11: (n |^ F2) is FinSequence of REAL by FINSEQ_1:def 4;

      

       A12: s2 is natural-valued by A9, A2, VALUED_0:def 6;

      ( rng (n |^ s2)) c= REAL ;

      then

       A13: (n |^ s2) is FinSequence of REAL by FINSEQ_1:def 4;

      ((n |^ F2),(n |^ s2)) are_fiberwise_equipotent by A10, A3, A1, Th29;

      then

       A14: ( Sum (n |^ F2)) = ( Sum (n |^ s2)) by A11, A13, RFINSEQ: 9;

      

       A15: for e1,e2 be ExtReal st e1 in ( dom s1) & e2 in ( dom s1) & e1 < e2 holds (s1 . e1) < (s1 . e2)

      proof

        let e1,e2 be ExtReal;

        assume

         A16: e1 in ( dom s1) & e2 in ( dom s1) & e1 < e2;

        then

         A17: (s1 . e1) <= (s1 . e2) by INTEGRA2: 2;

        assume

         A18: (s1 . e1) >= (s1 . e2);

        consider H be Function such that

         A19: ( dom H) = ( dom s1) & ( rng H) = ( dom F1) & H is one-to-one & s1 = (F1 * H) by A3, CLASSES1: 77;

        s1 is one-to-one by A19;

        hence thesis by A18, A17, XXREAL_0: 1, A16;

      end;

      for e1,e2 be ExtReal st e1 in ( dom s2) & e2 in ( dom s2) & e1 < e2 holds (s2 . e1) < (s2 . e2)

      proof

        let e1,e2 be ExtReal;

        assume

         A20: e1 in ( dom s2) & e2 in ( dom s2) & e1 < e2;

        then

         A21: (s2 . e1) <= (s2 . e2) by INTEGRA2: 2;

        assume

         A22: (s2 . e1) >= (s2 . e2);

        consider H be Function such that

         A23: ( dom H) = ( dom s2) & ( rng H) = ( dom F2) & H is one-to-one & s2 = (F2 * H) by A3, CLASSES1: 77;

        s2 is one-to-one by A23;

        hence thesis by A22, A21, XXREAL_0: 1, A20;

      end;

      then

       A24: s2 is increasing by VALUED_0:def 13;

      

       A25: ( Sum (n |^ s1)) = (((n |^ s1) . 1) + (((n |^ s1),2) +... )) by Th22;

      ( Sum (n |^ f1)) = (((n |^ f1) . 1) + (((n |^ f1),2) +... )) by Th22;

      then ( Sum (n |^ s1)) = ( Sum (n |^ s2)) by Th22, A1, A8, A14;

      then (((n |^ s1) . 1) + (((n |^ s1),2) +... )) = (((n |^ s2) . 1) + (((n |^ s2),2) +... )) & s1 is increasing natural-valued by A15, VALUED_0:def 13, A25, Th22, A4, A2, VALUED_0:def 6;

      hence thesis by A1, A12, A24, Th27, A9, A4;

    end;

    theorem :: FLEXARY1:31

    ex f be increasing natural-valued FinSequence st n = (((2 |^ f) . 1) + (((2 |^ f),2) +... ))

    proof

      set D = ( digits (n,2));

      consider d be XFinSequence of NAT such that

       A1: (( dom d) = ( dom D) & for i be Nat st i in ( dom d) holds (d . i) = ((D . i) * (2 |^ i))) & ( value (D,2)) = ( Sum d) by NUMERAL1:def 1;

      defpred P[ Nat] means $1 <= ( len d) implies ex f be increasing natural-valued FinSequence st (( len f) = 0 or (f . ( len f)) < $1) & ( Sum (2 |^ f)) = ( Sum (d | $1));

      

       A2: P[ 0 qua Nat]

      proof

        assume 0 <= ( len d);

        reconsider f = ( <*> NAT ) as increasing natural-valued FinSequence;

        take f;

        ( Sum (2 |^ f)) = 0 by RVSUM_1: 72;

        hence thesis;

      end;

      

       A3: P[i] implies P[(i + 1)]

      proof

        assume

         A4: P[i];

        set i1 = (i + 1);

        assume

         A5: i1 <= ( len d);

        then

        consider f be increasing natural-valued FinSequence such that

         A6: (( len f) = 0 or (f . ( len f)) < i) & ( Sum (2 |^ f)) = ( Sum (d | i)) by NAT_1: 13, A4;

        

         A7: i in ( dom d) by A5, NAT_1: 13, AFINSQ_1: 86;

        then

         A8: ( Sum (d | i1)) = (( Sum (d | i)) + (d . i)) & (d . i) = ((D . i) * (2 |^ i)) by A1, AFINSQ_2: 65;

        

         A9: (D . i) = 0 or (D . i) = 1

        proof

          per cases ;

            suppose n = 0 ;

            then

             A10: D = <% 0 %> by NUMERAL1:def 2;

            then ( dom D) = 1 & 1 = ( Segm 1) by AFINSQ_1:def 4, ORDINAL1:def 17;

            then i < 1 by A5, NAT_1: 13, A1;

            then i = 0 by NAT_1: 25;

            hence thesis by A10;

          end;

            suppose n <> 0 ;

            then 0 <= (D . i) & (D . i) < 2 by A7, A1, NUMERAL1:def 2;

            hence thesis by NAT_1: 23;

          end;

        end;

        per cases by A9;

          suppose

           A11: (D . i) = 0 ;

          take f;

          thus thesis by A11, A8, A6, NAT_1: 13;

        end;

          suppose

           A12: (D . i) = 1;

          set fi = (f ^ <*i*>);

          

           A13: ( len fi) = (( len f) + 1) by FINSEQ_2: 16;

          for e1,e2 be ExtReal st e1 in ( dom fi) & e2 in ( dom fi) & e1 < e2 holds (fi . e1) < (fi . e2)

          proof

            let e1,e2 be ExtReal such that

             A14: e1 in ( dom fi) & e2 in ( dom fi) & e1 < e2;

            

             A15: 1 <= e1 & 1 <= e2 & e1 <= (( len f) + 1) & e2 <= (( len f) + 1) by A14, A13, FINSEQ_3: 25;

            per cases ;

              suppose e1 <= ( len f) & e2 <= ( len f);

              then e1 in ( dom f) & e2 in ( dom f) by A15, A14, FINSEQ_3: 25;

              then (f . e1) < (f . e2) & (f . e1) = (fi . e1) & (f . e2) = (fi . e2) by A14, VALUED_0:def 13, FINSEQ_1:def 7;

              hence thesis;

            end;

              suppose

               A16: e1 <= ( len f) & e2 > ( len f);

              then e2 >= (( len f) + 1) by A14, NAT_1: 13;

              then e2 = (( len f) + 1) by A15, XXREAL_0: 1;

              then

               A17: (fi . e2) = i by FINSEQ_1: 42;

              

               A18: e1 = ( len f) or e1 < ( len f) by A16, XXREAL_0: 1;

              ( len f) >= 1 by A16, A15, XXREAL_0: 2;

              then

               A19: (f . ( len f)) < i & ( len f) in ( dom f) & e1 in ( dom f) by A14, A15, A16, A6, FINSEQ_3: 25;

              then (f . e1) <= (f . ( len f)) by A18, VALUED_0:def 13;

              then (f . e1) < i by A16, A14, FINSEQ_3: 25, XXREAL_0: 2, A6;

              hence thesis by A19, FINSEQ_1:def 7, A17;

            end;

              suppose e1 > ( len f) & e2 <= ( len f);

              hence thesis by A14, XXREAL_0: 2;

            end;

              suppose e1 > ( len f) & e2 > ( len f);

              then e1 >= (( len f) + 1) & e2 >= (( len f) + 1) by A14, NAT_1: 13;

              hence thesis by A15, A14, XXREAL_0: 1;

            end;

          end;

          then

          reconsider fi as increasing natural-valued FinSequence by VALUED_0:def 13;

          take fi;

          (fi . ( len fi)) = i & i < i1 by A13, NAT_1: 13, FINSEQ_1: 42;

          hence ( len fi) = 0 or (fi . ( len fi)) < (i + 1);

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

          then (fi | ( len f)) = f by FINSEQ_1: 21;

          then ( Sum (2 |^ fi)) = (( Sum (2 |^ f)) + (2 |^ (fi . (( len f) + 1)))) by FINSEQ_2: 16, Lm5;

          hence thesis by FINSEQ_1: 42, A12, A8, A6;

        end;

      end;

       P[i] from NAT_1:sch 2( A2, A3);

      then

      consider f be increasing natural-valued FinSequence such that ( len f) = 0 or (f . ( len f)) < ( len d) and

       A20: ( Sum (2 |^ f)) = ( Sum (d | ( len d)));

      

       A21: ( Sum (2 |^ f)) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) by Th22;

      ( Sum d) = n by A1, NUMERAL1: 5;

      hence thesis by A20, A21;

    end;

    begin

    definition

      let o be Function-yielding Function;

      let x,y be object;

      :: FLEXARY1:def5

      func o _ (x,y) -> set equals ((o . x) . y);

      coherence ;

    end

    definition

      let F be Function-yielding Function;

      :: FLEXARY1:def6

      attr F is double-one-to-one means

      : Def6: for x1,x2,y1,y2 be object st x1 in ( dom F) & y1 in ( dom (F . x1)) & x2 in ( dom F) & y2 in ( dom (F . x2)) & (F _ (x1,y1)) = (F _ (x2,y2)) holds x1 = x2 & y1 = y2;

    end

    registration

      let D be set;

      cluster empty -> double-one-to-one for FinSequence of (D * );

      coherence ;

    end

    registration

      cluster double-one-to-one for Function-yielding Function;

      existence

      proof

        take the empty FinSequence of ( the set * );

        thus thesis;

      end;

      let D be set;

      cluster double-one-to-one for FinSequence of (D * );

      existence

      proof

        take the empty FinSequence of (D * );

        thus thesis;

      end;

    end

    registration

      let F be double-one-to-one Function-yielding Function;

      let x be object;

      cluster (F . x) -> one-to-one;

      coherence

      proof

        per cases ;

          suppose

           A1: x in ( dom F);

          let x1,x2 be object;

          assume

           A2: x1 in ( dom (F . x)) & x2 in ( dom (F . x)) & ((F . x) . x1) = ((F . x) . x2);

          then (F _ (x,x1)) = (F _ (x,x2));

          hence thesis by A2, A1, Def6;

        end;

          suppose not x in ( dom F);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let F be one-to-one Function;

      cluster <*F*> -> double-one-to-one;

      coherence

      proof

        set FF = <*F*>;

        let x1,x2,y1,y2 be object such that

         A1: x1 in ( dom FF) & y1 in ( dom (FF . x1)) & x2 in ( dom FF) & y2 in ( dom (FF . x2)) & (FF _ (x1,y1)) = (FF _ (x2,y2));

        ( dom FF) = ( Seg 1) & ( Seg 1) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then x1 = 1 & x2 = 1 & (FF . 1) = F by A1, TARSKI:def 1, FINSEQ_1: 40;

        hence thesis by A1, FUNCT_1:def 4;

      end;

    end

    theorem :: FLEXARY1:32

    for f be Function-yielding Function holds f is double-one-to-one iff (for x holds (f . x) is one-to-one) & for x, y st x <> y holds ( rng (f . x)) misses ( rng (f . y))

    proof

      let f be Function-yielding Function;

      thus f is double-one-to-one implies (for x holds (f . x) is one-to-one) & for x, y st x <> y holds ( rng (f . x)) misses ( rng (f . y))

      proof

        assume

         A1: f is double-one-to-one;

        hence for x holds (f . x) is one-to-one;

        let x, y;

        assume

         A2: x <> y;

        assume ( rng (f . x)) meets ( rng (f . y));

        then

        consider z be object such that

         A3: z in ( rng (f . x)) & z in ( rng (f . y)) by XBOOLE_0: 3;

        consider w1 be object such that

         A4: w1 in ( dom (f . x)) & ((f . x) . w1) = z by A3, FUNCT_1:def 3;

        consider w2 be object such that

         A5: w2 in ( dom (f . y)) & ((f . y) . w2) = z by A3, FUNCT_1:def 3;

        

         A6: (f _ (x,w1)) = (f _ (y,w2)) by A4, A5;

        

         A7: x in ( dom f)

        proof

          assume not x in ( dom f);

          then (f . x) = {} by FUNCT_1:def 2;

          hence thesis by A4;

        end;

        y in ( dom f)

        proof

          assume not y in ( dom f);

          then (f . y) = {} by FUNCT_1:def 2;

          hence thesis by A5;

        end;

        hence thesis by A4, A5, A1, A6, A7, A2;

      end;

      assume that

       A8: for x holds (f . x) is one-to-one and

       A9: for x, y st x <> y holds ( rng (f . x)) misses ( rng (f . y));

      let x1,x2,y1,y2 be object such that

       A10: x1 in ( dom f) & y1 in ( dom (f . x1)) & x2 in ( dom f) & y2 in ( dom (f . x2)) & (f _ (x1,y1)) = (f _ (x2,y2));

      

       A11: ((f . x1) . y1) in ( rng (f . x1)) by A10, FUNCT_1:def 3;

      ((f . x2) . y2) in ( rng (f . x2)) by A10, FUNCT_1:def 3;

      then x1 = x2 & ((f . x1) . y1) = ((f . x2) . y2) & (f . x1) is one-to-one by A11, A10, XBOOLE_0: 3, A8, A9;

      hence thesis by A10;

    end;

    theorem :: FLEXARY1:33

    

     Th33: for D be set holds for f1,f2 be double-one-to-one FinSequence of (D * ) st ( Values f1) misses ( Values f2) holds (f1 ^ f2) is double-one-to-one

    proof

      let D be set;

      let f1,f2 be double-one-to-one FinSequence of (D * ) such that

       A1: ( Values f1) misses ( Values f2);

      set F = (f1 ^ f2);

      let x1,x2,y1,y2 be object such that

       A2: x1 in ( dom F) & y1 in ( dom (F . x1)) & x2 in ( dom F) & y2 in ( dom (F . x2)) & (F _ (x1,y1)) = (F _ (x2,y2));

      reconsider x1, x2 as Nat by A2;

      per cases ;

        suppose

         A3: x1 in ( dom f1) & x2 in ( dom f1);

        then

         A4: (F . x1) = (f1 . x1) & (F . x2) = (f1 . x2) by FINSEQ_1:def 7;

        then (f1 _ (x1,y1)) = (f1 _ (x2,y2)) by A2;

        hence thesis by A2, A3, Def6, A4;

      end;

        suppose

         A5: x1 in ( dom f1) & not x2 in ( dom f1);

        then

        consider n such that

         A6: n in ( dom f2) & x2 = (( len f1) + n) by A2, FINSEQ_1: 25;

        (F . x2) = (f2 . n) & (F . x1) = (f1 . x1) by A5, A6, FINSEQ_1:def 7;

        then ((F . x2) . y2) in ( Values f2) & ((F . x2) . y2) in ( Values f1) by A2, A5, A6, Th1;

        hence thesis by A1, XBOOLE_0: 3;

      end;

        suppose

         A7: not x1 in ( dom f1) & x2 in ( dom f1);

        then

        consider n such that

         A8: n in ( dom f2) & x1 = (( len f1) + n) by A2, FINSEQ_1: 25;

        (F . x1) = (f2 . n) & (F . x2) = (f1 . x2) by A7, A8, FINSEQ_1:def 7;

        then ((F . x2) . y2) in ( Values f1) & ((F . x2) . y2) in ( Values f2) by A2, A7, A8, Th1;

        hence thesis by A1, XBOOLE_0: 3;

      end;

        suppose

         A9: not x1 in ( dom f1) & not x2 in ( dom f1);

        then

        consider n such that

         A10: n in ( dom f2) & x1 = (( len f1) + n) by A2, FINSEQ_1: 25;

        consider k such that

         A11: k in ( dom f2) & x2 = (( len f1) + k) by A2, A9, FINSEQ_1: 25;

        

         A12: (F . x1) = (f2 . n) & (F . x2) = (f2 . k) by A10, A11, FINSEQ_1:def 7;

        then (f2 _ (n,y1)) = (f2 _ (k,y2)) by A2;

        hence thesis by A2, A10, A11, Def6, A12;

      end;

    end;

    definition

      let D be finite set;

      :: FLEXARY1:def7

      mode DoubleReorganization of D -> double-one-to-one FinSequence of (D * ) means

      : Def7: ( Values it ) = D;

      existence

      proof

        set F = ( canFS D);

        F is Element of (D * ) by FINSEQ_1:def 11;

        then {F} c= (D * ) & ( rng <*F*>) = {F} by ZFMISC_1: 31, FINSEQ_1: 38;

        then

        reconsider FF = <*F*> as double-one-to-one FinSequence of (D * ) by FINSEQ_1:def 4;

        

         A1: ( rngs FF) = <*( rng F)*> by FINSEQ_3: 132;

        ( rng <*( rng F)*>) = {( rng F)} by FINSEQ_1: 38;

        then ( union ( rng <*( rng F)*>)) = ( rng F) by ZFMISC_1: 25;

        then ( Union ( rngs FF)) = ( rng F) by CARD_3:def 4, A1;

        then ( Values FF) = ( rng F) by MATRIX_0:def 9;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    theorem :: FLEXARY1:34

    

     Th34: {} is DoubleReorganization of {} & <* {} *> is DoubleReorganization of {}

    proof

       {} = ( <*> ( {} * ));

      then

      reconsider D = {} as double-one-to-one FinSequence of ( {} * );

      ( rngs D) = ( {} --> D) by FUNCT_6: 23;

      then ( Union ( rngs D)) = {} by FUNCT_6: 26;

      then ( Values D) = {} by MATRIX_0:def 9;

      hence {} is DoubleReorganization of {} by Def7;

      ( rng {} ) = {} ;

      then

      reconsider F = {} as FinSequence of {} by FINSEQ_1:def 4;

       {F} c= ( {} * ) & ( rng <*F*>) = {F} by FINSEQ_1: 38;

      then

      reconsider FF = <*F*> as double-one-to-one FinSequence of ( {} * ) by FINSEQ_1:def 4;

      

       A1: ( rngs FF) = <*( rng F)*> by FINSEQ_3: 132;

      ( rng <*( rng F)*>) = {( rng F)} by FINSEQ_1: 38;

      then ( union ( rng <*( rng F)*>)) = ( rng F) by ZFMISC_1: 25;

      then ( Union ( rngs FF)) = ( rng F) by CARD_3:def 4, A1;

      then ( Values FF) = {} by MATRIX_0:def 9;

      hence thesis by Def7;

    end;

    theorem :: FLEXARY1:35

    

     Th35: for D be finite set, F be one-to-one onto FinSequence of D holds <*F*> is DoubleReorganization of D

    proof

      let D be finite set, F be one-to-one onto FinSequence of D;

      F is Element of (D * ) by FINSEQ_1:def 11;

      then {F} c= (D * ) & ( rng <*F*>) = {F} by ZFMISC_1: 31, FINSEQ_1: 38;

      then

      reconsider FF = <*F*> as double-one-to-one FinSequence of (D * ) by FINSEQ_1:def 4;

      

       A1: ( rngs FF) = <*( rng F)*> by FINSEQ_3: 132;

      ( rng <*( rng F)*>) = {( rng F)} by FINSEQ_1: 38;

      then ( union ( rng <*( rng F)*>)) = ( rng F) by ZFMISC_1: 25;

      then ( Union ( rngs FF)) = ( rng F) by CARD_3:def 4, A1;

      then ( Values FF) = ( rng F) by MATRIX_0:def 9;

      hence thesis by FUNCT_2:def 3, Def7;

    end;

    theorem :: FLEXARY1:36

    

     Th36: for D1,D2 be finite set st D1 misses D2 holds for o1 be DoubleReorganization of D1, o2 be DoubleReorganization of D2 holds (o1 ^ o2) is DoubleReorganization of (D1 \/ D2)

    proof

      let D1,D2 be finite set such that

       A1: D1 misses D2;

      let o1 be DoubleReorganization of D1, o2 be DoubleReorganization of D2;

      set D = (D1 \/ D2);

      ( rng o1) c= (D * )

      proof

        let x be object;

        assume x in ( rng o1);

        then

        reconsider x as FinSequence of D1 by FINSEQ_1:def 11;

        ( rng x) c= D1 & D1 c= D by XBOOLE_1: 7;

        then ( rng x) c= D;

        then x is FinSequence of D by FINSEQ_1:def 4;

        hence thesis by FINSEQ_1:def 11;

      end;

      then

      reconsider O1 = o1 as FinSequence of (D * ) by FINSEQ_1:def 4;

      ( rng o2) c= (D * )

      proof

        let x be object;

        assume x in ( rng o2);

        then

        reconsider x as FinSequence of D2 by FINSEQ_1:def 11;

        ( rng x) c= D2 & D2 c= D by XBOOLE_1: 7;

        then ( rng x) c= D;

        then x is FinSequence of D by FINSEQ_1:def 4;

        hence thesis by FINSEQ_1:def 11;

      end;

      then

      reconsider O2 = o2 as FinSequence of (D * ) by FINSEQ_1:def 4;

      

       A2: ( Values o1) = D1 & ( Values o2) = D2 by Def7;

      then

       A3: (O1 ^ O2) is double-one-to-one by A1, Th33;

      ( Values (O1 ^ O2)) = (D1 \/ D2) by A2, Th2;

      hence thesis by A3, Def7;

    end;

    theorem :: FLEXARY1:37

    

     Th37: for D be finite set, o be DoubleReorganization of D, F be one-to-one FinSequence st i in ( dom o) & (( rng F) /\ D) c= ( rng (o . i)) holds (o +* (i,F)) is DoubleReorganization of (( rng F) \/ (D \ ( rng (o . i))))

    proof

      let D be finite set, o be DoubleReorganization of D, F be one-to-one FinSequence such that

       A1: i in ( dom o) & (( rng F) /\ D) c= ( rng (o . i));

      set rF = ( rng F), oi = (o . i), roi = ( rng oi), oF = (o +* (i,F));

      

       A2: ( dom oF) = ( dom o) by FUNCT_7: 30;

      

       A3: (oF . i) = F by A1, FUNCT_7: 31;

      

       A4: ( Values o) = D by Def7;

      ( rng oF) c= ((rF \/ (D \ roi)) * )

      proof

        let y be object;

        assume y in ( rng oF);

        then

        consider x be object such that

         A5: x in ( dom oF) & (oF . x) = y by FUNCT_1:def 3;

        per cases ;

          suppose x = i;

          then

           A6: y = F by A5, A1, FUNCT_7: 31;

          F is FinSequence of (rF \/ (D \ roi)) by XBOOLE_1: 7, FINSEQ_1:def 4;

          hence thesis by A6, FINSEQ_1:def 11;

        end;

          suppose

           A7: x <> i;

          then

           A8: (oF . x) = (o . x) by FUNCT_7: 32;

          (o . x) in ( rng o) by A2, A5, FUNCT_1:def 3;

          then

          reconsider ox = (o . x) as FinSequence of D by FINSEQ_1:def 11;

          ( rng ox) misses roi

          proof

            assume ( rng ox) meets roi;

            then

            consider z be object such that

             A9: z in ( rng ox) & z in roi by XBOOLE_0: 3;

            consider a be object such that

             A10: a in ( dom ox) & (ox . a) = z by A9, FUNCT_1:def 3;

            consider b be object such that

             A11: b in ( dom oi) & (oi . b) = z by A9, FUNCT_1:def 3;

            (o _ (x,a)) = (o _ (i,b)) by A10, A11;

            hence thesis by A10, A11, A5, A2, A1, Def6, A7;

          end;

          then

           A12: ( rng ox) c= (D \ roi) by XBOOLE_1: 86;

          (D \ roi) c= (rF \/ (D \ roi)) by XBOOLE_1: 7;

          then ( rng ox) c= (rF \/ (D \ roi)) by A12;

          then ox is FinSequence of (rF \/ (D \ roi)) by FINSEQ_1:def 4;

          hence thesis by A8, A5, FINSEQ_1:def 11;

        end;

      end;

      then

      reconsider oF as FinSequence of ((rF \/ (D \ roi)) * ) by FINSEQ_1:def 4;

      

       A13: oF is double-one-to-one

      proof

        let x1,x2,y1,y2 be object such that

         A14: x1 in ( dom oF) & y1 in ( dom (oF . x1)) & x2 in ( dom oF) & y2 in ( dom (oF . x2)) & (oF _ (x1,y1)) = (oF _ (x2,y2));

        per cases ;

          suppose x1 = i & x2 = i;

          hence thesis by A3, A14, FUNCT_1:def 4;

        end;

          suppose

           A15: x1 = i & x2 <> i;

          then

           A16: ((oF . x1) . y1) in rF by A3, A14, FUNCT_1:def 3;

          

           A17: (oF . x2) = (o . x2) by A15, FUNCT_7: 32;

          then ((o . x2) . y2) in D by A14, A2, Th1, A4;

          then ((o . x2) . y2) in (D /\ rF) by A14, A17, A16, XBOOLE_0:def 4;

          then

          consider y3 be object such that

           A18: y3 in ( dom oi) & (oi . y3) = ((o . x2) . y2) by A1, FUNCT_1:def 3;

          (o _ (x2,y2)) = (o _ (i,y3)) by A18;

          hence thesis by Def6, A2, A18, A14, A17, A15;

        end;

          suppose

           A19: x1 <> i & x2 = i;

          then

           A20: ((oF . x2) . y2) in rF by A3, A14, FUNCT_1:def 3;

          

           A21: (oF . x1) = (o . x1) by A19, FUNCT_7: 32;

          then ((o . x1) . y1) in D by A14, A2, Th1, A4;

          then ((o . x1) . y1) in (D /\ rF) by A14, A21, A20, XBOOLE_0:def 4;

          then

          consider y3 be object such that

           A22: y3 in ( dom oi) & (oi . y3) = ((o . x1) . y1) by A1, FUNCT_1:def 3;

          (o _ (x1,y1)) = (o _ (i,y3)) by A22;

          hence thesis by Def6, A2, A22, A14, A21, A19;

        end;

          suppose x1 <> i & x2 <> i;

          then

           A23: (o . x1) = (oF . x1) & (o . x2) = (oF . x2) by FUNCT_7: 32;

          then (o _ (x1,y1)) = (o _ (x2,y2)) by A14;

          hence thesis by A23, A14, A2, Def6;

        end;

      end;

      

       A24: ( Values oF) c= (rF \/ (D \ roi))

      proof

        let z be object;

        assume z in ( Values oF);

        then

        consider x,y be object such that

         A25: x in ( dom oF) & y in ( dom (oF . x)) & z = ((oF . x) . y) by Th1;

        per cases ;

          suppose x = i;

          then (oF . x) = F by A1, FUNCT_7: 31;

          then z in rF by A25, FUNCT_1:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A26: x <> i;

          then

           A27: (oF . x) = (o . x) by FUNCT_7: 32;

          then

           A28: z in D by A4, A2, A25, Th1;

           not z in roi

          proof

            assume z in roi;

            then

            consider a be object such that

             A29: a in ( dom oi) & (oi . a) = z by FUNCT_1:def 3;

            (o _ (i,a)) = (o _ (x,y)) by A26, FUNCT_7: 32, A25, A29;

            hence thesis by A27, A25, A29, A1, A2, Def6, A26;

          end;

          then z in (D \ roi) by A28, XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      

       A30: (D \ roi) c= ( Values oF)

      proof

        let d be object;

        assume

         A31: d in (D \ roi);

        then

         A32: d in D & not d in roi by XBOOLE_0:def 5;

        consider x,y be object such that

         A33: x in ( dom o) & y in ( dom (o . x)) & d = ((o . x) . y) by A31, Th1, A4;

        x <> i by A33, FUNCT_1:def 3, A32;

        then (o . x) = (oF . x) by FUNCT_7: 32;

        hence thesis by Th1, A2, A33;

      end;

      rF c= ( Values oF)

      proof

        let d be object;

        assume d in rF;

        then ex x be object st x in ( dom F) & (F . x) = d by FUNCT_1:def 3;

        hence thesis by A1, A2, A3, Th1;

      end;

      then ( Values oF) = (rF \/ (D \ roi)) by A30, XBOOLE_1: 8, A24;

      hence thesis by A13, Def7;

    end;

    registration

      let D be finite set;

      let n be non zero Nat;

      cluster n -element for DoubleReorganization of D;

      existence

      proof

        defpred P[ Nat] means $1 > 0 implies ex o be DoubleReorganization of D st o is $1 -element;

        

         A1: P[ 0 ];

        

         A2: P[i] implies P[(i + 1)]

        proof

          assume

           A3: P[i];

          assume (i + 1) > 0 ;

          per cases ;

            suppose

             A4: i = 0 ;

            set F = ( canFS D);

             <*F*> is DoubleReorganization of D by Th35;

            hence thesis by A4;

          end;

            suppose i > 0 ;

            then

            consider o be DoubleReorganization of D such that

             A5: o is i -element by A3;

            reconsider e = <* {} *> as DoubleReorganization of {} by Th34;

            D misses {} ;

            then (o ^ e) is DoubleReorganization of (D \/ {} ) by Th36;

            hence thesis by A5;

          end;

        end;

         P[i] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end

    registration

      let D be finite natural-membered set;

      let o be DoubleReorganization of D;

      let x be object;

      cluster (o . x) -> natural-valued;

      coherence

      proof

        set ox = (o . x);

        per cases ;

          suppose

           A1: x in ( dom o);

          ( rng ox) c= NAT

          proof

            let y be object;

            assume y in ( rng ox);

            then

            consider z be object such that

             A2: z in ( dom ox) & (ox . z) = y by FUNCT_1:def 3;

            y in ( Values o) by A1, A2, Th1;

            then y in D by Def7;

            hence thesis by ORDINAL1:def 12;

          end;

          hence thesis by VALUED_0:def 6;

        end;

          suppose not x in ( dom o);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    theorem :: FLEXARY1:38

    

     Th38: for F be non empty FinSequence, G be finite Function st ( rng G) c= ( rng F) holds ex o be ( len F) -element DoubleReorganization of ( dom G) st for n holds ((F . n) = (G . (o _ (n,1))) & ... & (F . n) = (G . (o _ (n,( len (o . n))))))

    proof

      let F be non empty FinSequence, G be finite Function such that

       A1: ( rng G) c= ( rng F);

      set D = ( dom G);

      set d = the one-to-one onto FinSequence of D;

      

       A2: ( rng d) = D by FUNCT_2:def 3;

      then

       A3: ( card ( dom d)) = ( card D) by CARD_1: 70;

      

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

      

       A5: ( card D) = ( len d) & ( card G) = ( card D) by CARD_1: 62, A3;

      defpred P[ Nat] means $1 <= ( card G) implies ex o be ( len F) -element DoubleReorganization of (d .: ( Seg $1)) st for k holds ((F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k))))));

      

       A6: P[ 0 ]

      proof

        assume 0 <= ( card G);

        take o = the ( len F) -element DoubleReorganization of (d .: ( Seg 0 ));

        let i, j;

        thus thesis;

      end;

      

       A7: P[i] implies P[(i + 1)]

      proof

        set i1 = (i + 1), di1 = (d . i1);

        assume

         A8: P[i];

        assume

         A9: i1 <= ( card G);

        then

        consider o be ( len F) -element DoubleReorganization of (d .: ( Seg i)) such that

         A10: for j holds ((F . j) = (G . (o _ (j,1))) & ... & (F . j) = (G . (o _ (j,( len (o . j)))))) by NAT_1: 13, A8;

        

         A11: ( len o) = ( len F) by CARD_1:def 7;

        then

         A12: ( dom o) = ( dom F) by FINSEQ_3: 29;

        

         A13: ( Values o) = (d .: ( Seg i)) by Def7;

        

         A14: i1 in ( dom d) by NAT_1: 11, A5, A9, FINSEQ_3: 25;

        then di1 in D by A2, FUNCT_1:def 3;

        then (G . di1) in ( rng G) by FUNCT_1:def 3;

        then

        consider x be object such that

         A15: x in ( dom F) & (F . x) = (G . di1) by A1, FUNCT_1:def 3;

        reconsider x as Nat by A15;

        set ox = (o . x), I1 = <*di1*>, oxI = (ox ^ I1);

        

         A16: i < i1 by NAT_1: 13;

         not di1 in ( rng ox)

        proof

          assume (d . i1) in ( rng ox);

          then

          consider y be object such that

           A17: y in ( dom ox) & (d . i1) = (ox . y) by FUNCT_1:def 3;

          (d . i1) in (d .: ( Seg i)) by Th1, A15, A12, A13, A17;

          then

          consider z be object such that

           A18: z in ( dom d) & z in ( Seg i) & (d . z) = (d . i1) by FUNCT_1:def 6;

          i1 in ( Seg i) by A14, FUNCT_1:def 4, A18;

          hence thesis by FINSEQ_1: 1, A16;

        end;

        then

         A19: oxI is one-to-one by GRAPHSP: 1;

        

         A20: x in ( dom o) by A15, A11, FINSEQ_3: 29;

        ox in ( rng o) by A15, A12, FUNCT_1:def 3;

        then

         A21: ox is FinSequence of (d .: ( Seg i)) by FINSEQ_1:def 11;

        then

         A22: ( rng ox) c= (d .: ( Seg i)) by FINSEQ_1:def 4;

        

         A23: (( rng ox) /\ (d .: ( Seg i))) = ( rng ox) by A21, FINSEQ_1:def 4, XBOOLE_1: 28;

         not i1 in ( Seg i) by A16, FINSEQ_1: 1;

        then {i1} misses ( Seg i) by ZFMISC_1: 52, ZFMISC_1: 45;

        then

         A24: ((d .: {i1}) /\ (d .: ( Seg i))) = (d .: {} ) by FUNCT_1: 62;

        then

         A25: (d .: {i1}) misses (d .: ( Seg i));

        ( Im (d,i1)) = {di1} by A14, FUNCT_1: 59;

        then

         A26: (d .: {i1}) = {di1} by RELAT_1:def 16;

        

         A27: ( rng I1) = {di1} by FINSEQ_1: 39;

        then ( rng oxI) = (( rng ox) \/ {di1}) by FINSEQ_1: 31;

        then

         A28: (( rng oxI) /\ (d .: ( Seg i))) = (( rng ox) \/ {} ) by A23, XBOOLE_1: 23, A24, A26;

        

         A29: (( Seg i) \/ {i1}) = ( Seg i1) by FINSEQ_1: 9;

        then

         A30: ((d .: ( Seg i)) \/ (d .: {i1})) = (d .: ( Seg i1)) by RELAT_1: 120;

        (d .: ( Seg i)) c= (d .: ( Seg i1)) by XBOOLE_1: 7, A29, RELAT_1: 123;

        then

         A31: ( rng ox) c= (d .: ( Seg i1)) by A22;

        set O = (o +* (x,oxI));

        (( rng oxI) \/ ((d .: ( Seg i)) \ ( rng ox))) = ((( rng ox) \/ {di1}) \/ ((d .: ( Seg i)) \ ( rng ox))) by A27, FINSEQ_1: 31

        .= (( rng ox) \/ ( {di1} \/ ((d .: ( Seg i)) \ ( rng ox)))) by XBOOLE_1: 4

        .= (( rng ox) \/ (( {di1} \/ (d .: ( Seg i))) \ ( rng ox))) by A22, A25, A26, XBOOLE_1: 63, XBOOLE_1: 87

        .= (( rng ox) \/ ( {di1} \/ (d .: ( Seg i)))) by XBOOLE_1: 39

        .= (d .: ( Seg i1)) by A26, A31, XBOOLE_1: 12, A30;

        then

        reconsider O as ( len F) -element DoubleReorganization of (d .: ( Seg i1)) by A19, A20, Th37, A28;

        take O;

        let k;

        set Ok = (O . k);

        

         A32: ( dom I1) = ( Seg 1) & ( Seg 1) = {1} & (I1 . 1) = di1 by FINSEQ_1: 38, FINSEQ_1: 40, FINSEQ_1: 2;

        thus (F . k) = (G . (O _ (k,1))) & ... & (F . k) = (G . (O _ (k,( len Ok))))

        proof

          let j;

          assume

           A33: 1 <= j & j <= ( len Ok);

          

           A34: (F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k))))) by A10;

          per cases ;

            suppose

             A35: k <> x;

            then Ok = (o . k) by FUNCT_7: 32;

            then (F . k) = (G . (o _ (k,j))) by A33, A34;

            hence thesis by A35, FUNCT_7: 32;

          end;

            suppose

             A36: k = x;

            then

             A37: Ok = oxI by A15, A12, FUNCT_7: 31;

            per cases ;

              suppose

               A38: j in ( dom ox);

              then

               A39: (oxI . j) = (ox . j) & j <= ( len ox) by FINSEQ_1:def 7, FINSEQ_3: 25;

              (o _ (k,j)) = (oxI . j) by A36, A38, FINSEQ_1:def 7

              .= (Ok . j) by A36, A15, A12, FUNCT_7: 31;

              hence thesis by A39, A36, A34, A33;

            end;

              suppose not j in ( dom ox);

              then

              consider n such that

               A40: n in ( dom I1) & j = (( len ox) + n) by A37, A33, FINSEQ_3: 25, FINSEQ_1: 25;

              n = 1 by A32, A40, TARSKI:def 1;

              

              then (F . k) = (G . (oxI . j)) by A40, A32, FINSEQ_1:def 7, A15, A36

              .= (G . (Ok . j)) by A36, A15, A12, FUNCT_7: 31;

              hence thesis;

            end;

          end;

        end;

      end;

      

       A41: (d .: ( Seg ( card D))) = D by A2, RELAT_1: 113, A5, A4;

       P[i] from NAT_1:sch 2( A6, A7);

      then ex o be ( len F) -element DoubleReorganization of ( dom G) st for k holds ((F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k)))))) by A41, A5;

      hence thesis;

    end;

    theorem :: FLEXARY1:39

    for F be non empty FinSequence, G be FinSequence st ( rng G) c= ( rng F) holds ex o be ( len F) -element DoubleReorganization of ( dom G) st for n holds (o . n) is increasing & ((F . n) = (G . (o _ (n,1))) & ... & (F . n) = (G . (o _ (n,( len (o . n))))))

    proof

      let F be non empty FinSequence, G be FinSequence such that

       A1: ( rng G) c= ( rng F);

      defpred P[ Nat] means $1 <= ( len G) implies ex o be ( len F) -element DoubleReorganization of ( Seg $1) st for k holds (o . k) is increasing & ((F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k))))));

      

       A2: P[ 0 ]

      proof

        assume 0 <= ( len G);

        take o = the ( len F) -element DoubleReorganization of ( Seg 0 );

        let i;

        thus (o . i) is increasing;

        let j;

        thus thesis;

      end;

      

       A3: P[i] implies P[(i + 1)]

      proof

        set i1 = (i + 1);

        assume

         A4: P[i];

        assume

         A5: i1 <= ( len G);

        then

        consider o be ( len F) -element DoubleReorganization of ( Seg i) such that

         A6: for j holds (o . j) is increasing & ((F . j) = (G . (o _ (j,1))) & ... & (F . j) = (G . (o _ (j,( len (o . j)))))) by NAT_1: 13, A4;

        

         A7: ( len o) = ( len F) by CARD_1:def 7;

        then

         A8: ( dom o) = ( dom F) by FINSEQ_3: 29;

        

         A9: ( Values o) = ( Seg i) by Def7;

        i1 in ( dom G) by NAT_1: 11, A5, FINSEQ_3: 25;

        then (G . i1) in ( rng G) by FUNCT_1:def 3;

        then

        consider x be object such that

         A10: x in ( dom F) & (F . x) = (G . i1) by A1, FUNCT_1:def 3;

        reconsider x as Nat by A10;

        set ox = (o . x), I1 = <*i1*>, oxI = (ox ^ I1);

        

         A11: i < i1 by NAT_1: 13;

         not i1 in ( rng ox)

        proof

          assume i1 in ( rng ox);

          then

          consider y be object such that

           A12: y in ( dom ox) & i1 = (ox . y) by FUNCT_1:def 3;

          i1 in ( Seg i) by Th1, A10, A8, A9, A12;

          hence thesis by FINSEQ_1: 1, A11;

        end;

        then

         A13: oxI is one-to-one by GRAPHSP: 1;

        

         A14: x in ( dom o) by A10, A7, FINSEQ_3: 29;

        ox in ( rng o) by A10, A8, FUNCT_1:def 3;

        then

         A15: ox is FinSequence of ( Seg i) by FINSEQ_1:def 11;

        then

         A16: ( rng ox) c= ( Seg i) by FINSEQ_1:def 4;

        

         A17: (( rng ox) /\ ( Seg i)) = ( rng ox) by A15, FINSEQ_1:def 4, XBOOLE_1: 28;

         not i1 in ( Seg i) by A11, FINSEQ_1: 1;

        then

         A18: {i1} misses ( Seg i) by ZFMISC_1: 52, ZFMISC_1: 45;

        

         A19: ( rng I1) = {i1} by FINSEQ_1: 39;

        then ( rng oxI) = (( rng ox) \/ {i1}) by FINSEQ_1: 31;

        then

         A20: (( rng oxI) /\ ( Seg i)) = (( rng ox) \/ {} ) by A17, A18, XBOOLE_1: 23;

        

         A21: (( Seg i) \/ {i1}) = ( Seg i1) by FINSEQ_1: 9;

        ( Seg i) c= ( {i1} \/ ( Seg i)) by XBOOLE_1: 7;

        then

         A22: ( rng ox) c= ( {i1} \/ ( Seg i)) by A16;

        set O = (o +* (x,oxI));

        (( rng oxI) \/ (( Seg i) \ ( rng ox))) = ((( rng ox) \/ {i1}) \/ (( Seg i) \ ( rng ox))) by A19, FINSEQ_1: 31

        .= (( rng ox) \/ ( {i1} \/ (( Seg i) \ ( rng ox)))) by XBOOLE_1: 4

        .= (( rng ox) \/ (( {i1} \/ ( Seg i)) \ ( rng ox))) by A16, A18, XBOOLE_1: 63, XBOOLE_1: 87

        .= (( rng ox) \/ ( {i1} \/ ( Seg i))) by XBOOLE_1: 39

        .= ( {i1} \/ ( Seg i)) by A22, XBOOLE_1: 12;

        then

        reconsider O as ( len F) -element DoubleReorganization of ( Seg i1) by A13, A14, Th37, A20, A21;

        take O;

        let k;

        set Ok = (O . k);

        

         A23: ( dom I1) = ( Seg 1) & ( Seg 1) = {1} & (I1 . 1) = i1 by FINSEQ_1: 38, FINSEQ_1: 40, FINSEQ_1: 2;

        thus Ok is increasing

        proof

          per cases ;

            suppose k <> x;

            then Ok = (o . k) by FUNCT_7: 32;

            hence thesis by A6;

          end;

            suppose k = x;

            then

             A24: Ok = oxI by A10, A8, FUNCT_7: 31;

            let e1,e2 be ExtReal;

            assume

             A25: e1 in ( dom Ok) & e2 in ( dom Ok) & e1 < e2;

            per cases ;

              suppose

               A26: e1 in ( dom ox) & e2 in ( dom ox);

              then (Ok . e1) = (ox . e1) & (Ok . e2) = (ox . e2) & ox is increasing by A6, A24, FINSEQ_1:def 7;

              hence (Ok . e1) < (Ok . e2) by A25, A26, VALUED_0:def 13;

            end;

              suppose not e1 in ( dom ox) & e2 in ( dom ox);

              then e2 <= ( len ox) & 1 <= e1 & (1 > e1 or e1 > ( len ox)) by A25, FINSEQ_3: 25;

              hence thesis by XXREAL_0: 2, A25;

            end;

              suppose

               A27: e1 in ( dom ox) & not e2 in ( dom ox);

              then

              consider n such that

               A28: n in ( dom I1) & e2 = (( len ox) + n) by A24, A25, FINSEQ_1: 25;

              n = 1 by A23, A28, TARSKI:def 1;

              then

               A29: (oxI . e2) = i1 by A28, FINSEQ_1:def 7, A23;

              

               A30: (ox . e1) = (oxI . e1) by A27, FINSEQ_1:def 7;

              (ox . e1) in ( Seg i) by A10, A8, Th1, A9, A27;

              then (ox . e1) <= i by FINSEQ_1: 1;

              hence thesis by A29, A30, NAT_1: 13, A24;

            end;

              suppose

               A31: not e1 in ( dom ox) & not e2 in ( dom ox);

              then

              consider n such that

               A32: n in ( dom I1) & e1 = (( len ox) + n) by A24, A25, FINSEQ_1: 25;

              consider k such that

               A33: k in ( dom I1) & e2 = (( len ox) + k) by A24, A31, A25, FINSEQ_1: 25;

              n = 1 & k = 1 by A33, A23, A32, TARSKI:def 1;

              hence thesis by A32, A33, A25;

            end;

          end;

        end;

        thus (F . k) = (G . (O _ (k,1))) & ... & (F . k) = (G . (O _ (k,( len Ok))))

        proof

          let j;

          assume

           A34: 1 <= j & j <= ( len Ok);

          

           A35: (F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k))))) by A6;

          per cases ;

            suppose

             A36: k <> x;

            then Ok = (o . k) by FUNCT_7: 32;

            then (F . k) = (G . (o _ (k,j))) by A34, A35;

            hence thesis by A36, FUNCT_7: 32;

          end;

            suppose

             A37: k = x;

            then

             A38: Ok = oxI by A10, A8, FUNCT_7: 31;

            per cases ;

              suppose

               A39: j in ( dom ox);

              then

               A40: (oxI . j) = (ox . j) & j <= ( len ox) by FINSEQ_1:def 7, FINSEQ_3: 25;

              (o _ (k,j)) = (oxI . j) by A37, A39, FINSEQ_1:def 7

              .= (Ok . j) by A37, A14, FUNCT_7: 31;

              hence thesis by A40, A37, A35, A34;

            end;

              suppose not j in ( dom ox);

              then

              consider n such that

               A41: n in ( dom I1) & j = (( len ox) + n) by A38, A34, FINSEQ_3: 25, FINSEQ_1: 25;

              n = 1 by A23, A41, TARSKI:def 1;

              

              then (F . k) = (G . (oxI . j)) by A41, A23, FINSEQ_1:def 7, A10, A37

              .= (G . (Ok . j)) by A37, A14, FUNCT_7: 31;

              hence thesis;

            end;

          end;

        end;

      end;

      

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

       P[i] from NAT_1:sch 2( A2, A3);

      then ex o be ( len F) -element DoubleReorganization of ( dom G) st for k holds (o . k) is increasing & ((F . k) = (G . (o _ (k,1))) & ... & (F . k) = (G . (o _ (k,( len (o . k)))))) by A42;

      hence thesis;

    end;

    registration

      let f be finite Function;

      let o be DoubleReorganization of ( dom f);

      let x be object;

      cluster (f * (o . x)) -> FinSequence-like;

      coherence

      proof

        reconsider X = x as set by TARSKI: 1;

        per cases ;

          suppose x in ( dom o);

          then (o . x) in ( rng o) by FUNCT_1:def 3;

          then

          reconsider ox = (o . X) as FinSequence of ( dom f) by FINSEQ_1:def 11;

          

           A1: ( rng ox) c= ( dom f);

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

          hence thesis by A1, RELAT_1: 27;

        end;

          suppose not x in ( dom o);

          then (o . x) = {} by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

    end

    registration

      cluster complex-functions-valued FinSequence-yielding for FinSequence;

      existence

      proof

        take T = the empty Function;

        thus thesis;

      end;

    end

    notation

      let f be Function-yielding Function, g be Function;

      synonym g *. f for ^^^g,f__;

    end

    registration

      let f be Function-yielding Function, g be Function;

      cluster (g *. f) -> Function-yielding;

      coherence

      proof

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( dom (g *. f));

          then x in ( dom f) by FOMODEL2:def 6;

          then ((g *. f) . x) = (g * (f . xx)) by FOMODEL2:def 6;

          hence ((g *. f) . x) is Function;

        end;

        hence thesis by FUNCOP_1:def 6;

      end;

    end

    registration

      let g be Function;

      let f be (( dom g) * ) -valued FinSequence;

      cluster (g *. f) -> FinSequence-yielding;

      coherence

      proof

        set gf = (g *. f);

        now

          let x be object;

          reconsider X = x as set by TARSKI: 1;

          

           A1: ( dom gf) = ( dom f) by FOMODEL2:def 6;

          assume

           A2: x in ( dom gf);

          then

           A3: (gf . x) = (g * (f . X)) by A1, FOMODEL2:def 6;

          (f . x) in ( rng f) by A2, A1, FUNCT_1:def 3;

          then

          reconsider fx = (f . X) as FinSequence of ( dom g) by FINSEQ_1:def 11;

          

           A4: ( rng fx) c= ( dom g);

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

          hence (gf . x) is FinSequence by FINSEQ_1:def 2, A3, A4, RELAT_1: 27;

        end;

        hence thesis by PRE_POLY:def 3;

      end;

      let x be object;

      cluster ((g *. f) . x) -> ( len (f . x)) -element;

      coherence

      proof

        set gf = (g *. f);

        reconsider X = x as set by TARSKI: 1;

        

         A5: ( dom gf) = ( dom f) by FOMODEL2:def 6;

        per cases ;

          suppose

           A6: x in ( dom gf);

          then

           A7: (gf . x) = (g * (f . X)) by A5, FOMODEL2:def 6;

          (f . x) in ( rng f) by A6, A5, FUNCT_1:def 3;

          then

          reconsider fx = (f . X) as FinSequence of ( dom g) by FINSEQ_1:def 11;

          ( rng fx) c= ( dom g);

          then ( dom (gf . x)) = ( dom fx) by RELAT_1: 27, A7;

          then ( len (gf . X)) = ( len fx) by FINSEQ_3: 29;

          hence thesis by CARD_1:def 7;

        end;

          suppose not x in ( dom gf);

          then (gf . x) = {} & (f . x) = {} by A5, FUNCT_1:def 2;

          hence thesis;

        end;

      end;

    end

    registration

      let f be Function-yielding FinSequence, g be Function;

      cluster (g *. f) -> FinSequence-like;

      coherence

      proof

        ( dom (g *. f)) = ( dom f) & ( dom f) = ( Seg ( len f)) by FOMODEL2:def 6, FINSEQ_1:def 3;

        hence thesis;

      end;

      cluster (g *. f) -> ( len f) -element;

      coherence

      proof

        ( dom (g *. f)) = ( dom f) & ( dom f) = ( Seg ( len f)) by FOMODEL2:def 6, FINSEQ_1:def 3;

        then ( len (g *. f)) = ( len f) by FINSEQ_3: 29;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let f be Function-yielding Function, g be complex-valued Function;

      cluster (g *. f) -> complex-functions-valued;

      coherence

      proof

        set gf = (g *. f);

        now

          let x be object;

          

           A1: ( dom gf) = ( dom f) by FOMODEL2:def 6;

          reconsider X = x as set by TARSKI: 1;

          assume x in ( dom gf);

          then (gf . x) = (g * (f . X)) by A1, FOMODEL2:def 6;

          hence (gf . x) is complex-valued Function;

        end;

        hence thesis by VALUED_2:def 26;

      end;

    end

    registration

      let f be Function-yielding Function, g be natural-valued Function;

      cluster (g *. f) -> natural-functions-valued;

      coherence

      proof

        set gf = (g *. f);

        now

          let x be object;

          

           A1: ( dom gf) = ( dom f) by FOMODEL2:def 6;

          reconsider X = x as set by TARSKI: 1;

          assume x in ( dom gf);

          then (gf . x) = (g * (f . X)) by A1, FOMODEL2:def 6;

          hence (gf . x) is natural-valued Function;

        end;

        hence thesis by VALUED_2:def 31;

      end;

    end

    theorem :: FLEXARY1:40

    for f be Function-yielding Function, g be Function holds ( Values (g *. f)) = (g .: ( Values f))

    proof

      let f be Function-yielding Function, g be Function;

      set gf = (g *. f);

      

       A1: ( dom gf) = ( dom f) by FOMODEL2:def 6;

      thus ( Values gf) c= (g .: ( Values f))

      proof

        let a be object;

        assume a in ( Values gf);

        then

        consider x,y be object such that

         A2: x in ( dom gf) & y in ( dom (gf . x)) & a = ((gf . x) . y) by Th1;

        (gf . x) = (g * (f . x)) by A1, FOMODEL2:def 6, A2;

        then

         A3: ((gf . x) . y) = (g . ((f . x) . y)) & y in ( dom (f . x)) & ((f . x) . y) in ( dom g) by A2, FUNCT_1: 11, FUNCT_1: 12;

        then ((f . x) . y) in ( Values f) by A1, A2, Th1;

        hence thesis by A3, A2, FUNCT_1:def 6;

      end;

      let a be object;

      assume a in (g .: ( Values f));

      then

      consider b be object such that

       A4: b in ( dom g) & b in ( Values f) & (g . b) = a by FUNCT_1:def 6;

      consider x,y be object such that

       A5: x in ( dom f) & y in ( dom (f . x)) & b = ((f . x) . y) by A4, Th1;

      

       A6: (g . ((f . x) . y)) = ((g * (f . x)) . y) & y in ( dom (g * (f . x))) by A4, A5, FUNCT_1: 11, FUNCT_1: 13;

      (g * (f . x)) = (gf . x) & x in ( dom gf) by A5, FOMODEL2:def 6;

      hence thesis by Th1, A4, A5, A6;

    end;

    theorem :: FLEXARY1:41

    

     Th41: for f be Function-yielding Function, g be Function holds ((g *. f) . x) = (g * (f . x))

    proof

      let f be Function-yielding Function, g be Function;

      per cases ;

        suppose x in ( dom f);

        hence thesis by FOMODEL2:def 6;

      end;

        suppose not x in ( dom f);

        then not x in ( dom (g *. f)) & (f . x) = {} by FOMODEL2:def 6, FUNCT_1:def 2;

        then ((g *. f) . x) = {} & (g * (f . x)) = {} by FUNCT_1:def 2;

        hence thesis;

      end;

    end;

    theorem :: FLEXARY1:42

    

     Th42: for f be Function-yielding Function, g be FinSequence, x,y be object holds ((g *. f) _ (x,y)) = (g . (f _ (x,y)))

    proof

      let f be Function-yielding Function, g be FinSequence, x,y be object;

      

       A1: ((g *. f) . x) = (g * (f . x)) by Th41;

      per cases by A1, FUNCT_1: 11;

        suppose y in ( dom ((g *. f) . x));

        hence thesis by A1, FUNCT_1: 12;

      end;

        suppose not y in ( dom (f . x));

        then not y in ( dom ((g *. f) . x)) & ((f . x) . y) = {} by A1, FUNCT_1: 11, FUNCT_1:def 2;

        then not ((f . x) . y) in ( dom g) & (((g *. f) . x) . y) = {} by FINSEQ_3: 25, FUNCT_1:def 2;

        hence thesis by FUNCT_1:def 2;

      end;

        suppose not ((f . x) . y) in ( dom g);

        then not y in ( dom ((g *. f) . x)) & (g . ((f . x) . y)) = {} by A1, FUNCT_1: 11, FUNCT_1:def 2;

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    definition

      let f be complex-functions-valued FinSequence-yielding Function;

      :: FLEXARY1:def8

      func Sum f -> complex-valued Function means

      : Def8: ( dom it ) = ( dom f) & for x be set holds (it . x) = ( Sum (f . x));

      existence

      proof

        defpred P[ object, object] means for x be set st x = $1 holds $2 = ( Sum (f . x));

        

         A1: for e be object st e in ( dom f) holds ex u be object st P[e, u]

        proof

          let e be object;

          assume e in ( dom f);

          then

          reconsider E = e as set;

          take s = ( Sum (f . E));

          thus thesis;

        end;

        consider s be Function such that

         A2: ( dom s) = ( dom f) & for e be object st e in ( dom f) holds P[e, (s . e)] from CLASSES1:sch 1( A1);

        ( rng s) c= COMPLEX

        proof

          let y be object;

          assume y in ( rng s);

          then

          consider x be object such that

           A3: x in ( dom s) & (s . x) = y by FUNCT_1:def 3;

          reconsider x as set by TARSKI: 1;

          (s . x) = ( Sum (f . x)) by A3, A2;

          hence thesis by A3, XCMPLX_0:def 2;

        end;

        then

        reconsider s as complex-valued Function by VALUED_0:def 1;

        take s;

        thus ( dom s) = ( dom f) by A2;

        let x be set;

        per cases ;

          suppose x in ( dom f);

          hence thesis by A2;

        end;

          suppose

           A4: not x in ( dom f);

          then ( Sum (f . x)) = 0 by RVSUM_2: 29, FUNCT_1:def 2;

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

        end;

      end;

      uniqueness

      proof

        let C1,C2 be complex-valued Function such that

         A5: ( dom C1) = ( dom f) & for x be set holds (C1 . x) = ( Sum (f . x)) and

         A6: ( dom C2) = ( dom f) & for x be set holds (C2 . x) = ( Sum (f . x));

        now

          let x be object;

          reconsider X = x as set by TARSKI: 1;

          

          thus (C1 . x) = ( Sum (f . X)) by A5

          .= (C2 . x) by A6;

        end;

        hence thesis by A5, A6;

      end;

    end

    registration

      let f be complex-functions-valued FinSequence-yielding FinSequence;

      cluster ( Sum f) -> FinSequence-like;

      coherence

      proof

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

        hence thesis by Def8;

      end;

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

      coherence

      proof

        ( dom ( Sum f)) = ( dom f) by Def8;

        then ( len ( Sum f)) = ( len f) by FINSEQ_3: 29;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let f be natural-functions-valued FinSequence-yielding Function;

      cluster ( Sum f) -> natural-valued;

      coherence

      proof

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( dom ( Sum f));

          

           A1: (( Sum f) . x) = ( Sum (f . xx)) by Def8;

          ( rng (f . xx)) c= NAT by VALUED_0:def 6;

          then

          reconsider fx = (f . x) as FinSequence of NAT by FINSEQ_1:def 4;

          ( Sum fx) is Nat;

          hence (( Sum f) . x) is natural by A1;

        end;

        hence thesis by VALUED_0:def 12;

      end;

    end

    registration

      let f,g be complex-functions-valued FinSequence;

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

      coherence

      proof

        

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

        now

          let x be object;

          assume x in ( rng (f ^ g));

          then x in ( rng f) or x in ( rng g) by A1, XBOOLE_0:def 3;

          hence x is complex-valued Function;

        end;

        hence thesis by VALUED_2:def 2, VALUED_2:def 20;

      end;

    end

    registration

      let f,g be ext-real-valued FinSequence;

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

      coherence

      proof

        

         A1: ( rng f) c= ExtREAL & ( rng g) c= ExtREAL by VALUED_0:def 2;

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

        hence thesis by A1, XBOOLE_1: 8, VALUED_0:def 2;

      end;

    end

    registration

      let f be complex-functions-valued Function;

      let X be set;

      cluster (f | X) -> complex-functions-valued;

      coherence

      proof

        

         A1: ( dom (f | X)) c= ( dom f) by RELAT_1: 60;

        now

          let x be object;

          assume x in ( dom (f | X));

          then x in ( dom f) & ((f | X) . x) = (f . x) by FUNCT_1: 47, A1;

          hence ((f | X) . x) is complex-valued Function;

        end;

        hence thesis by VALUED_2:def 26;

      end;

    end

    registration

      let f be FinSequence-yielding Function;

      let X be set;

      cluster (f | X) -> FinSequence-yielding;

      coherence

      proof

        

         A1: ( dom (f | X)) c= ( dom f) by RELAT_1: 60;

        now

          let x be object;

          assume x in ( dom (f | X));

          then x in ( dom f) & ((f | X) . x) = (f . x) by FUNCT_1: 47, A1;

          hence ((f | X) . x) is FinSequence;

        end;

        hence thesis by PRE_POLY:def 3;

      end;

    end

    registration

      let F be complex-valued Function;

      cluster <*F*> -> complex-functions-valued;

      coherence

      proof

        now

          let x be object;

          

           A1: ( dom <*F*>) = ( Seg 1) & ( Seg 1) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          assume x in ( dom <*F*>);

          then x = 1 by A1, TARSKI:def 1;

          hence ( <*F*> . x) is complex-valued Function by FINSEQ_1: 40;

        end;

        hence thesis by VALUED_2:def 26;

      end;

    end

    theorem :: FLEXARY1:43

    

     Th43: for f,g be FinSequence st (f ^ g) is FinSequence-yielding holds f is FinSequence-yielding & g is FinSequence-yielding

    proof

      let f,g be FinSequence such that

       A1: (f ^ g) is FinSequence-yielding;

       A2:

      now

        let x be object;

        

         A3: ( dom f) c= ( dom (f ^ g)) by FINSEQ_1: 26;

        assume x in ( dom f);

        then (f . x) = ((f ^ g) . x) & x in ( dom (f ^ g)) by A3, FINSEQ_1:def 7;

        hence (f . x) is FinSequence by A1;

      end;

      now

        let x be object;

        assume

         A4: x in ( dom g);

        then

        reconsider xx = x as Nat;

        (g . x) = ((f ^ g) . (xx + ( len f))) by A4, FINSEQ_1:def 7;

        hence (g . x) is FinSequence by A1;

      end;

      hence thesis by A2, PRE_POLY:def 3;

    end;

    theorem :: FLEXARY1:44

    

     Th44: for f,g be FinSequence st (f ^ g) is complex-functions-valued holds f is complex-functions-valued & g is complex-functions-valued

    proof

      let f,g be FinSequence such that

       A1: (f ^ g) is complex-functions-valued;

       A2:

      now

        let x be object;

        

         A3: ( dom f) c= ( dom (f ^ g)) by FINSEQ_1: 26;

        assume x in ( dom f);

        then (f . x) = ((f ^ g) . x) & x in ( dom (f ^ g)) by A3, FINSEQ_1:def 7;

        hence (f . x) is complex-valued Function by A1;

      end;

      now

        let x be object;

        assume

         A4: x in ( dom g);

        then

        reconsider xx = x as Nat;

        (g . x) = ((f ^ g) . (xx + ( len f))) by A4, FINSEQ_1:def 7;

        hence (g . x) is complex-valued Function by A1;

      end;

      hence thesis by A2, VALUED_2:def 26;

    end;

    theorem :: FLEXARY1:45

    

     Th45: for f be complex-valued FinSequence holds ( Sum <*f*>) = <*( Sum f)*>

    proof

      let f be complex-valued FinSequence;

      

       A1: ( len <*f*>) = 1 & ( dom <*f*>) = ( dom ( Sum <*f*>)) & ( dom <*f*>) = ( Seg 1) by Def8, FINSEQ_1: 39, FINSEQ_1: 38;

      

       A2: (( Sum <*f*>) . 1) = ( Sum ( <*f*> . 1)) by Def8;

      ( <*f*> . 1) = f by FINSEQ_1: 40;

      hence thesis by A1, FINSEQ_3: 29, A2, FINSEQ_1: 40;

    end;

    theorem :: FLEXARY1:46

    

     Th46: for f,g be complex-functions-valued FinSequence-yielding FinSequence holds ( Sum (f ^ g)) = (( Sum f) ^ ( Sum g))

    proof

      let f,g be complex-functions-valued FinSequence-yielding FinSequence;

      

       A1: ( len ( Sum f)) = ( len f) & ( len ( Sum g)) = ( len g) & ( len ( Sum (f ^ g))) = ( len (f ^ g)) by CARD_1:def 7;

      

       A2: ( len (f ^ g)) = (( len f) + ( len g)) & ( len (( Sum f) ^ ( Sum g))) = (( len f) + ( len g)) by CARD_1:def 7, FINSEQ_1: 22;

      

       A3: ( dom f) = ( dom ( Sum f)) & ( dom g) = ( dom ( Sum g)) by Def8;

      for i st 1 <= i & i <= (( len f) + ( len g)) holds (( Sum (f ^ g)) . i) = ((( Sum f) ^ ( Sum g)) . i)

      proof

        let i such that

         A4: 1 <= i & i <= (( len f) + ( len g));

        

         A5: (( Sum (f ^ g)) . i) = ( Sum ((f ^ g) . i)) & (( Sum f) . i) = ( Sum (f . i)) by Def8;

        

         A6: i in ( dom (f ^ g)) by A4, A2, FINSEQ_3: 25;

        per cases by A6, FINSEQ_1: 25;

          suppose i in ( dom f);

          then ((f ^ g) . i) = (f . i) & ((( Sum f) ^ ( Sum g)) . i) = (( Sum f) . i) by A3, FINSEQ_1:def 7;

          hence thesis by A5;

        end;

          suppose ex j st j in ( dom g) & i = (( len f) + j);

          then

          consider j such that

           A7: j in ( dom g) & i = (( len f) + j);

          ((f ^ g) . i) = (g . j) & ((( Sum f) ^ ( Sum g)) . i) = (( Sum g) . j) by A7, A3, A1, FINSEQ_1:def 7;

          hence thesis by A5, Def8;

        end;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: FLEXARY1:47

    for f be complex-valued FinSequence, o be DoubleReorganization of ( dom f) holds ( Sum f) = ( Sum ( Sum (f *. o)))

    proof

      defpred P[ Nat] means for f be complex-valued FinSequence, o be DoubleReorganization of ( dom f) st ( len f) = $1 holds ( Sum f) = ( Sum ( Sum (f *. o)));

      

       A1: P[ 0 ]

      proof

        let f be complex-valued FinSequence, o be DoubleReorganization of ( dom f) such that

         A2: ( len f) = 0 ;

        set fo = (f *. o), S = ( Sum fo);

        

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

        x in ( dom S) implies (S . x) = 0

        proof

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( dom S);

          

           A4: (S . xx) = ( Sum (fo . x)) by Def8;

          ( dom (fo . x)) = {}

          proof

            assume ( dom (fo . x)) <> {} ;

            then

            consider y be object such that

             A5: y in ( dom (fo . x)) by XBOOLE_0:def 1;

            ( len (fo . x)) = ( len (o . x)) by CARD_1:def 7;

            then

             A6: ( dom (fo . x)) = ( dom (o . x)) by FINSEQ_3: 29;

            f = {} by A2;

            hence thesis by A6, A5;

          end;

          then (fo . x) = ( <*> REAL );

          hence thesis by RVSUM_1: 72, A4;

        end;

        then

         A7: S = (( len S) |-> 0 ) by A3;

        f = ( <*> REAL ) by A2;

        hence thesis by RVSUM_1: 72, A7, RVSUM_1: 81;

      end;

      

       A8: P[i] implies P[(i + 1)]

      proof

        assume

         A9: P[i];

        set i1 = (i + 1);

        let f be complex-valued FinSequence, o be DoubleReorganization of ( dom f) such that

         A10: ( len f) = i1;

        set fo = (f *. o);

        

         A11: 1 <= i1 by NAT_1: 11;

        then

         A12: i1 in ( dom f) by A10, FINSEQ_3: 25;

        ( Values o) = ( dom f) by Def7;

        then

        consider x,y be object such that

         A13: x in ( dom o) & y in ( dom (o . x)) & ((o . x) . y) = i1 by A11, A10, FINSEQ_3: 25, Th1;

        reconsider x, y as Nat by A13;

        set ox = (o . x), rox = ( rng ox);

        

         A14: ox in ( rng o) by A13, FUNCT_1:def 3;

        then

         A15: rox c= ( dom f) by RELAT_1:def 19;

        set C = ( canFS (rox \ {i1}));

        

         A16: i1 in rox by A13, FUNCT_1:def 3;

        

         A17: ( rng C) = (rox \ {i1}) by FUNCT_2:def 3;

        

         A18: ((rox \ {i1}) \/ {i1}) = rox by ZFMISC_1: 116, A16;

        

         A19: ( rng <*i1*>) = {i1} by FINSEQ_1: 38;

        then

         A20: ( rng (C ^ <*i1*>)) = rox by A18, A17, FINSEQ_1: 31;

        (C ^ <*i1*>) is one-to-one by XBOOLE_1: 79, FINSEQ_3: 91, A17, A19;

        then

        consider P be Permutation of ( dom ox) such that

         A21: (C ^ <*i1*>) = (ox * P) by A20, RFINSEQ: 26, RFINSEQ: 4;

        

         A22: ( rng C) c= rox by A17;

        

         A23: ( rng C) c= (( dom f) \ {i1}) by A17, A14, RELAT_1:def 19, XBOOLE_1: 33;

        

         A24: (( rng C) \/ (( dom f) \ {i1})) = (( dom f) \ {i1}) by A17, A15, XBOOLE_1: 33, XBOOLE_1: 12;

        

         A25: ( rng C) c= ( dom f) by A15, A17;

        

         A26: (( rng C) \/ (( dom f) \ rox)) = (( rng C) \/ (( dom f) \ (( rng C) \/ {i1}))) by A17, ZFMISC_1: 116, A16

        .= (( rng C) \/ ((( dom f) \ ( rng C)) /\ (( dom f) \ {i1}))) by XBOOLE_1: 53

        .= ((( rng C) \/ (( dom f) \ ( rng C))) /\ (( rng C) \/ (( dom f) \ {i1}))) by XBOOLE_1: 24

        .= (( dom f) /\ (( dom f) \ {i1})) by A25, XBOOLE_1: 45, A24

        .= (( dom f) \ {i1}) by XBOOLE_1: 28;

        ( dom f) = ( Seg i1) by A10, FINSEQ_1:def 3;

        then

         A27: (( dom f) \ {i1}) = ( Seg i) by FINSEQ_1: 10;

        set fi = (f | i);

        

         A28: ( len fi) = i by NAT_1: 11, A10, FINSEQ_1: 59;

        (( rng C) /\ ( dom f)) c= rox by A22;

        then

        reconsider oC = (o +* (x,C)) as DoubleReorganization of ( dom fi) by A27, A13, Th37, A26;

        set FO = (fi *. oC);

        

         A29: ( dom oC) = ( dom o) by FUNCT_7: 30;

        then

         A30: ( len oC) = ( len o) by FINSEQ_3: 29;

        

         A31: ( len FO) = ( len oC) by CARD_1:def 7;

        set FOx = (FO | x);

        consider H be FinSequence such that

         A32: FO = (FOx ^ H) by FINSEQ_1: 80;

        

         A33: 1 <= x & x <= ( len o) by A13, FINSEQ_3: 25;

        then

         A34: ( len FOx) = x by FINSEQ_1: 59, A30, A31;

        then

         A35: ( dom FOx) = ( Seg x) by FINSEQ_1:def 3;

        

         A36: x in ( Seg x) by A33;

        reconsider x1 = (x - 1) as Nat by A33;

        ( len FOx) = (x1 + 1) by A33, FINSEQ_1: 59, A30, A31;

        then

         A37: FOx = ((FOx | x1) ^ <*(FOx . x)*>) by FINSEQ_3: 55;

        

         A38: x1 <= (x1 + 1) by NAT_1: 11;

        then

         A39: (FOx | x1) = (FO | x1) by FINSEQ_1: 82;

        reconsider H as complex-functions-valued FinSequence-yielding FinSequence by A32, Th43, Th44;

        reconsider FF = <*(FO . x)*>, FOx1 = (FO | x1) as complex-functions-valued FinSequence-yielding FinSequence;

        ( Sum (FOx1 ^ FF)) = (( Sum FOx1) ^ ( Sum FF)) by Th46;

        then

         A40: ( Sum ( Sum (FOx1 ^ FF))) = (( Sum ( Sum FOx1)) + ( Sum ( Sum FF))) by RVSUM_2: 32;

        FO = ((FOx1 ^ FF) ^ H) by A39, A37, A35, A36, FUNCT_1: 47, A32;

        then

         A41: ( Sum FO) = (( Sum (FOx1 ^ FF)) ^ ( Sum H)) by Th46;

        

         A42: ( Sum FF) = <*( Sum (FO . x))*> by Th45;

        

         A43: ( len fo) = ( len o) by CARD_1:def 7;

        set fox = (fo | x);

        consider h be FinSequence such that

         A44: fo = (fox ^ h) by FINSEQ_1: 80;

        

         A45: ( len fox) = x by A33, FINSEQ_1: 59, A43;

        then

         A46: ( dom fox) = ( Seg x) by FINSEQ_1:def 3;

        ( len fox) = (x1 + 1) by A33, FINSEQ_1: 59, A43;

        then

         A47: fox = ((fox | x1) ^ <*(fox . x)*>) by FINSEQ_3: 55;

        

         A48: (fox | x1) = (fo | x1) by A38, FINSEQ_1: 82;

        reconsider h as complex-functions-valued FinSequence-yielding FinSequence by A44, Th43, Th44;

        reconsider ff = <*(fo . x)*>, fox1 = (fo | x1) as complex-functions-valued FinSequence-yielding FinSequence;

        ( Sum (fox1 ^ ff)) = (( Sum fox1) ^ ( Sum ff)) by Th46;

        then

         A49: ( Sum ( Sum (fox1 ^ ff))) = (( Sum ( Sum fox1)) + ( Sum ( Sum ff))) by RVSUM_2: 32;

        fo = ((fox1 ^ ff) ^ h) by A44, A47, A48, A46, A36, FUNCT_1: 47;

        then

         A50: ( Sum fo) = (( Sum (fox1 ^ ff)) ^ ( Sum h)) by Th46;

        

         A51: ( Sum ff) = <*( Sum (fo . x))*> by Th45;

        

         A52: ( len fox1) = x1 & ( len FOx1) = x1 by A38, A45, A34, A48, A39, FINSEQ_1: 59;

        for i st 1 <= i & i <= x1 holds (fox1 . i) = (FOx1 . i)

        proof

          let j;

          assume

           A53: 1 <= j & j <= x1;

          then

           A54: j < x by A38, NAT_1: 13;

          then

           A55: j <= ( len o) by A33, XXREAL_0: 2;

          then

           A56: j in ( dom o) by A53, FINSEQ_3: 25;

          

           A57: (fo . j) = (f * (o . j)) & (FO . j) = (fi * (oC . j)) by A55, A53, FINSEQ_3: 25, A29, FOMODEL2:def 6;

          j in ( Seg x1) by A53;

          then

           A58: (fox1 . j) = (fo . j) & (FOx1 . j) = (FO . j) by FUNCT_1: 49;

          (o . j) in ( rng o) & ( rng o) c= (( dom f) * ) by A56, FUNCT_1:def 3;

          then

           A59: (o . j) is FinSequence of ( dom f) by FINSEQ_1:def 11;

           not i1 in ( rng (o . j))

          proof

            assume i1 in ( rng (o . j));

            then

            consider w be object such that

             A60: w in ( dom (o . j)) & ((o . j) . w) = i1 by FUNCT_1:def 3;

            (o _ (j,w)) = (o _ (x,y)) by A60, A13;

            hence thesis by A60, A56, A13, Def6, A54;

          end;

          then

           A61: ( rng (o . j)) c= ( Seg i) by A27, A59, FINSEQ_1:def 4, ZFMISC_1: 34;

          ((f | ( Seg i)) * (o . j)) = ((f * ( id ( Seg i))) * (o . j)) by RELAT_1: 65

          .= (f * (( id ( Seg i)) * (o . j))) by RELAT_1: 36

          .= (f * (o . j)) by A61, RELAT_1: 53;

          hence thesis by A57, A54, FUNCT_7: 32, A58;

        end;

        then

         A62: fox1 = FOx1 by A52;

        

         A63: ( len FO) = (( len FOx) + ( len H)) by A32, FINSEQ_1: 22;

        then

         A64: (( len FOx) + ( len H)) = (( len fox) + ( len h)) by A44, FINSEQ_1: 22, A43, A31, A30;

        for i st 1 <= i & i <= ( len H) holds (H . i) = (h . i)

        proof

          let j;

          set jx = (j + x);

          assume

           A65: 1 <= j & j <= ( len H);

          then j in ( dom H) & j in ( dom h) by A64, A34, A45, FINSEQ_3: 25;

          then

           A66: (H . j) = (FO . jx) & (h . j) = (fo . jx) by A34, A45, A32, A44, FINSEQ_1:def 7;

          j <> 0 by A65;

          then

           A67: jx <> x;

          j <= jx by NAT_1: 11;

          then jx >= 1 by A65, XXREAL_0: 2;

          then

           A68: jx in ( dom o) by A65, A63, A34, A31, A29, XREAL_1: 6, FINSEQ_3: 25;

          then

           A69: (fo . jx) = (f * (o . jx)) & (FO . jx) = (fi * (oC . jx)) by A29, FOMODEL2:def 6;

          (o . jx) in ( rng o) & ( rng o) c= (( dom f) * ) by A68, FUNCT_1:def 3;

          then

           A70: (o . jx) is FinSequence of ( dom f) by FINSEQ_1:def 11;

           not i1 in ( rng (o . jx))

          proof

            assume i1 in ( rng (o . jx));

            then

            consider w be object such that

             A71: w in ( dom (o . jx)) & ((o . jx) . w) = i1 by FUNCT_1:def 3;

            (o _ (jx,w)) = (o _ (x,y)) by A71, A13;

            then jx = x & y = w by A71, A68, A13, Def6;

            then j = 0 ;

            hence thesis by A65;

          end;

          then

           A72: ( rng (o . jx)) c= ( Seg i) by A27, A70, FINSEQ_1:def 4, ZFMISC_1: 34;

          ((f | ( Seg i)) * (o . jx)) = ((f * ( id ( Seg i))) * (o . jx)) by RELAT_1: 65

          .= (f * (( id ( Seg i)) * (o . jx))) by RELAT_1: 36

          .= (f * (o . jx)) by A72, RELAT_1: 53;

          hence thesis by A69, A67, FUNCT_7: 32, A66;

        end;

        then

         A73: H = h by A64, A34, A45;

        

         A74: (fo . x) = (f * ox) & (FO . x) = (fi * (oC . x)) by A13, A29, FOMODEL2:def 6;

        

         A75: ( dom (f * ox)) = ( dom ox) by A15, RELAT_1: 27;

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

        then

        reconsider g = (f * ox) as FinSequence of COMPLEX by FINSEQ_1:def 4;

        reconsider PP = P as Permutation of ( dom g) by A75;

        

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

        ( rng P) = ( dom ox) by FUNCT_2:def 3;

        then

         A77: ( dom (ox * P)) = ( dom P) & ( rng (ox * P)) = ( rng ox) & ( dom (g * P)) = ( dom P) & ( rng (g * P)) = ( rng g) by A75, RELAT_1: 27, RELAT_1: 28;

        then (g * PP) is FinSequence by A76, FUNCT_2: 52, FINSEQ_1:def 2;

        then

        reconsider G = (g * PP) as FinSequence of COMPLEX by FINSEQ_1:def 4, A77;

        

         A78: ( Sum g) = ( addcomplex $$ g) by RVSUM_1:def 11

        .= ( addcomplex "**" G) by FINSOP_1: 7

        .= ( Sum G) by RVSUM_1:def 11;

        reconsider F = f as Function of ( dom f), ( rng f) by FUNCT_2: 1;

        reconsider I1 = i1 as Element of ( dom f) by A11, A10, FINSEQ_3: 25;

        reconsider C1 = C as FinSequence of ( dom f) by A25, FINSEQ_1:def 4;

        

         A79: ( dom f) is non empty & ( rng f) is non empty by A12, RELAT_1: 42;

        G = (f * (ox * P)) by RELAT_1: 36;

        then

         A80: G = ((F * C1) ^ <*(f . i1)*>) by A21, A79, A12, FINSEQOP: 8;

        (fi * C) = ((f * ( id ( Seg i))) * C) by RELAT_1: 65

        .= (f * (( id ( Seg i)) * C)) by RELAT_1: 36

        .= (f * C) by A23, A27, RELAT_1: 53;

        then (FO . x) = (f * C) by A74, A13, FUNCT_7: 31;

        then

         A81: ( Sum (fo . x)) = (( Sum (FO . x)) + (f . i1)) by A80, RVSUM_2: 31, A78, A74;

        

         A82: ( Sum fi) = ( Sum ( Sum FO)) by A9, A28

        .= ((( Sum ( Sum FOx1)) + ( Sum ( Sum FF))) + ( Sum ( Sum H))) by A41, A40, RVSUM_2: 32

        .= ((( Sum ( Sum fox1)) + ( Sum (FO . x))) + ( Sum ( Sum h))) by A62, A73, A42, RVSUM_2: 30;

        

         A83: ( Sum ( Sum fo)) = ((( Sum ( Sum fox1)) + ( Sum ( Sum ff))) + ( Sum ( Sum h))) by A49, A50, RVSUM_2: 32

        .= ((( Sum ( Sum fox1)) + ( Sum (fo . x))) + ( Sum ( Sum h))) by A51, RVSUM_2: 30

        .= (((( Sum ( Sum fox1)) + ( Sum (FO . x))) + ( Sum ( Sum h))) + (f . i1)) by A81;

        f = (fi ^ <*(f . i1)*>) by FINSEQ_3: 55, A10;

        hence thesis by RVSUM_2: 31, A83, A82;

      end;

      

       A84: P[i] from NAT_1:sch 2( A1, A8);

      let f be complex-valued FinSequence, o be DoubleReorganization of ( dom f);

       P[( len f)] by A84;

      hence thesis;

    end;

    registration

      cluster ( NAT * ) -> natural-functions-membered;

      coherence

      proof

        for x be object st x in ( NAT * ) holds x is natural-valued Function;

        hence thesis by VALUED_2:def 7;

      end;

      cluster ( COMPLEX * ) -> complex-functions-membered;

      coherence

      proof

        for x be object st x in ( COMPLEX * ) holds x is complex-valued Function;

        hence thesis by VALUED_2:def 2;

      end;

    end

    theorem :: FLEXARY1:48

    for f be FinSequence of ( COMPLEX * ) holds ( Sum (( COMPLEX -concatenation ) "**" f)) = ( Sum ( Sum f))

    proof

      set CC = ( COMPLEX -concatenation );

      defpred P[ Nat] means for f be FinSequence of ( COMPLEX * ) st ( len f) = $1 holds ( Sum (CC "**" f)) = ( Sum ( Sum f));

      

       A1: CC is having_a_unity & ( the_unity_wrt CC) = {} by MONOID_0: 67;

      

       A2: P[ 0 ]

      proof

        let f be FinSequence of ( COMPLEX * );

        assume

         A3: ( len f) = 0 ;

        then ( Sum f) = {} ;

        hence thesis by A1, A3, FINSOP_1:def 1;

      end;

      

       A4: P[i] implies P[(i + 1)]

      proof

        assume

         A5: P[i];

        set i1 = (i + 1);

        let f be FinSequence of ( COMPLEX * );

        assume

         A6: ( len f) = i1;

        then

        consider q be FinSequence of ( COMPLEX * ), d be Element of ( COMPLEX * ) such that

         A7: f = (q ^ <*d*>) by FINSEQ_2: 19;

        (( len q) + 1) = ( len f) by A7, FINSEQ_2: 16;

        then

         A8: ( Sum ( Sum q)) = ( Sum (CC "**" q)) by A6, A5;

        ( Sum f) = (( Sum q) ^ ( Sum <*d*>)) by A7, Th46

        .= (( Sum q) ^ <*( Sum d)*>) by Th45;

        then

         A9: ( Sum ( Sum f)) = (( Sum ( Sum q)) + ( Sum d)) by RVSUM_2: 31;

        (CC "**" f) = ((CC "**" q) ^ (CC "**" <*d*>)) by Th3, A7

        .= ((CC "**" q) ^ d) by FINSOP_1: 11;

        hence thesis by RVSUM_2: 32, A8, A9;

      end;

       P[i] from NAT_1:sch 2( A2, A4);

      hence thesis;

    end;

    definition

      let f be finite Function;

      :: FLEXARY1:def9

      mode valued_reorganization of f -> DoubleReorganization of ( dom f) means

      : Def9: (for n holds ex x st x = (f . (it _ (n,1))) & ... & x = (f . (it _ (n,( len (it . n)))))) & for n1,n2,i1,i2 be Nat st i1 in ( dom (it . n1)) & i2 in ( dom (it . n2)) & (f . (it _ (n1,i1))) = (f . (it _ (n2,i2))) holds n1 = n2;

      existence

      proof

        per cases ;

          suppose

           A1: f = {} ;

          take o = the DoubleReorganization of ( dom f);

          thus for n holds ex x st x = (f . (o _ (n,1))) & ... & x = (f . (o _ (n,( len (o . n)))))

          proof

            let n;

            take x = {} ;

            thus thesis by A1;

          end;

          let n1,n2,i1,i2 be Nat;

          thus thesis by A1;

        end;

          suppose f <> {} ;

          then

          reconsider F = ( rng f) as non empty finite set;

          set c = the one-to-one onto FinSequence of F;

          

           A2: ( rng c) = F by FUNCT_2:def 3;

          then

          reconsider C = c as non empty FinSequence;

          consider o be ( len C) -element DoubleReorganization of ( dom f) such that

           A3: for n holds (c . n) = (f . (o _ (n,1))) & ... & (c . n) = (f . (o _ (n,( len (o . n))))) by Th38, A2;

          take o;

          thus for n holds ex x st x = (f . (o _ (n,1))) & ... & x = (f . (o _ (n,( len (o . n)))))

          proof

            let n;

            take x = (c . n);

            let i;

            assume

             A4: 1 <= i & i <= ( len (o . n));

            (c . n) = (f . (o _ (n,1))) & ... & (c . n) = (f . (o _ (n,( len (o . n))))) by A3;

            hence thesis by A4;

          end;

          let n1,n2,i1,i2 be Nat such that

           A5: i1 in ( dom (o . n1)) & i2 in ( dom (o . n2)) & (f . (o _ (n1,i1))) = (f . (o _ (n2,i2)));

          

           A6: (c . n1) = (f . (o _ (n1,1))) & ... & (c . n1) = (f . (o _ (n1,( len (o . n1))))) by A3;

          

           A7: (c . n2) = (f . (o _ (n2,1))) & ... & (c . n2) = (f . (o _ (n2,( len (o . n2))))) by A3;

          1 <= i1 & i1 <= ( len (o . n1)) by A5, FINSEQ_3: 25;

          then

           A8: (c . n1) = (f . (o _ (n1,i1))) by A6;

          

           A9: 1 <= i2 & i2 <= ( len (o . n2)) by A5, FINSEQ_3: 25;

          ( len o) = ( len C) by CARD_1:def 7;

          then

           A10: ( dom o) = ( dom c) by FINSEQ_3: 29;

          

           A11: n1 in ( dom o)

          proof

            assume not n1 in ( dom o);

            then (o . n1) = {} by FUNCT_1:def 2;

            hence thesis by A5;

          end;

          n2 in ( dom o)

          proof

            assume not n2 in ( dom o);

            then (o . n2) = {} by FUNCT_1:def 2;

            hence thesis by A5;

          end;

          hence n1 = n2 by FUNCT_1:def 4, A9, A7, A5, A8, A11, A10;

        end;

      end;

    end

    theorem :: FLEXARY1:49

    for f be finite Function holds for o be valued_reorganization of f holds ( rng ((f *. o) . n)) = {} or (( rng ((f *. o) . n)) = {(f . (o _ (n,1)))} & 1 in ( dom (o . n)))

    proof

      let f be finite Function;

      let o be valued_reorganization of f;

      assume ( rng ((f *. o) . n)) <> {} ;

      then

      consider y such that

       A1: y in ( rng ((f *. o) . n)) by XBOOLE_0:def 1;

      consider x such that

       A2: x in ( dom ((f *. o) . n)) & (((f *. o) . n) . x) = y by A1, FUNCT_1:def 3;

      reconsider x as Nat by A2;

      

       A3: ( dom (f *. o)) = ( dom o) by FOMODEL2:def 6;

      n in ( dom (f *. o))

      proof

        assume not n in ( dom (f *. o));

        then ((f *. o) . n) = {} by FUNCT_1:def 2;

        hence thesis by A1;

      end;

      then ((f *. o) . n) = (f * (o . n)) by A3, FOMODEL2:def 6;

      then

       A4: ((f * (o . n)) . x) = (f . ((o . n) . x)) & x in ( dom (o . n)) by A2, FUNCT_1: 11, FUNCT_1: 12;

      consider w be object such that

       A5: w = (f . (o _ (n,1))) & ... & w = (f . (o _ (n,( len (o . n))))) by Def9;

      1 <= x & x <= ( len (o . n)) by A4, FINSEQ_3: 25;

      then

       A6: w = (f . (o _ (n,x))) & 1 <= ( len (o . n)) by XXREAL_0: 2, A5;

      ( rng ((f *. o) . n)) c= {(f . (o _ (n,1)))}

      proof

        let z be object;

        assume

         A7: z in ( rng ((f *. o) . n));

        then

        consider x such that

         A8: x in ( dom ((f *. o) . n)) & (((f *. o) . n) . x) = z by FUNCT_1:def 3;

        reconsider x as Nat by A8;

        

         A9: ( dom (f *. o)) = ( dom o) by FOMODEL2:def 6;

        n in ( dom (f *. o))

        proof

          assume not n in ( dom (f *. o));

          then ((f *. o) . n) = {} by FUNCT_1:def 2;

          hence thesis by A7;

        end;

        then

         A10: ((f *. o) . n) = (f * (o . n)) by A9, FOMODEL2:def 6;

        then

         A11: ((f * (o . n)) . x) = (f . ((o . n) . x)) & x in ( dom (o . n)) by A8, FUNCT_1: 11, FUNCT_1: 12;

        then 1 <= x & x <= ( len (o . n)) by FINSEQ_3: 25;

        then w = (f . (o _ (n,x))) & 1 <= ( len (o . n)) by XXREAL_0: 2, A5;

        then z = (f . (o _ (n,1))) by A5, A8, A11, A10;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by A6, FINSEQ_3: 25, ZFMISC_1: 33;

    end;

    

     Lm7: for f be FinSequence holds for o1,o2 be valued_reorganization of f st ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i)) holds ( rng (o1 . i)) c= ( rng (o2 . i))

    proof

      let f be FinSequence;

      let o1,o2 be valued_reorganization of f such that

       A1: ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i));

      ( len ((f *. o1) . i)) = ( len (o1 . i)) by CARD_1:def 7;

      then

       A2: ( dom (o1 . i)) = ( dom ((f *. o1) . i)) by FINSEQ_3: 29;

      

       A3: ( len ((f *. o2) . i)) = ( len (o2 . i)) by CARD_1:def 7;

      

       A4: ( Values o1) = ( dom f) & ( Values o2) = ( dom f) by Def7;

      let y be object;

      assume y in ( rng (o1 . i));

      then

      consider x be object such that

       A5: x in ( dom (o1 . i)) & ((o1 . i) . x) = y by FUNCT_1:def 3;

      reconsider x as Nat by A5;

      (((f *. o1) . i) . x) in ( rng ((f *. o2) . i)) by A2, A5, FUNCT_1:def 3, A1;

      then

      consider u be object such that

       A6: u in ( dom ((f *. o2) . i)) & (((f *. o2) . i) . u) = (((f *. o1) . i) . x) by FUNCT_1:def 3;

      

       A7: ((f *. o1) _ (i,x)) = (f . (o1 _ (i,x))) by Th42;

      

       A8: ((f *. o2) _ (i,u)) = (f . (o2 _ (i,u))) by Th42;

      i in ( dom o1)

      proof

        assume not i in ( dom o1);

        then (o1 . i) = {} by FUNCT_1:def 2;

        hence thesis by A5;

      end;

      then

      consider j,w be object such that

       A9: j in ( dom o2) & w in ( dom (o2 . j)) & ((o2 . j) . w) = y by Th1, A5, A4;

      

       A10: u in ( dom (o2 . i)) by A6, A3, FINSEQ_3: 29;

      (f . (o2 _ (i,u))) = (f . (o2 _ (j,w))) by A5, A9, A6, A7, A8;

      then j = i by Def9, A10, A9;

      hence thesis by A9, FUNCT_1:def 3;

    end;

    theorem :: FLEXARY1:50

    for f be FinSequence holds for o1,o2 be valued_reorganization of f st ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i)) holds ( rng (o1 . i)) = ( rng (o2 . i)) by Lm7;

    theorem :: FLEXARY1:51

    for f be FinSequence, g be complex-valued FinSequence holds for o1,o2 be DoubleReorganization of ( dom g) st o1 is valued_reorganization of f & o2 is valued_reorganization of f & ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i)) holds (( Sum (g *. o1)) . i) = (( Sum (g *. o2)) . i)

    proof

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

      let o1,o2 be DoubleReorganization of ( dom g) such that

       A1: o1 is valued_reorganization of f & o2 is valued_reorganization of f & ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i));

      

       A2: ( rng (o1 . i)) = ( rng (o2 . i)) by A1, Lm7;

      then

      consider h be Function such that

       A3: ( dom h) = ( dom (o1 . i)) & ( rng h) = ( dom (o2 . i)) & h is one-to-one & ((o2 . i) * h) = (o1 . i) by RFINSEQ: 26, CLASSES1: 77;

      ( rng ((g *. o1) . i)) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider g1 = ((g *. o1) . i) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      ( rng ((g *. o2) . i)) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider g2 = ((g *. o2) . i) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      ( len (o1 . i)) = ( len (o2 . i)) by A2, FINSEQ_1: 48;

      then

       A4: ( dom (o1 . i)) = ( dom (o2 . i)) by FINSEQ_3: 29;

      

       A5: ( len ((g *. o2) . i)) = ( len (o2 . i)) by CARD_1:def 7;

      then ( dom g2) = ( dom (o2 . i)) by FINSEQ_3: 29;

      then

      reconsider h as Function of ( dom g2), ( dom g2) by A3, A4, FUNCT_2: 1;

      h is onto by A3, A5, FINSEQ_3: 29, FUNCT_2:def 3;

      then

      reconsider h as Permutation of ( dom g2) by A3;

      

       A6: g1 = (g * (o1 . i)) by Th41

      .= ((g * (o2 . i)) * h) by A3, RELAT_1: 36

      .= (g2 * h) by Th41;

      

      thus (( Sum (g *. o1)) . i) = ( Sum ((g *. o1) . i)) by Def8

      .= ( addcomplex "**" g1) by RVSUM_1:def 11

      .= ( addcomplex "**" g2) by A6, FINSOP_1: 7

      .= ( Sum ((g *. o2) . i)) by RVSUM_1:def 11

      .= (( Sum (g *. o2)) . i) by Def8;

    end;