eulrpart.miz



    begin

    reserve x,y for object,

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

    registration

      let r be ext-real number;

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

      coherence

      proof

        

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

         {r} c= ExtREAL by XXREAL_0:def 1;

        hence thesis by A1, VALUED_0:def 2;

      end;

      cluster <*r*> -> decreasing increasing non-decreasing non-increasing;

      coherence ;

    end

    theorem :: EULRPART:1

    

     Th1: for f,g be non-decreasing ext-real-valued FinSequence st (f . ( len f)) <= (g . 1) holds (f ^ g) is non-decreasing

    proof

      let f,g be non-decreasing ext-real-valued FinSequence such that

       A1: (f . ( len f)) <= (g . 1);

      set fg = (f ^ g);

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

      proof

        let e1,e2 be ExtReal such that

         A2: e1 in ( dom fg) & e2 in ( dom fg) & e1 <= e2;

        per cases ;

          suppose

           A3: e1 in ( dom f) & e2 in ( dom f);

          then (fg . e1) = (f . e1) & (fg . e2) = (f . e2) by FINSEQ_1:def 7;

          hence thesis by A2, A3, VALUED_0:def 15;

        end;

          suppose

           A4: e1 in ( dom f) & not e2 in ( dom f);

          then

          consider i such that

           A5: i in ( dom g) & e2 = (( len f) + i) by A2, FINSEQ_1: 25;

          

           A6: 1 <= e1 & e1 <= ( len f) & 1 <= i & i <= ( len g) by A4, A5, FINSEQ_3: 25;

          then 1 <= ( len f) & 1 <= ( len g) by XXREAL_0: 2;

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

          then

           A7: (f . e1) <= (f . ( len f)) & (g . 1) <= (g . i) by VALUED_0:def 15, A4, A5, A6;

          then

           A8: (f . e1) <= (g . 1) by A1, XXREAL_0: 2;

          (fg . e1) = (f . e1) & (fg . e2) = (g . i) by A5, A4, FINSEQ_1:def 7;

          hence thesis by A8, A7, XXREAL_0: 2;

        end;

          suppose not e1 in ( dom f) & e2 in ( dom f);

          then not (1 <= e1 & e1 <= ( len f)) & e2 <= ( len f) & 1 <= e1 by A2, FINSEQ_3: 25;

          hence thesis by XXREAL_0: 2, A2;

        end;

          suppose

           A9: not e1 in ( dom f) & not e2 in ( dom f);

          then

          consider i such that

           A10: i in ( dom g) & e1 = (( len f) + i) by A2, FINSEQ_1: 25;

          consider j such that

           A11: j in ( dom g) & e2 = (( len f) + j) by A2, FINSEQ_1: 25, A9;

          (fg . e1) = (g . i) & (fg . e2) = (g . j) by A10, A11, FINSEQ_1:def 7;

          hence thesis by A10, A2, A11, XREAL_1: 6, VALUED_0:def 15;

        end;

      end;

      hence thesis by VALUED_0:def 15;

    end;

    definition

      let R be Relation;

      :: EULRPART:def1

      attr R is odd-valued means

      : Def1: ( rng R) c= OddNAT ;

    end

    theorem :: EULRPART:2

    

     Th2: n in OddNAT iff n is odd

    proof

      thus n in OddNAT implies n is odd

      proof

        assume n in OddNAT ;

        then ex i be Element of NAT st n = ((2 * i) + 1) by FIB_NUM2:def 4;

        hence thesis;

      end;

      assume n is odd;

      then

      consider i such that

       A1: n = ((2 * i) + 1) by ABIAN: 9;

      i in NAT by ORDINAL1:def 12;

      hence thesis by A1, FIB_NUM2:def 4;

    end;

    registration

      cluster odd-valued -> non-zero natural-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is odd-valued;

         OddNAT c= NAT ;

        then

         A2: ( rng R) c= NAT by A1;

         not 0 in ( rng R)

        proof

          assume 0 in ( rng R);

          then 0 is odd by A1, Th2;

          hence thesis;

        end;

        hence thesis by ORDINAL1:def 15, A2, VALUED_0:def 6;

      end;

    end

    definition

      let F be Function;

      :: original: odd-valued

      redefine

      :: EULRPART:def2

      attr F is odd-valued means

      : Def2: for x st x in ( dom F) holds (F . x) is odd Nat;

      compatibility

      proof

        thus F is odd-valued implies for x st x in ( dom F) holds (F . x) is odd Nat

        proof

          assume

           A1: F is odd-valued;

          let x;

          assume x in ( dom F);

          then (F . x) in ( rng F) by FUNCT_1:def 3;

          then (F . x) in OddNAT by A1;

          then ex k be Element of NAT st (F . x) = ((2 * k) + 1) by FIB_NUM2:def 4;

          hence thesis;

        end;

        assume

         A2: for x st x in ( dom F) holds (F . x) is odd Nat;

        ( rng F) c= OddNAT

        proof

          let y;

          assume y in ( rng F);

          then

          consider x such that

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

          (F . x) is odd Nat by A2, A3;

          then

          consider i such that

           A4: (F . x) = ((2 * i) + 1) by ABIAN: 9;

          i in NAT by ORDINAL1:def 12;

          hence thesis by FIB_NUM2:def 4, A3, A4;

        end;

        hence thesis;

      end;

    end

    registration

      cluster empty -> odd-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume R is empty;

        then ( rng R) c= OddNAT ;

        hence thesis;

      end;

      let i be odd Nat;

      cluster <*i*> -> odd-valued;

      coherence

      proof

         {i} c= OddNAT by Th2, ZFMISC_1: 31;

        hence thesis by FINSEQ_1: 38;

      end;

    end

    registration

      let f,g be odd-valued FinSequence;

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

      coherence

      proof

        

         A1: ( rng f) c= OddNAT & ( rng g) c= OddNAT by Def1;

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

        hence thesis by A1, XBOOLE_1: 8;

      end;

    end

    registration

      cluster OddNAT -valued -> odd-valued for Relation;

      coherence by RELAT_1:def 19;

    end

    definition

      let n be Nat;

      :: EULRPART:def3

      mode a_partition of n -> non-zero non-decreasing natural-valued FinSequence means

      : Def3: ( Sum it ) = n;

      existence

      proof

        per cases ;

          suppose n <> 0 ;

          then not 0 in ( rng <*n*>);

          then

           A1: <*n*> is non-zero by ORDINAL1:def 15;

          ( Sum <*n*>) = n by RVSUM_1: 73;

          hence thesis by A1;

        end;

          suppose n = 0 ;

          hence thesis by RVSUM_1: 72;

        end;

      end;

    end

    theorem :: EULRPART:3

     {} is a_partition of 0 by RVSUM_1: 72, Def3;

    registration

      let n be Nat;

      cluster odd-valued for a_partition of n;

      existence

      proof

        per cases ;

          suppose n = 0 ;

          then

          reconsider N = {} as a_partition of n by RVSUM_1: 72, Def3;

          N is odd-valued;

          hence thesis;

        end;

          suppose

           A1: n is odd;

          ( Sum <*n*>) = n by RVSUM_1: 73;

          then <*n*> is a_partition of n by Def3, A1;

          hence thesis by A1;

        end;

          suppose

           A2: n is even & n <> 0 ;

          then

          consider i such that

           A3: n = (2 * i) by ABIAN:def 2;

          i <> 0 by A2, A3;

          then

          reconsider i1 = (i - 1) as Nat;

          

           A4: (((i1 * 2) + 1) + 1) = n by A3;

          

           A5: 1 = (1 + (2 * 0 ));

          reconsider N1 = <*1*>, N2 = <*((i1 * 2) + 1)*> as non-decreasing natural-valued FinSequence;

          ( len N1) = 1 by FINSEQ_1: 39;

          then (N1 . ( len N1)) = 1 & (N2 . 1) = ((i1 * 2) + 1) by FINSEQ_1: 40;

          then

           A6: (N1 ^ N2) is non-decreasing by NAT_1: 11, Th1;

          ( rng <*1, ((i1 * 2) + 1)*>) = {1, ((i1 * 2) + 1)} by FINSEQ_2: 127;

          then

           A7: <*1, ((i1 * 2) + 1)*> is non-zero;

          (N1 ^ N2) = <*1, ((i1 * 2) + 1)*>;

          then ( Sum (N1 ^ N2)) = n by RVSUM_1: 77, A4;

          then

          reconsider N = (N1 ^ N2) as a_partition of n by A7, A6, Def3;

          N is odd-valued by A5;

          hence thesis;

        end;

      end;

      cluster one-to-one for a_partition of n;

      existence

      proof

        per cases ;

          suppose n = 0 ;

          then

          reconsider N = {} as a_partition of n by RVSUM_1: 72, Def3;

          N is one-to-one;

          hence thesis;

        end;

          suppose n <> 0 ;

          then not 0 in ( rng <*n*>);

          then

           A8: <*n*> is non-zero by ORDINAL1:def 15;

          ( Sum <*n*>) = n by RVSUM_1: 73;

          then

          reconsider N = <*n*> as a_partition of n by A8, Def3;

          N is one-to-one;

          hence thesis;

        end;

      end;

    end

    registration

      let n be Nat;

      sethood of a_partition of n

      proof

        take N = ( NAT * );

        let p be a_partition of n;

        ( rng p) c= NAT by VALUED_0:def 6;

        then p is FinSequence of NAT by FINSEQ_1:def 4;

        hence thesis by FINSEQ_1:def 11;

      end;

    end

    definition

      let f be odd-valued FinSequence;

      :: EULRPART:def4

      mode odd_organization of f -> valued_reorganization of f means

      : Def4: ((2 * n) - 1) = (f . (it _ (n,1))) & ... & ((2 * n) - 1) = (f . (it _ (n,( len (it . n)))));

      existence

      proof

        

         A1: ( rng f) c= NAT by VALUED_0:def 6;

         {1} c= NAT by ZFMISC_1: 31;

        then

        reconsider D = (( rng f) \/ {1}) as finite non empty Subset of NAT by A1, XBOOLE_1: 8;

        set m = ( max D);

        deffunc G( Nat) = ((2 * $1) -' 1);

        consider g be FinSequence of NAT such that

         A2: ( len g) = (m + 1) & for j st j in ( dom g) holds (g . j) = G(j) from FINSEQ_2:sch 1;

        reconsider g as non empty FinSequence of NAT by A2;

        ( rng f) c= ( rng g)

        proof

          let y;

          assume

           A3: y in ( rng f);

          then

          consider x such that

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

          reconsider n = y as odd Nat by A4, Def2;

          consider i such that

           A5: ((2 * i) + 1) = n by ABIAN: 9;

          n in D by A3, XBOOLE_0:def 3;

          then

           A6: n <= m by XXREAL_2:def 8;

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

          then ((2 * i) + 1) <= ((2 * m) + 1) by A6, A5, XXREAL_0: 2;

          then (2 * i) <= (2 * m) by XREAL_1: 6;

          then i <= m by XREAL_1: 68;

          then

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

          then

           A8: (i + 1) in ( dom g) by A2, FINSEQ_3: 25;

          

           A9: (g . (i + 1)) = ((2 * (i + 1)) -' 1) by A7, A2, FINSEQ_3: 25;

          (2 * 1) <= (2 * (i + 1)) by NAT_1: 11, XREAL_1: 64;

          then (g . (i + 1)) = ((2 * (i + 1)) - 1) by XXREAL_0: 2, A9, XREAL_1: 233;

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

        end;

        then

        consider o be ( len g) -element DoubleReorganization of ( dom f) such that

         A10: (o . n) is increasing & ((g . n) = (f . (o _ (n,1))) & ... & (g . n) = (f . (o _ (n,( len (o . n)))))) by FLEXARY1: 39;

        o is valued_reorganization of f

        proof

          thus for n holds ex x st x = (f . (o _ (n,1))) & ... & x = (f . (o _ (n,( len (o . n)))))

          proof

            let n;

            (g . n) = (f . (o _ (n,1))) & ... & (g . n) = (f . (o _ (n,( len (o . n))))) by A10;

            hence thesis;

          end;

          let n1,n2,i1,i2 be Nat such that

           A11: i1 in ( dom (o . n1)) & i2 in ( dom (o . n2)) & (f . (o _ (n1,i1))) = (f . (o _ (n2,i2)));

          

           A12: (g . n1) = (f . (o _ (n1,1))) & ... & (g . n1) = (f . (o _ (n1,( len (o . n1))))) by A10;

          1 <= i1 & i1 <= ( len (o . n1)) by A11, FINSEQ_3: 25;

          then

           A13: (g . n1) = (f . (o _ (n1,i1))) by A12;

          

           A14: (g . n2) = (f . (o _ (n2,1))) & ... & (g . n2) = (f . (o _ (n2,( len (o . n2))))) by A10;

          1 <= i2 & i2 <= ( len (o . n2)) by A11, FINSEQ_3: 25;

          then

           A15: (g . n1) = (g . n2) by A14, A11, A13;

          ( len o) = ( len g) by CARD_1:def 7;

          then

           A16: ( dom o) = ( dom g) by FINSEQ_3: 29;

          

           A17: n1 in ( dom g)

          proof

            assume not n1 in ( dom g);

            then (o . n1) = {} by A16, FUNCT_1:def 2;

            hence thesis by A11;

          end;

          then

           A18: (g . n1) = G(n1) by A2;

          

           A19: n2 in ( dom g)

          proof

            assume not n2 in ( dom g);

            then (o . n2) = {} by A16, FUNCT_1:def 2;

            hence thesis by A11;

          end;

          then

           A20: G(n1) = G(n2) by A2, A18, A15;

          (2 * 1) <= (2 * n1) by A17, FINSEQ_3: 25, XREAL_1: 64;

          then

           A21: ((2 * n1) -' 1) = ((2 * n1) - 1) by XXREAL_0: 2, XREAL_1: 233;

          (2 * 1) <= (2 * n2) by A19, FINSEQ_3: 25, XREAL_1: 64;

          then ((2 * n2) -' 1) = ((2 * n2) - 1) by XXREAL_0: 2, XREAL_1: 233;

          hence n1 = n2 by A20, A21;

        end;

        then

        reconsider o as valued_reorganization of f;

        take o;

        for n holds ((2 * n) - 1) = (f . (o _ (n,1))) & ... & ((2 * n) - 1) = (f . (o _ (n,( len (o . n)))))

        proof

          let n;

          let i such that

           A22: 1 <= i & i <= ( len (o . n));

          

           A23: (g . n) = (f . (o _ (n,1))) & ... & (g . n) = (f . (o _ (n,( len (o . n))))) by A10;

          ( len o) = ( len g) by CARD_1:def 7;

          then

           A24: ( dom o) = ( dom g) by FINSEQ_3: 29;

          (o . n) <> {} by A22;

          then n in ( dom o) by FUNCT_1:def 2;

          then

           A25: 1 <= n & n <= ( len o) & (g . n) = G(n) by A24, A2, FINSEQ_3: 25;

          then (2 * 1) <= (2 * n) by XREAL_1: 64;

          then ((2 * n) -' 1) = ((2 * n) - 1) by XXREAL_0: 2, XREAL_1: 233;

          hence thesis by A23, A22, A25;

        end;

        hence thesis;

      end;

    end

    theorem :: EULRPART:4

    

     Th4: for f be odd-valued FinSequence holds for o be DoubleReorganization of ( dom f) st for n holds ((2 * n) - 1) = (f . (o _ (n,1))) & ... & ((2 * n) - 1) = (f . (o _ (n,( len (o . n))))) holds o is odd_organization of f

    proof

      let f be odd-valued FinSequence;

      let o be DoubleReorganization of ( dom f) such that

       A1: for n holds ((2 * n) - 1) = (f . (o _ (n,1))) & ... & ((2 * n) - 1) = (f . (o _ (n,( len (o . n)))));

      

       A2: for n holds ex x st x = (f . (o _ (n,1))) & ... & x = (f . (o _ (n,( len (o . n)))))

      proof

        let n;

        take x = ((2 * n) - 1);

        thus thesis by A1;

      end;

      for n1,n2,i1,i2 be Nat st i1 in ( dom (o . n1)) & i2 in ( dom (o . n2)) & (f . (o _ (n1,i1))) = (f . (o _ (n2,i2))) holds n1 = n2

      proof

        let n1,n2,i1,i2 be Nat such that

         A3: i1 in ( dom (o . n1)) & i2 in ( dom (o . n2)) & (f . (o _ (n1,i1))) = (f . (o _ (n2,i2)));

        

         A4: ((2 * n1) - 1) = (f . (o _ (n1,1))) & ... & ((2 * n1) - 1) = (f . (o _ (n1,( len (o . n1))))) by A1;

        1 <= i1 & i1 <= ( len (o . n1)) by A3, FINSEQ_3: 25;

        then

         A5: (f . (o _ (n1,i1))) = ((2 * n1) - 1) by A4;

        

         A6: ((2 * n2) - 1) = (f . (o _ (n2,1))) & ... & ((2 * n2) - 1) = (f . (o _ (n2,( len (o . n2))))) by A1;

        1 <= i2 & i2 <= ( len (o . n2)) by A3, FINSEQ_3: 25;

        then ((2 * n2) - 1) = ((2 * n1) - 1) by A6, A5, A3;

        hence thesis;

      end;

      then o is valued_reorganization of f by A2, FLEXARY1:def 9;

      hence thesis by A1, Def4;

    end;

    theorem :: EULRPART:5

    

     Th5: for f be odd-valued FinSequence, g be complex-valued FinSequence holds for o1,o2 be DoubleReorganization of ( dom g) st o1 is odd_organization of f & o2 is odd_organization of f holds (( Sum (g *. o1)) . i) = (( Sum (g *. o2)) . i)

    proof

      let f be odd-valued FinSequence, g be complex-valued FinSequence;

      

       A1: for o1,o2 be DoubleReorganization of ( dom g) st o1 is odd_organization of f & o2 is odd_organization of f holds ( rng ((f *. o1) . n)) c= ( rng ((f *. o2) . n))

      proof

        let o1,o2 be DoubleReorganization of ( dom g) such that

         A2: o1 is odd_organization of f & o2 is odd_organization of f;

        reconsider O1 = o1 as odd_organization of f by A2;

        let y be object;

        assume

         A3: y in ( rng ((f *. o1) . n));

        then

         A4: ( rng ((f *. o1) . n)) = {(f . (o1 _ (n,1)))} & 1 in ( dom (o1 . n)) by FLEXARY1: 49, A2;

        

         A5: n in ( dom o1)

        proof

          assume not n in ( dom o1);

          then (o1 . n) = {} by FUNCT_1:def 2;

          hence thesis by A3, FLEXARY1: 49, A2;

        end;

        then ((o1 . n) . 1) in ( Values o1) by FLEXARY1: 1, A4;

        then ((o1 . n) . 1) in ( dom f) by FLEXARY1:def 7, A2;

        then ((o1 . n) . 1) in ( Values o2) by FLEXARY1:def 7, A2;

        then

        consider j,w be object such that

         A6: j in ( dom o2) & w in ( dom (o2 . j)) & ((o2 . j) . w) = ((o1 . n) . 1) by FLEXARY1: 1;

        reconsider j, w as Nat by A6;

        

         A7: ((f *. o1) . n) = (f * (o1 . n)) by A5, FOMODEL2:def 6;

        ( len ((f *. O1) . n)) = ( len (o1 . n)) by CARD_1:def 7;

        then

         A8: ( dom ((f *. o1) . n)) = ( dom (o1 . n)) by FINSEQ_3: 29;

        

         A9: ((2 * n) - 1) = (f . (o1 _ (n,1))) & ... & ((2 * n) - 1) = (f . (o1 _ (n,( len (o1 . n))))) by A2, Def4;

        

         A10: 1 <= ( len (o1 . n)) by A4, FINSEQ_3: 25;

        

         A11: ((2 * j) - 1) = (f . (o2 _ (j,1))) & ... & ((2 * j) - 1) = (f . (o2 _ (j,( len (o2 . j))))) by A2, Def4;

        1 <= w & w <= ( len (o2 . j)) by A6, FINSEQ_3: 25;

        then ((2 * j) - 1) = (f . (o2 _ (j,w))) by A11;

        then

         A12: ((2 * j) - 1) = ((2 * n) - 1) by A6, A10, A9;

        then

         A13: y = (f . (o2 _ (n,w))) by A4, A3, TARSKI:def 1, A6;

        

         A14: ((f *. o2) _ (n,w)) = (f . (o2 _ (n,w))) by FLEXARY1: 42;

        

         A15: ((o2 . n) . w) in ( dom f) by A8, A4, A7, FUNCT_1: 11, A6, A12;

        ((f *. o2) . n) = (f * (o2 . n)) by A12, A6, FOMODEL2:def 6;

        then w in ( dom ((f *. o2) . n)) by A15, A6, A12, FUNCT_1: 11;

        hence thesis by FUNCT_1:def 3, A13, A14;

      end;

      let o1,o2 be DoubleReorganization of ( dom g) such that

       A16: o1 is odd_organization of f & o2 is odd_organization of f;

      ( rng ((f *. o1) . i)) = ( rng ((f *. o2) . i)) by A1, A16;

      hence thesis by A16, FLEXARY1: 51;

    end;

    theorem :: EULRPART:6

    

     Th6: for p be a_partition of n holds ex O be odd-valued FinSequence, a be natural-valued FinSequence st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) & ((p . 1) = ((O . 1) * (2 |^ (a . 1))) & ... & (p . ( len p)) = ((O . ( len p)) * (2 |^ (a . ( len p)))))

    proof

      let p be a_partition of n;

      defpred P[ object, object] means for i, j st (p . $1) = ((2 |^ i) * ((2 * j) + 1)) holds $2 = [((2 * j) + 1), i];

      

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

      

       A2: for k st k in ( Seg ( len p)) holds ex x st P[k, x]

      proof

        let k;

        assume k in ( Seg ( len p));

        then (p . k) in ( rng p) by FUNCT_1:def 3, A1;

        then

        consider n,m be Nat such that

         A3: (p . k) = ((2 |^ n) * ((2 * m) + 1)) by NAGATA_2: 1;

        take x = [((2 * m) + 1), n];

        let i, j;

        assume (p . k) = ((2 |^ i) * ((2 * j) + 1));

        then i = n & j = m by A3, CARD_4: 4;

        hence thesis;

      end;

      consider Oa be FinSequence such that

       A4: ( dom Oa) = ( Seg ( len p)) & for k st k in ( Seg ( len p)) holds P[k, (Oa . k)] from FINSEQ_1:sch 1( A2);

      deffunc P1( object) = ((Oa . $1) `1 );

      consider O be FinSequence such that

       A5: ( len O) = ( len p) & for k st k in ( dom O) holds (O . k) = P1(k) from FINSEQ_1:sch 2;

      

       A6: ( dom O) = ( dom p) by FINSEQ_3: 29, A5;

      for x st x in ( dom O) holds (O . x) is odd Nat

      proof

        let x;

        assume

         A7: x in ( dom O);

        then (p . x) in ( rng p) by FUNCT_1:def 3, A6;

        then

        consider n,m be Nat such that

         A8: (p . x) = ((2 |^ n) * ((2 * m) + 1)) by NAGATA_2: 1;

        (Oa . x) = [((2 * m) + 1), n] by A7, A1, A8, A6, A4;

        then P1(x) = ((2 * m) + 1);

        hence thesis by A7, A5;

      end;

      then

      reconsider O as odd-valued FinSequence by Def2;

      deffunc P2( object) = ((Oa . $1) `2 );

      consider A be FinSequence such that

       A9: ( len A) = ( len p) & for k st k in ( dom A) holds (A . k) = P2(k) from FINSEQ_1:sch 2;

      

       A10: ( dom A) = ( dom p) by FINSEQ_3: 29, A9;

      for x st x in ( dom A) holds (A . x) is natural

      proof

        let x;

        assume

         A11: x in ( dom A);

        then (p . x) in ( rng p) by FUNCT_1:def 3, A10;

        then

        consider n,m be Nat such that

         A12: (p . x) = ((2 |^ n) * ((2 * m) + 1)) by NAGATA_2: 1;

        (Oa . x) = [((2 * m) + 1), n] by A11, A1, A12, A10, A4;

        then P2(x) = n;

        hence thesis by A11, A9;

      end;

      then

      reconsider A as natural-valued FinSequence by VALUED_0:def 12;

      take O, A;

      thus ( len O) = ( len p) = ( len A) by A5, A9;

      set OA = (O (#) (2 |^ A));

      ( dom (2 |^ A)) = ( dom A) by FLEXARY1:def 4;

      then

       A13: (( dom O) /\ ( dom (2 |^ A))) = ( dom p) by A10, A6;

      

       A14: (p . 1) = ((O . 1) * (2 |^ (A . 1))) & ... & (p . ( len p)) = ((O . ( len p)) * (2 |^ (A . ( len p))))

      proof

        let i;

        assume

         A15: 1 <= i & i <= ( len p);

        then i in ( dom p) by FINSEQ_3: 25;

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

        then

        consider n,m be Nat such that

         A16: (p . i) = ((2 |^ n) * ((2 * m) + 1)) by NAGATA_2: 1;

        (Oa . i) = [((2 * m) + 1), n] & ( [((2 * m) + 1), n] `1 ) = ((2 * m) + 1) & ( [((2 * m) + 1), n] `2 ) = n by A15, FINSEQ_3: 25, A1, A16, A4;

        then (O . i) = ((2 * m) + 1) & (A . i) = n by A15, FINSEQ_3: 25, A5, A9;

        hence thesis by A16;

      end;

      for i st i in ( dom p) holds (p . i) = (OA . i)

      proof

        let i;

        assume

         A17: i in ( dom p);

        then 1 <= i & i <= ( len p) by FINSEQ_3: 25;

        then

         A18: (p . i) = ((O . i) * (2 |^ (A . i))) by A14;

        ((2 |^ A) . i) = (2 to_power (A . i)) by A17, A10, FLEXARY1:def 4;

        hence thesis by VALUED_1: 5, A18;

      end;

      hence thesis by A13, VALUED_1:def 4, A14;

    end;

    theorem :: EULRPART:7

    

     Th7: for D be finite set holds for f be Function of D, NAT holds ex h be FinSequence of D st for d be Element of D holds ( card ( Coim (h,d))) = (f . d)

    proof

      defpred P[ Nat] means for D be finite set st ( card D) = $1 holds for f be Function of D, NAT holds ex h be FinSequence of D st for d be Element of D holds ( card ( Coim (h,d))) = (f . d);

      

       A1: P[ 0 ]

      proof

        let D be finite set such that

         A2: ( card D) = 0 ;

        let f be Function of D, NAT ;

        take h = ( <*> D);

        let d be Element of D;

        

         A3: ( Coim (h,d)) = (h " {d}) by RELAT_1:def 17;

         not d in ( dom f) by A2;

        hence thesis by FUNCT_1:def 2, A3;

      end;

      

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

      proof

        assume

         A5: P[i];

        set i1 = (i + 1);

        let D be finite set such that

         A6: ( card D) = i1;

        let f be Function of D, NAT ;

        D is non empty by A6;

        then

        consider d be object such that

         A7: d in D;

        set Dd = (D \ {d});

        

         A8: ( card Dd) = i by A6, A7, STIRL2_1: 55;

        reconsider fd = (f | Dd) as Function of Dd, NAT ;

        consider h be FinSequence of Dd such that

         A9: for x be Element of Dd holds ( card ( Coim (h,x))) = (fd . x) by A5, A8;

        

         A10: ( rng h) c= Dd;

        Dd c= D;

        then ( rng h) c= D;

        then

        reconsider h as FinSequence of D by FINSEQ_1:def 4;

        reconsider g = ((f . d) |-> d) as FinSequence of D by A7, FINSEQ_2: 63;

        take hg = (h ^ g);

        let x be Element of D;

        ( Coim (hg,x)) = (hg " {x}) & ( Coim (h,x)) = (h " {x}) & ( Coim (g,x)) = (g " {x}) by RELAT_1:def 17;

        then

         A11: ( card ( Coim (hg,x))) = (( card (h " {x})) + ( card (g " {x}))) by FINSEQ_3: 57;

        per cases ;

          suppose

           A12: x <> d;

          then x in Dd by A7, ZFMISC_1: 56;

          then

           A13: ( card ( Coim (h,x))) = (fd . x) & (fd . x) = (f . x) by A9, FUNCT_1: 49;

           not d in {x} by A12, TARSKI:def 1;

          then (g " {x}) = {} by FUNCOP_1: 16;

          hence thesis by RELAT_1:def 17, A11, A13;

        end;

          suppose

           A14: x = d;

          then not x in ( rng h) by ZFMISC_1: 56, A10;

          then

           A15: (h " {x}) = {} by FUNCT_1: 72;

          d in {x} by A14, TARSKI:def 1;

          then (g " {x}) = ( Seg (f . d)) by FUNCOP_1: 14;

          hence thesis by FINSEQ_1: 57, A15, A11, A14;

        end;

      end;

      let D be finite set;

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

      then P[( card D)];

      hence thesis;

    end;

    

     Lm1: for f1,f2,g1,g2 be complex-valued FinSequence st ( len f1) = ( len g1) & ( len f2) <= ( len g2) holds ((f1 ^ f2) (#) (g1 ^ g2)) = ((f1 (#) g1) ^ (f2 (#) g2))

    proof

      let f1,f2,g1,g2 be complex-valued FinSequence such that

       A1: ( len f1) = ( len g1) and

       A2: ( len f2) <= ( len g2);

      

       A3: ( dom f1) = ( Seg ( len f1)) & ( dom f2) = ( Seg ( len f2)) & ( dom g1) = ( Seg ( len g1)) & ( dom g2) = ( Seg ( len g2)) by FINSEQ_1:def 3;

      

       A4: ( dom (f1 ^ f2)) = ( Seg ( len (f1 ^ f2))) & ( dom (g1 ^ g2)) = ( Seg ( len (g1 ^ g2))) by FINSEQ_1:def 3;

      

       A5: ( len (f1 ^ f2)) = (( len f1) + ( len f2)) & ( len (g1 ^ g2)) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

      then (( dom (f1 ^ f2)) /\ ( dom (g1 ^ g2))) = ( dom (f1 ^ f2)) by A1, A2, XREAL_1: 6, A4, FINSEQ_1: 7;

      then ( dom ((f1 ^ f2) (#) (g1 ^ g2))) = ( dom (f1 ^ f2)) by VALUED_1:def 4;

      then

       A6: ( len ((f1 ^ f2) (#) (g1 ^ g2))) = ( len (f1 ^ f2)) by FINSEQ_3: 29;

      (( dom f1) /\ ( dom g1)) = ( dom f1) by A1, A3;

      then

       A7: ( dom (f1 (#) g1)) = ( dom f1) by VALUED_1:def 4;

      then

       A8: ( len (f1 (#) g1)) = ( len f1) by FINSEQ_3: 29;

      

       A9: (( dom f2) /\ ( dom g2)) = ( dom f2) by A2, A3, FINSEQ_1: 7;

      then

       A10: ( dom (f2 (#) g2)) = ( dom f2) by VALUED_1:def 4;

      then

       A11: ( len (f2 (#) g2)) = ( len f2) by FINSEQ_3: 29;

      for i st 1 <= i & i <= ( len (f1 ^ f2)) holds (((f1 ^ f2) (#) (g1 ^ g2)) . i) = (((f1 (#) g1) ^ (f2 (#) g2)) . i)

      proof

        let i;

        assume 1 <= i & i <= ( len (f1 ^ f2));

        then

         A12: i in ( dom (f1 ^ f2)) by FINSEQ_3: 25;

        per cases ;

          suppose

           A13: i in ( dom f1);

          then

           A14: ((f1 ^ f2) . i) = (f1 . i) & ((g1 ^ g2) . i) = (g1 . i) by A1, A3, FINSEQ_1:def 7;

          (((f1 (#) g1) ^ (f2 (#) g2)) . i) = ((f1 (#) g1) . i) by A13, A7, FINSEQ_1:def 7

          .= ((f1 . i) * (g1 . i)) by VALUED_1: 5;

          hence thesis by A14, VALUED_1: 5;

        end;

          suppose not i in ( dom f1);

          then

          consider j such that

           A15: j in ( dom f2) & i = (( len f1) + j) by A12, FINSEQ_1: 25;

          

           A16: ((f1 ^ f2) . i) = (f2 . j) & ((g1 ^ g2) . i) = (g2 . j) by A9, A15, A1, FINSEQ_1:def 7;

          (((f1 (#) g1) ^ (f2 (#) g2)) . i) = ((f2 (#) g2) . j) by A15, A8, A10, FINSEQ_1:def 7

          .= ((f2 . j) * (g2 . j)) by VALUED_1: 5;

          hence thesis by VALUED_1: 5, A16;

        end;

      end;

      hence thesis by A5, A6, A8, A11, FINSEQ_1: 22;

    end;

    theorem :: EULRPART:8

    

     Th8: for f1,f2,g1,g2 be complex-valued FinSequence st ( len f1) = ( len g1) holds ((f1 ^ f2) (#) (g1 ^ g2)) = ((f1 (#) g1) ^ (f2 (#) g2))

    proof

      let f1,f2,g1,g2 be complex-valued FinSequence such that

       A1: ( len f1) = ( len g1);

      ( len f2) <= ( len g2) or ( len f2) >= ( len g2);

      hence thesis by A1, Lm1;

    end;

    

     Lm2: for f be complex-valued FinSequence holds ((( id ( dom f)) (#) f) . i) = (i * (f . i))

    proof

      let f be complex-valued FinSequence;

      per cases ;

        suppose i in ( dom f);

        then (( id ( dom f)) . i) = i by FUNCT_1: 17;

        hence thesis by VALUED_1: 5;

      end;

        suppose not i in ( dom f);

        then

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

        ((( id ( dom f)) (#) f) . i) = ((( id ( dom f)) . i) * (f . i)) by VALUED_1: 5;

        hence thesis by A1;

      end;

    end;

    theorem :: EULRPART:9

    

     Th9: for f,h be natural-valued FinSequence st for i holds ( card ( Coim (h,i))) = (f . i) holds ( Sum h) = (((1 * (f . 1)) + (2 * (f . 2))) + (((( id ( dom f)) (#) f),3) +... ))

    proof

      defpred P[ Nat] means for f,h be natural-valued FinSequence st ( len f) = $1 & for i holds ( card ( Coim (h,i))) = (f . i) holds ( Sum h) = (((( id ( dom f)) (#) f),1) +... );

      

       A1: P[ 0 ]

      proof

        let f,h be natural-valued FinSequence such that

         A2: ( len f) = 0 and

         A3: for i holds ( card ( Coim (h,i))) = (f . i);

        set L = (( len h) |-> 0 );

        now

          let i such that

           A4: 1 <= i & i <= ( len h);

          

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

          f = {} by A2;

          then (f . (h . i)) = 0 ;

          then ( card ( Coim (h,(h . i)))) = 0 by A3;

          then ( Coim (h,(h . i))) = {} ;

          then (h " {(h . i)}) = {} by RELAT_1:def 17;

          then not (h . i) in ( rng h) by FUNCT_1: 72;

          hence (h . i) = (L . i) by A5, FUNCT_1:def 3;

        end;

        then

         A6: h = (( len h) |-> 0 ) by CARD_1:def 7;

        

         A7: f = {} by A2;

        then

        reconsider E = (( id ( dom f)) (#) f) as complex-valued FinSequence;

        (((( id ( dom f)) (#) f),1) +... ) = ((E . 1) + ((E,(1 + 1)) +... )) by FLEXARY1: 20

        .= ( Sum E) by FLEXARY1: 22

        .= 0 by A7, RVSUM_1: 72;

        hence thesis by A6, RVSUM_1: 81;

      end;

      

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

      proof

        assume

         A9: P[i];

        set i1 = (i + 1);

        let f,h be natural-valued FinSequence such that

         A10: ( len f) = i1 and

         A11: for i holds ( card ( Coim (h,i))) = (f . i);

        

         A12: ( id ( dom f)) = ( idseq i1) by FINSEQ_1:def 3, A10;

        set fi = (f | i);

        

         A13: f = (fi ^ <*(f . i1)*>) by A10, FINSEQ_3: 55;

        

         A14: i < i1 by NAT_1: 13;

        then

         A15: ( len fi) = i by A10, FINSEQ_1: 59;

        then

         A16: ( id ( dom fi)) = ( idseq i) by FINSEQ_1:def 3;

        

         A17: ( idseq i1) = (( idseq i) ^ <*i1*>) by FINSEQ_2: 51;

        ( len fi) = ( len ( idseq i)) by CARD_1:def 7, A15;

        then

         A18: (( id ( dom f)) (#) f) = ((( idseq i) (#) fi) ^ ( <*i1*> (#) <*(f . i1)*>)) by Th8, A12, A13, A17;

        

         A19: (( Seg 1) /\ ( Seg 1)) = ( Seg 1);

        ( dom <*i1*>) = ( Seg 1) & ( dom <*(f . i1)*>) = ( Seg 1) by FINSEQ_1: 38;

        then ( dom ( <*i1*> (#) <*(f . i1)*>)) = ( Seg 1) by VALUED_1:def 4, A19;

        then

         A20: ( len ( <*i1*> (#) <*(f . i1)*>)) = 1 by FINSEQ_1:def 3;

        ( <*i1*> . 1) = i1 & ( <*(f . i1)*> . 1) = (f . i1) by FINSEQ_1: 40;

        then (( <*i1*> (#) <*(f . i1)*>) . 1) = (i1 * (f . i1)) by VALUED_1: 5;

        then

         A21: ( <*i1*> (#) <*(f . i1)*>) = <*(i1 * (f . i1))*> by A20, FINSEQ_1: 40;

        

         A22: (((( id ( dom f)) (#) f),1) +... ) = ( Sum (( idseq i1) (#) f)) by A12, FLEXARY1: 21;

        per cases ;

          suppose

           A23: (f . i1) = 0 ;

          then

           A24: (((( id ( dom f)) (#) f),1) +... ) = (( Sum (( idseq i) (#) fi)) + 0 ) by A21, A12, A18, A22, RVSUM_1: 74;

          for j holds ( card ( Coim (h,j))) = (fi . j)

          proof

            let j;

            per cases ;

              suppose j in ( dom fi);

              then (fi . j) = (f . j) & (f . j) = ( card ( Coim (h,j))) by A11, FUNCT_1: 47;

              hence thesis;

            end;

              suppose

               A25: j = i1;

              then not j in ( dom fi) by A14, A15, FINSEQ_3: 25;

              then (fi . j) = 0 & (f . j) = ( card ( Coim (h,j))) by A11, FUNCT_1:def 2;

              hence thesis by A23, A25;

            end;

              suppose

               A26: j <> i1 & not j in ( dom fi);

              then

               A27: (fi . j) = 0 by FUNCT_1:def 2;

              j < 1 or j > i by A26, A15, FINSEQ_3: 25;

              then j < 1 or j >= i1 by NAT_1: 13;

              then j < 1 or j > i1 by A26, XXREAL_0: 1;

              then not j in ( dom f) by A10, FINSEQ_3: 25;

              then (f . j) = 0 by FUNCT_1:def 2;

              hence thesis by A11, A27;

            end;

          end;

          

          then ( Sum h) = (((( idseq i) (#) fi),1) +... ) by A9, A16, A15

          .= ( Sum (( idseq i) (#) fi)) by FLEXARY1: 21;

          hence thesis by A24;

        end;

          suppose (f . i1) <> 0 ;

          then ( card ( Coim (h,i1))) <> 0 by A11;

          then ( Coim (h,i1)) <> {} ;

          then

          consider xx be object such that

           A28: xx in ( Coim (h,i1)) by XBOOLE_0:def 1;

          

           A29: xx in ( Coim (h,i1)) & ( Coim (h,i1)) = (h " {i1}) by A28, RELAT_1:def 17;

          then

          reconsider D = ( dom h) as non empty set by FUNCT_1:def 7;

          

           A30: ( rng h) c= REAL ;

          then

          reconsider H = h as Function of D, REAL by FUNCT_2: 2;

          reconsider h1 = H as FinSequence of REAL by A30, FINSEQ_1:def 4;

          set X = (h " {i1}), Y = (D \ X);

          ( dom (H | (Y \/ X))) is finite;

          then

           A31: (( FinS (H,(Y \/ X))),(( FinS (H,Y)) ^ ( FinS (H,X)))) are_fiberwise_equipotent by RFUNCT_3: 76, XBOOLE_1: 79;

          

           A32: D = (X \/ Y) by RELAT_1: 132, XBOOLE_1: 45;

          (H | D) = H;

          then (H,( FinS (H,(X \/ Y)))) are_fiberwise_equipotent by A32, RFUNCT_3:def 13;

          

          then

           A33: ( Sum h1) = ( Sum (( FinS (H,Y)) ^ ( FinS (H,X)))) by A31, CLASSES1: 76, RFINSEQ: 9

          .= (( Sum ( FinS (H,Y))) + ( Sum ( FinS (H,X)))) by RVSUM_1: 75;

          

           A34: ( dom (H | X)) = X & ( dom (H | Y)) = Y by RELAT_1: 132, RELAT_1: 62;

          ( rng (H | X)) c= {i1}

          proof

            let y be object;

            assume y in ( rng (H | X));

            then

            consider x be object such that

             A35: x in X & ((H | X) . x) = y by A34, FUNCT_1:def 3;

            ((H | X) . x) = (H . x) by A35, FUNCT_1: 49;

            hence thesis by A35, FUNCT_1:def 7;

          end;

          then ( FinS (H,X)) = (( card X) |-> i1) by A29, A34, ZFMISC_1: 33, RFUNCT_3: 75;

          then

           A36: ( FinS (H,X)) = ((f . i1) |-> i1) by A29, A11;

          

           A37: ((H | Y),( FinS (H,Y))) are_fiberwise_equipotent by A34, RFUNCT_3:def 13;

          then ( rng (H | Y)) = ( rng ( FinS (H,Y))) by CLASSES1: 75;

          then ( rng ( FinS (H,Y))) c= NAT by VALUED_0:def 6;

          then

          reconsider F = ( FinS (H,Y)) as natural-valued FinSequence by VALUED_0:def 6;

          for j holds ( card ( Coim (F,j))) = (fi . j)

          proof

            let j;

            set hY = (h | Y);

            

             A38: ( card ( Coim (F,j))) = ( card ( Coim (hY,j))) by A37, CLASSES1:def 10;

            

             A39: (hY " {j}) = ( Coim (hY,j)) & (h " {j}) = ( Coim (h,j)) by RELAT_1:def 17;

            

             A40: (hY " {j}) = (Y /\ (h " {j})) by FUNCT_1: 70

            .= (((h " {j}) /\ D) \ (h " {i1})) by XBOOLE_1: 49

            .= ((h " {j}) \ (h " {i1})) by RELAT_1: 132, XBOOLE_1: 28

            .= (h " ( {j} \ {i1})) by FUNCT_1: 69;

            

             A41: ( card ( Coim (h,j))) = (f . j) by A11;

            per cases ;

              suppose

               A42: j in ( dom fi);

              then j <> i1 by A15, FINSEQ_3: 25, A14;

              then ( card ( Coim (F,j))) = ( card ( Coim (h,j))) by ZFMISC_1: 14, A38, A39, A40;

              hence thesis by A41, A42, FUNCT_1: 47;

            end;

              suppose

               A43: j = i1;

              then

               A44: not j in ( dom fi) by A14, A15, FINSEQ_3: 25;

              ( card ( Coim (F,j))) = ( card (h " {} )) by A43, A38, A39, A40;

              hence thesis by A44, FUNCT_1:def 2;

            end;

              suppose

               A45: not j in ( dom fi) & j <> i1;

              then

               A46: (fi . j) = 0 by FUNCT_1:def 2;

              j < 1 or j > i by A45, A15, FINSEQ_3: 25;

              then j < 1 or j >= i1 by NAT_1: 13;

              then j < 1 or j > i1 by A45, XXREAL_0: 1;

              then

               A47: not j in ( dom f) by A10, FINSEQ_3: 25;

              ( card ( Coim (F,j))) = ( card ( Coim (h,j))) by A45, ZFMISC_1: 14, A38, A39, A40;

              hence thesis by A46, A47, FUNCT_1:def 2, A41;

            end;

          end;

          

          then

           A48: ( Sum F) = (((( idseq i) (#) fi),1) +... ) by A9, A15, A16

          .= ( Sum (( idseq i) (#) fi)) by FLEXARY1: 21;

          (((( id ( dom f)) (#) f),1) +... ) = (( Sum (( idseq i) (#) fi)) + (i1 * (f . i1))) by A21, A12, A18, A22, RVSUM_1: 74;

          hence thesis by A33, A48, A36, RVSUM_1: 80;

        end;

      end;

      

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

      let f,h be natural-valued FinSequence such that

       A50: for i holds ( card ( Coim (h,i))) = (f . i);

      set I = (( idseq ( len f)) (#) f);

      

       A51: ( id ( dom f)) = ( idseq ( len f)) by FINSEQ_1:def 3;

      then

       A52: (I . 1) = (1 * (f . 1)) by Lm2;

      

       A53: (I . 2) = (2 * (f . 2)) by Lm2, A51;

      ( Sum h) = ((I,1) +... ) by A49, A51, A50

      .= ((I . 1) + ((I,(1 + 1)) +... )) by FLEXARY1: 20

      .= ((I . 1) + ((I . 2) + ((I,(2 + 1)) +... ))) by FLEXARY1: 20;

      hence thesis by A52, A53, A51;

    end;

    theorem :: EULRPART:10

    

     Th10: for g be natural-valued FinSequence holds for sort be DoubleReorganization of ( dom g) holds ex h be (2 * ( len sort)) -element FinSequence of NAT st for j holds (h . (2 * j)) = 0 & (h . ((2 * j) - 1)) = ((g . (sort _ (j,1))) + ((((g *. sort) . j),2) +... ))

    proof

      let g be natural-valued FinSequence;

      let sort be DoubleReorganization of ( dom g);

      defpred P[ object, object] means ($1 = ((2 * j) - 1) implies $2 = ((g . (sort _ (j,1))) + ((((g *. sort) . j),2) +... ))) & ($1 = (2 * j) implies $2 = 0 );

      set S = ( Seg (2 * ( len sort)));

      

       A1: for k st k in S holds ex x st P[k, x]

      proof

        let k;

        assume k in ( Seg (2 * ( len sort)));

        per cases ;

          suppose

           A2: k is even;

          set j = the Nat;

          take x = 0 ;

          thus thesis by A2;

        end;

          suppose k is odd;

          then

          consider j such that

           A4: k = ((2 * j) + 1) by ABIAN: 9;

          set j1 = (j + 1);

          take x = ((g . (sort _ (j1,1))) + ((((g *. sort) . j1),2) +... ));

          let i;

          thus thesis by A4;

        end;

      end;

      consider f be FinSequence such that

       A5: ( dom f) = S & for i st i in S holds P[i, (f . i)] from FINSEQ_1:sch 1( A1);

      

       A6: ( rng f) c= NAT

      proof

        let y;

        assume y in ( rng f);

        then

        consider x such that

         A7: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

        reconsider x as Nat by A7;

        per cases ;

          suppose x is even;

          then ex i st x = (2 * i) by ABIAN:def 2;

          then (f . x) = 0 by A5, A7;

          hence thesis by A7;

        end;

          suppose x is odd;

          then

          consider i such that

           A8: x = ((2 * i) + 1) by ABIAN: 9;

          ((2 * (i + 1)) - 1) = x by A8;

          then (f . x) = ((g . (sort _ ((i + 1),1))) + ((((g *. sort) . (i + 1)),2) +... )) by A7, A5;

          hence thesis by A7, ORDINAL1:def 12;

        end;

      end;

      

       A9: ( len f) = (2 * ( len sort)) by A5, FINSEQ_1:def 3;

      then

      reconsider f as (2 * ( len sort)) -element FinSequence of NAT by A6, FINSEQ_1:def 4, CARD_1:def 7;

      take f;

      let i;

      thus (f . (2 * i)) = 0

      proof

        (2 * i) in ( dom f) or not (2 * i) in ( dom f);

        hence thesis by A5, FUNCT_1:def 2;

      end;

      thus (f . ((2 * i) - 1)) = ((g . (sort _ (i,1))) + ((((g *. sort) . i),2) +... ))

      proof

        per cases by FINSEQ_3: 25;

          suppose ((2 * i) - 1) in ( dom f);

          hence thesis by A5;

        end;

          suppose

           A10: ((2 * i) - 1) > ( len f);

          then

           A11: not ((2 * i) - 1) in ( dom f) by FINSEQ_3: 25;

          (((2 * i) - 1) + 1) > ( len f) by A10, NAT_1: 13;

          then i > ( len sort) by A9, XREAL_1: 64;

          then

           A12: not i in ( dom sort) by FINSEQ_3: 25;

          then (sort . i) = {} by FUNCT_1:def 2;

          then not (sort _ (i,1)) in ( dom g) by FINSEQ_3: 25;

          then

           A13: (g . (sort _ (i,1))) = {} by FUNCT_1:def 2;

          ( dom (g *. sort)) = ( dom sort) by FOMODEL2:def 6;

          then ((g *. sort) . i) = {} by A12, FUNCT_1:def 2;

          then ((g . (sort _ (i,1))) + ((((g *. sort) . i),2) +... )) = 0 by FLEXARY1: 15, A13;

          hence thesis by A11, FUNCT_1:def 2;

        end;

          suppose

           A14: ((2 * i) - 1) < 1;

          then

           A15: not ((2 * i) - 1) in ( dom f) by FINSEQ_3: 25;

          (((2 * i) - 1) + 1) < (1 + 1) by A14, XREAL_1: 6;

          then (2 * i) < (2 * 1);

          then

           A16: not i in ( dom sort) by XREAL_1: 64, FINSEQ_3: 25;

          then (sort . i) = 0 by FUNCT_1:def 2;

          then not (sort _ (i,1)) in ( dom g) by FUNCT_1:def 2, FINSEQ_3: 25;

          then

           A17: (g . (sort _ (i,1))) = 0 by FUNCT_1:def 2;

          ( dom (g *. sort)) = ( dom sort) by FOMODEL2:def 6;

          then ((g *. sort) . i) = {} by A16, FUNCT_1:def 2;

          then ((g . (sort _ (i,1))) + ((((g *. sort) . i),2) +... )) = 0 by FLEXARY1: 15, A17;

          hence thesis by A15, FUNCT_1:def 2;

        end;

      end;

    end;

    

     Lm3: for mu be natural-valued FinSequence st for j holds (mu . (2 * j)) = 0 holds ex h be odd-valued FinSequence st h is non-decreasing & for j holds ( card ( Coim (h,j))) = (mu . j)

    proof

      let mu be natural-valued FinSequence such that

       A1: for j holds (mu . (2 * j)) = 0 ;

      set S = ( Seg ( len mu));

      

       A2: ( rng mu) c= NAT by VALUED_0:def 6;

      

       A3: ( dom mu) = S by FINSEQ_1:def 3;

      then mu is Function of S, NAT by A2, FUNCT_2: 2;

      then

      consider h be FinSequence of S such that

       A4: for d be Element of S holds ( card ( Coim (h,d))) = (mu . d) by Th7;

      

       A5: ( rng h) c= S by FINSEQ_1:def 4;

      

       A6: ( rng h) c= OddNAT

      proof

        let y be object;

        assume

         A7: y in ( rng h);

        then

         A8: ( card ( Coim (h,y))) = (mu . y) by A4, A5;

        ( Coim (h,y)) = (h " {y}) by RELAT_1:def 17;

        then

         A9: ( Coim (h,y)) <> {} by A7, FUNCT_1: 72;

        consider x such that

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

        reconsider y as Nat by A10;

        y is odd

        proof

          assume y is even;

          then ex j st y = (2 * j) by ABIAN:def 2;

          hence thesis by A1, A9, A8;

        end;

        hence thesis by Th2;

      end;

      then

      reconsider h as odd-valued FinSequence by Def1;

      ( rng h) c= REAL ;

      then

      reconsider h as FinSequence of REAL by FINSEQ_1:def 4;

      set s = ( sort_a h);

      ( rng h) = ( rng s) by RFINSEQ2:def 6, CLASSES1: 75;

      then

      reconsider s as odd-valued FinSequence by A6, Def1;

      take s;

      thus s is non-decreasing;

      let i;

      per cases ;

        suppose i in S;

        then (mu . i) = ( card ( Coim (h,i))) by A4;

        hence thesis by RFINSEQ2:def 6, CLASSES1:def 10;

      end;

        suppose

         A11: not i in S;

        then

         A12: (mu . i) = 0 & not i in ( rng h) by A5, A3, FUNCT_1:def 2;

        (h " {i}) = {} by A11, A5, FUNCT_1: 72;

        then ( Coim (h,i)) = {} by RELAT_1:def 17;

        then ( card ( Coim (h,i))) = 0 ;

        hence thesis by CLASSES1:def 10, RFINSEQ2:def 6, A12;

      end;

    end;

    begin

    theorem :: EULRPART:11

    

     Th11: for d be one-to-one a_partition of n holds ex e be odd-valued a_partition of n st for j be Nat, O1 be odd-valued FinSequence, a1 be natural-valued FinSequence st ( len O1) = ( len d) = ( len a1) & d = (O1 (#) (2 |^ a1)) holds for sort be DoubleReorganization of ( dom d) st (1 = (O1 . (sort _ (1,1))) & ... & 1 = (O1 . (sort _ (1,( len (sort . 1)))))) & (3 = (O1 . (sort _ (2,1))) & ... & 3 = (O1 . (sort _ (2,( len (sort . 2)))))) & (5 = (O1 . (sort _ (3,1))) & ... & 5 = (O1 . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O1 . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O1 . (sort _ (i,( len (sort . i))))) holds ( card ( Coim (e,1))) = (((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +... )) & ( card ( Coim (e,3))) = (((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +... )) & ( card ( Coim (e,5))) = (((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +... )) & ( card ( Coim (e,((j * 2) - 1)))) = (((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +... ))

    proof

      let d be one-to-one a_partition of n;

      consider O be odd-valued FinSequence, a be natural-valued FinSequence such that

       A1: ( len O) = ( len d) = ( len a) & d = (O (#) (2 |^ a)) and (d . 1) = ((O . 1) * (2 |^ (a . 1))) & ... & (d . ( len d)) = ((O . ( len d)) * (2 |^ (a . ( len d)))) by Th6;

      ( len (2 |^ a)) = ( len O) by A1, CARD_1:def 7;

      then

      reconsider sort = the odd_organization of O as DoubleReorganization of ( dom (2 |^ a)) by FINSEQ_3: 29;

      consider mu be (2 * ( len sort)) -element FinSequence of NAT such that

       A2: for j holds (mu . (2 * j)) = 0 & (mu . ((2 * j) - 1)) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... )) by Th10;

      set alpha = (a * (sort . 1)), beta = (a * (sort . 2)), gamma = (a * (sort . 3));

      

       A3: n = (((((((2 |^ alpha) . 1) + (((2 |^ alpha),2) +... )) * 1) + ((((2 |^ beta) . 1) + (((2 |^ beta),2) +... )) * 3)) + ((((2 |^ gamma) . 1) + (((2 |^ gamma),2) +... )) * 5)) + (((( id ( dom mu)) (#) mu),7) +... ))

      proof

        reconsider o1 = sort as DoubleReorganization of ( dom d) by A1, FINSEQ_3: 29;

        

         A4: ( dom (d *. o1)) = ( dom o1) & ( dom ((2 |^ a) *. sort)) = ( dom sort) by FOMODEL2:def 6;

        

         A5: for j holds ( Sum ((d *. o1) . j)) = (((2 * j) - 1) * (mu . ((2 * j) - 1)))

        proof

          let j;

          

           A6: (mu . ((2 * j) - 1)) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... )) by A2;

          per cases ;

            suppose j in ( dom o1);

            set jj = ((2 * j) - 1);

            

             A7: ((d *. o1) . j) = (d * (o1 . j)) by FLEXARY1: 41;

            

             A8: (((2 |^ a) *. sort) . j) = ((2 |^ a) * (sort . j)) by FLEXARY1: 41;

            

             A9: ( len ((d *. o1) . j)) = ( len (o1 . j)) by CARD_1:def 7;

            

             A10: ( len (((2 |^ a) *. sort) . j)) = ( len (sort . j)) by CARD_1:def 7;

            for n st 1 <= n & n <= ( len (sort . j)) holds (((d *. o1) . j) . n) = ((jj * (((2 |^ a) *. sort) . j)) . n)

            proof

              let n;

              assume

               A11: 1 <= n & n <= ( len (sort . j));

              

               A12: ((2 * j) - 1) = (O . (o1 _ (j,1))) & ... & ((2 * j) - 1) = (O . (o1 _ (j,( len (o1 . j))))) by Def4;

              

              thus (((d *. o1) . j) . n) = (d . (o1 _ (j,n))) by A11, A9, FINSEQ_3: 25, A7, FUNCT_1: 12

              .= ((O . (o1 _ (j,n))) * ((2 |^ a) . (o1 _ (j,n)))) by A1, VALUED_1: 5

              .= (jj * ((2 |^ a) . (o1 _ (j,n)))) by A12, A11

              .= (jj * ((((2 |^ a) *. sort) . j) . n)) by A11, A10, FINSEQ_3: 25, A8, FUNCT_1: 12

              .= ((jj * (((2 |^ a) *. sort) . j)) . n) by VALUED_1: 6;

            end;

            then

             A13: ((d *. o1) . j) = (jj * (((2 |^ a) *. sort) . j)) by A9, CARD_1:def 7;

            ((((2 |^ a) *. sort) . j) . 1) = (((2 |^ a) *. sort) _ (j,1));

            then ((2 |^ a) . (sort _ (j,1))) = ((((2 |^ a) *. sort) . j) . 1) by FLEXARY1: 42;

            

            then ( Sum (((2 |^ a) *. sort) . j)) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... )) by FLEXARY1: 22

            .= (mu . jj) by A2;

            hence thesis by A13, RVSUM_1: 87;

          end;

            suppose

             A14: not j in ( dom sort);

            then (sort . j) = {} by FUNCT_1:def 2;

            then

             A15: not ((sort . j) . 1) in ( dom (2 |^ a)) by FINSEQ_3: 25;

             not j in ( dom ((2 |^ a) *. sort)) by A14, FOMODEL2:def 6;

            then (((2 |^ a) *. sort) . j) = {} by FUNCT_1:def 2;

            then (((((2 |^ a) *. sort) . j),2) +... ) = 0 by FLEXARY1: 15;

            then (mu . ((2 * j) - 1)) = 0 by A6, A15, FUNCT_1:def 2;

            hence thesis by A14, A4, FUNCT_1:def 2, RVSUM_1: 72;

          end;

        end;

        set I = ( idseq ( len mu));

        

         A16: I = ( id ( dom mu)) by FINSEQ_1:def 3;

        

         A17: (1 -' 1) = 0 & (2 -' 1) = (2 - 1) by XREAL_1: 233, XREAL_1: 232;

        

         A18: for j holds ((( Sum (d *. o1)),(4 + (j * 1))) +...+ (( Sum (d *. o1)),((4 + (j * 1)) + (1 -' 1)))) = (((I (#) mu),(7 + (j * 2))) +...+ ((I (#) mu),((7 + (j * 2)) + (2 -' 1))))

        proof

          let j;

          set S = ( Sum (d *. o1));

          

           A19: ((S,(4 + (j * 1))) +...+ (S,((4 + (j * 1)) + (1 -' 1)))) = (S . (4 + j)) by A17, FLEXARY1: 11

          .= ( Sum ((d *. o1) . (4 + j))) by FLEXARY1:def 8

          .= (((2 * (4 + j)) - 1) * (mu . ((2 * (4 + j)) - 1))) by A5

          .= (((2 * j) + 7) * (mu . ((2 * j) + 7)));

          

           A20: (((I (#) mu),(7 + (j * 2))) +...+ ((I (#) mu),((7 + (j * 2)) + (2 -' 1)))) = (((I (#) mu) . (7 + (j * 2))) + (((I (#) mu),((7 + (j * 2)) + 1)) +...+ ((I (#) mu),((7 + (j * 2)) + 1)))) by NAT_1: 11, FLEXARY1: 13, A17

          .= (((I (#) mu) . (7 + (j * 2))) + ((I (#) mu) . ((7 + (j * 2)) + 1))) by FLEXARY1: 11;

          ((7 + (j * 2)) + 1) = (2 * (j + 4));

          then (mu . ((7 + (j * 2)) + 1)) = 0 by A2;

          then ((I (#) mu) . ((7 + (j * 2)) + 1)) = (((7 + (j * 2)) + 1) * 0 ) by A16, Lm2;

          hence thesis by A19, A20, A16, Lm2;

        end;

        

         A21: ((( Sum (d *. o1)),4) +... ) = (((I (#) mu),7) +... ) from FLEXARY1:sch 1( A18);

        

         A22: ((2 * 1) - 1) = 1;

        

        then

         A23: (1 * (mu . 1)) = ( Sum ((d *. o1) . 1)) by A5

        .= (( Sum (d *. o1)) . 1) by FLEXARY1:def 8;

        

         A24: ((2 * 2) - 1) = 3;

        

        then

         A25: (3 * (mu . 3)) = ( Sum ((d *. o1) . 2)) by A5

        .= (( Sum (d *. o1)) . 2) by FLEXARY1:def 8;

        

         A26: ((2 * 3) - 1) = 5;

        

        then

         A27: (5 * (mu . 5)) = ( Sum ((d *. o1) . 3)) by A5

        .= (( Sum (d *. o1)) . 3) by FLEXARY1:def 8;

        for j holds ((2 |^ a) . (sort _ (j,1))) = ((2 |^ (a * (sort . j))) . 1) & (((2 |^ a) *. sort) . j) = (2 |^ (a * (sort . j)))

        proof

          let j;

          

           A28: ((2 |^ a) . (sort _ (j,1))) = (((2 |^ a) *. sort) _ (j,1)) by FLEXARY1: 42;

          (((2 |^ a) *. sort) . j) = ((2 |^ a) * (sort . j)) by FLEXARY1: 41

          .= (2 |^ (a * (sort . j))) by FLEXARY1: 25;

          hence thesis by A28;

        end;

        then

         A29: ((2 |^ a) . (sort _ (1,1))) = ((2 |^ alpha) . 1) & ((2 |^ a) . (sort _ (2,1))) = ((2 |^ beta) . 1) & ((2 |^ a) . (sort _ (3,1))) = ((2 |^ gamma) . 1) & (((2 |^ a) *. sort) . 1) = (2 |^ alpha) & (((2 |^ a) *. sort) . 2) = (2 |^ beta) & (((2 |^ a) *. sort) . 3) = (2 |^ gamma);

        

        thus n = ( Sum d) by Def3

        .= ( Sum ( Sum (d *. o1))) by FLEXARY1: 47

        .= ((1 * (mu . 1)) + ((( Sum (d *. o1)),2) +... )) by FLEXARY1: 22, A23

        .= ((1 * (mu . 1)) + ((3 * (mu . 3)) + ((( Sum (d *. o1)),(2 + 1)) +... ))) by A25, FLEXARY1: 20

        .= (((1 * (mu . 1)) + (3 * (mu . 3))) + ((( Sum (d *. o1)),3) +... ))

        .= (((1 * (mu . 1)) + (3 * (mu . 3))) + ((5 * (mu . 5)) + ((( Sum (d *. o1)),(3 + 1)) +... ))) by FLEXARY1: 20, A27

        .= ((((1 * (mu . 1)) + (3 * (mu . 3))) + (5 * (mu . 5))) + (((( id ( dom mu)) (#) mu),7) +... )) by A16, A21

        .= ((((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... ))) + (3 * (mu . 3))) + (5 * (mu . 5))) + (((( id ( dom mu)) (#) mu),7) +... )) by A2, A22

        .= ((((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... ))) + (3 * (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )))) + (5 * (mu . 5))) + (((( id ( dom mu)) (#) mu),7) +... )) by A2, A24

        .= (((((((2 |^ alpha) . 1) + (((2 |^ alpha),2) +... )) * 1) + ((((2 |^ beta) . 1) + (((2 |^ beta),2) +... )) * 3)) + ((((2 |^ gamma) . 1) + (((2 |^ gamma),2) +... )) * 5)) + (((( id ( dom mu)) (#) mu),7) +... )) by A2, A26, A29;

      end;

      

       A30: n = (((((mu . 1) * 1) + ((mu . 3) * 3)) + ((mu . 5) * 5)) + (((( id ( dom mu)) (#) mu),7) +... ))

      proof

        for j holds ((2 |^ a) . (sort _ (j,1))) = ((2 |^ (a * (sort . j))) . 1) & (((2 |^ a) *. sort) . j) = (2 |^ (a * (sort . j)))

        proof

          let j;

          

           A31: ((2 |^ a) . (sort _ (j,1))) = (((2 |^ a) *. sort) _ (j,1)) by FLEXARY1: 42;

          (((2 |^ a) *. sort) . j) = ((2 |^ a) * (sort . j)) by FLEXARY1: 41

          .= (2 |^ (a * (sort . j))) by FLEXARY1: 25;

          hence thesis by A31;

        end;

        then

         A32: ((2 |^ a) . (sort _ (1,1))) = ((2 |^ alpha) . 1) & ((2 |^ a) . (sort _ (2,1))) = ((2 |^ beta) . 1) & ((2 |^ a) . (sort _ (3,1))) = ((2 |^ gamma) . 1) & (((2 |^ a) *. sort) . 1) = (2 |^ alpha) & (((2 |^ a) *. sort) . 2) = (2 |^ beta) & (((2 |^ a) *. sort) . 3) = (2 |^ gamma);

        

         A33: (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... )) = (mu . ((2 * 1) - 1)) by A2;

        

         A34: (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )) = (mu . ((2 * 2) - 1)) by A2;

        (((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +... )) = (mu . ((2 * 3) - 1)) by A2;

        hence thesis by A33, A34, A3, A32;

      end;

      consider h be odd-valued FinSequence such that

       A35: h is non-decreasing & for i holds ( card ( Coim (h,i))) = (mu . i) by Lm3, A2;

      

       A36: n = ((((( card ( Coim (h,1))) * 1) + (( card ( Coim (h,3))) * 3)) + (( card ( Coim (h,5))) * 5)) + (((( id ( dom mu)) (#) mu),7) +... ))

      proof

        

         A37: (mu . 1) = ( card ( Coim (h,1))) by A35;

        (mu . 3) = ( card ( Coim (h,3))) by A35;

        hence thesis by A35, A37, A30;

      end;

      n = ( Sum h)

      proof

        set I = ( idseq ( len mu));

        

         A38: I = ( id ( dom mu)) by FINSEQ_1:def 3;

        then ((I (#) mu) . 3) = (3 * (mu . 3)) by Lm2;

        

        then

         A39: (((I (#) mu),3) +... ) = ((3 * (mu . 3)) + (((I (#) mu),(3 + 1)) +... )) by FLEXARY1: 20

        .= ((3 * ( card ( Coim (h,3)))) + (((I (#) mu),(3 + 1)) +... )) by A35;

        

         A40: ((I (#) mu) . 4) = (4 * (mu . 4)) & 4 = (2 * 2) by A38, Lm2;

        then (mu . 4) = 0 by A2;

        then

         A41: (((I (#) mu),4) +... ) = ( 0 + (((I (#) mu),(4 + 1)) +... )) by A40, FLEXARY1: 20;

        ((I (#) mu) . 5) = (5 * (mu . 5)) by A38, Lm2;

        

        then

         A42: (((I (#) mu),5) +... ) = ((5 * (mu . 5)) + (((I (#) mu),(5 + 1)) +... )) by FLEXARY1: 20

        .= ((5 * ( card ( Coim (h,5)))) + (((I (#) mu),(5 + 1)) +... )) by A35;

        

         A43: ((I (#) mu) . 6) = (6 * (mu . 6)) & 6 = (3 * 2) by A38, Lm2;

        then (mu . 6) = 0 by A2;

        then

         A44: (((I (#) mu),6) +... ) = ( 0 + (((I (#) mu),(6 + 1)) +... )) by A43, FLEXARY1: 20;

        (2 * 1) = 2;

        then (mu . 2) = 0 by A2;

        then (2 * (mu . 2)) = 0 ;

        

        hence ( Sum h) = (((1 * (mu . 1)) + 0 ) + (((( id ( dom mu)) (#) mu),3) +... )) by Th9, A35

        .= ((1 * ( card ( Coim (h,1)))) + (((( id ( dom mu)) (#) mu),3) +... )) by A35

        .= n by A36, A39, A41, A38, A42, A44;

      end;

      then

      reconsider h as odd-valued a_partition of n by A35, Def3;

      take h;

      let j;

      let O1 be odd-valued FinSequence, a1 be natural-valued FinSequence such that

       A45: ( len O1) = ( len d) = ( len a1) & d = (O1 (#) (2 |^ a1));

      let sort1 be DoubleReorganization of ( dom d) such that

       A46: (1 = (O1 . (sort1 _ (1,1))) & ... & 1 = (O1 . (sort1 _ (1,( len (sort1 . 1)))))) & (3 = (O1 . (sort1 _ (2,1))) & ... & 3 = (O1 . (sort1 _ (2,( len (sort1 . 2)))))) & (5 = (O1 . (sort1 _ (3,1))) & ... & 5 = (O1 . (sort1 _ (3,( len (sort1 . 3)))))) & for i holds ((2 * i) - 1) = (O1 . (sort1 _ (i,1))) & ... & ((2 * i) - 1) = (O1 . (sort1 _ (i,( len (sort1 . i)))));

      for j st 1 <= j & j <= ( len d) holds (O . j) = (O1 . j) & (a . j) = (a1 . j)

      proof

        let j such that

         A48: 1 <= j & j <= ( len d);

        

         A49: ((O1 . j) * ((2 |^ a1) . j)) = ((O1 (#) (2 |^ a1)) . j) by VALUED_1: 5

        .= ((O . j) * ((2 |^ a) . j)) by VALUED_1: 5, A1, A45;

        j in ( dom a) by A48, FINSEQ_3: 25, A1;

        

        then

         A50: ((2 |^ a) . j) = (2 to_power (a . j)) by FLEXARY1:def 4

        .= (2 |^ (a . j));

        j in ( dom a1) by A48, FINSEQ_3: 25, A45;

        

        then

         A51: ((2 |^ a1) . j) = (2 to_power (a1 . j)) by FLEXARY1:def 4

        .= (2 |^ (a1 . j));

        j in ( dom O) by A48, FINSEQ_3: 25, A1;

        then (O . j) is odd Nat by Def2;

        then

        consider i1 be Nat such that

         A52: (O . j) = ((2 * i1) + 1) by ABIAN: 9;

        j in ( dom O1) by A48, FINSEQ_3: 25, A45;

        then (O1 . j) is odd Nat by Def2;

        then ex i2 be Nat st (O1 . j) = ((2 * i2) + 1) by ABIAN: 9;

        hence thesis by A50, A51, A52, A49, CARD_4: 4;

      end;

      then

       A53: O = O1 & a = a1 by A45, A1;

      

       A54: for j holds ( card ( Coim (h,((j * 2) - 1)))) = (((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +... ))

      proof

        let j;

        

         A55: ((2 |^ a) . (sort _ (j,1))) = (((2 |^ a) *. sort) _ (j,1)) by FLEXARY1: 42;

        

         A56: ( len (2 |^ a)) = ( len a) by CARD_1:def 7;

        then

         A57: ( dom O) = ( dom d) & ( dom d) = ( dom a) & ( dom (2 |^ a)) = ( dom a) by A1, FINSEQ_3: 29;

        ( card ( Coim (h,((j * 2) - 1)))) = (mu . ((2 * j) - 1))

        proof

          per cases ;

            suppose

             A58: j = 0 ;

            then

             A59: not ((2 * j) - 1) in ( dom mu);

             not ((2 * j) - 1) in ( rng h) by A58;

            then (h " {((2 * j) - 1)}) = {} by FUNCT_1: 72;

            then ( Coim (h,((j * 2) - 1))) = {} by RELAT_1:def 17;

            hence thesis by A59, FUNCT_1:def 2;

          end;

            suppose j > 0 ;

            hence thesis by A35;

          end;

        end;

        

        then

         A60: ( card ( Coim (h,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),2) +... )) by A2, A55

        .= ( Sum (((2 |^ a) *. sort) . j)) by FLEXARY1: 22;

        reconsider S = sort1 as DoubleReorganization of ( dom (2 |^ a)) by A56, A1, FINSEQ_3: 29;

        ((2 |^ a1) . (sort1 _ (j,1))) = (((2 |^ a1) *. sort1) _ (j,1)) by FLEXARY1: 42;

        then

         A61: (((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +... )) = ( Sum (((2 |^ a) *. S) . j)) by A53, FLEXARY1: 22;

        

         A62: sort1 is odd_organization of O by A57, Th4, A46, A53;

        

        thus ( card ( Coim (h,((j * 2) - 1)))) = (( Sum ((2 |^ a) *. sort)) . j) by FLEXARY1:def 8, A60

        .= (( Sum ((2 |^ a) *. S)) . j) by A62, Th5

        .= (((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +... )) by FLEXARY1:def 8, A61;

      end;

      ((2 * 1) - 1) = 1 & ((2 * 2) - 1) = 3 & ((2 * 3) - 1) = 5;

      hence thesis by A54;

    end;

    definition

      let n be Nat;

      let p be one-to-one a_partition of n;

      :: EULRPART:def5

      func Euler_transformation p -> odd-valued a_partition of n means

      : Def5: for O be odd-valued FinSequence, a be natural-valued FinSequence st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for sort be DoubleReorganization of ( dom p) st (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i))))) holds ( card ( Coim (it ,1))) = (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... )) & ( card ( Coim (it ,3))) = (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )) & ( card ( Coim (it ,5))) = (((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +... )) & ( card ( Coim (it ,((j * 2) - 1)))) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... ));

      existence by Th11;

      uniqueness

      proof

        let E1,E2 be odd-valued a_partition of n such that

         A1: for O be odd-valued FinSequence, a be natural-valued FinSequence st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for sort be DoubleReorganization of ( dom p) st (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i))))) holds ( card ( Coim (E1,1))) = (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... )) & ( card ( Coim (E1,3))) = (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )) & ( card ( Coim (E1,5))) = (((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +... )) & ( card ( Coim (E1,((j * 2) - 1)))) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... )) and

         A2: for O be odd-valued FinSequence, a be natural-valued FinSequence st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for sort be DoubleReorganization of ( dom p) st (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i))))) holds ( card ( Coim (E2,1))) = (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... )) & ( card ( Coim (E2,3))) = (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )) & ( card ( Coim (E2,5))) = (((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +... )) & ( card ( Coim (E2,((j * 2) - 1)))) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... ));

        consider O be odd-valued FinSequence, a be natural-valued FinSequence such that

         A3: ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) and (p . 1) = ((O . 1) * (2 |^ (a . 1))) & ... & (p . ( len p)) = ((O . ( len p)) * (2 |^ (a . ( len p)))) by Th6;

        reconsider sort = the odd_organization of O as DoubleReorganization of ( dom p) by A3, FINSEQ_3: 29;

        

         A4: ((2 * 1) - 1) = 1;

        

         A5: ((2 * 2) - 1) = 3;

        ((2 * 3) - 1) = 5;

        then

         A6: (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i))))) by A4, Def4, A5;

        

         A7: for x be object holds ( card ( Coim (E1,x))) = ( card ( Coim (E2,x)))

        proof

          let x be object;

          per cases ;

            suppose

             A8: not x in OddNAT ;

            ( rng E1) c= OddNAT & ( rng E2) c= OddNAT by Def1;

            then (E1 " {x}) = {} & (E2 " {x}) = {} by A8, FUNCT_1: 72;

            then ( Coim (E1,x)) = {} & ( Coim (E2,x)) = {} by RELAT_1:def 17;

            hence thesis;

          end;

            suppose x in OddNAT ;

            then

            consider i be Element of NAT such that

             A9: x = ((2 * i) + 1) by FIB_NUM2:def 4;

            set i1 = (i + 1);

            ( card ( Coim (E1,((i1 * 2) - 1)))) = (((2 |^ a) . (sort _ (i1,1))) + (((((2 |^ a) *. sort) . i1),2) +... )) by A1, A3, A6

            .= ( card ( Coim (E2,((i1 * 2) - 1)))) by A6, A3, A2;

            hence thesis by A9;

          end;

        end;

        thus E1 = E2

        proof

          ( rng E1) c= REAL ;

          then

          reconsider e1 = E1 as FinSequence of REAL by FINSEQ_1:def 4;

          ( rng E2) c= REAL ;

          then

          reconsider e2 = E2 as FinSequence of REAL by FINSEQ_1:def 4;

          e1 = e2 by RFINSEQ2: 19, A7, CLASSES1:def 10;

          hence thesis;

        end;

      end;

    end

    theorem :: EULRPART:12

    

     Th12: for n be Nat, p be one-to-one a_partition of n, e be odd-valued a_partition of n holds e = ( Euler_transformation p) iff for O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for j holds ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... )

    proof

      let n be Nat, p be one-to-one a_partition of n, e be odd-valued a_partition of n;

      thus e = ( Euler_transformation p) implies for O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for j holds ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... )

      proof

        assume

         A1: e = ( Euler_transformation p);

        let O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O such that

         A2: ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a));

        let j;

        ( len (2 |^ a)) = ( len a) by CARD_1:def 7;

        then

         A3: ( dom O) = ( dom p) & ( dom p) = ( dom a) & ( dom (2 |^ a)) = ( dom a) by A2, FINSEQ_3: 29;

        reconsider S = sort as DoubleReorganization of ( dom p) by A2, FINSEQ_3: 29;

        

         A4: ((2 * 1) - 1) = 1;

        

         A5: ((2 * 2) - 1) = 3;

        ((2 * 3) - 1) = 5;

        then

         A6: (1 = (O . (S _ (1,1))) & ... & 1 = (O . (S _ (1,( len (S . 1)))))) & (3 = (O . (S _ (2,1))) & ... & 3 = (O . (S _ (2,( len (S . 2)))))) & (5 = (O . (S _ (3,1))) & ... & 5 = (O . (S _ (3,( len (S . 3)))))) & for i holds ((2 * i) - 1) = (O . (S _ (i,1))) & ... & ((2 * i) - 1) = (O . (S _ (i,( len (S . i))))) by A4, Def4, A5;

        ((2 |^ a) . (sort _ (j,1))) = (((2 |^ a) *. sort) _ (j,1)) by FLEXARY1: 42;

        

        then ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),(1 + 1)) +... )) by A6, A2, A1, Def5

        .= (((((2 |^ a) *. S) . j),1) +... ) by FLEXARY1: 20, A3;

        hence thesis;

      end;

      assume

       A7: for O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for j holds ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... );

      for j holds for O be odd-valued FinSequence, a be natural-valued FinSequence st ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a)) holds for sort be DoubleReorganization of ( dom p) st (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i))))) holds ( card ( Coim (e,1))) = (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +... )) & ( card ( Coim (e,3))) = (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +... )) & ( card ( Coim (e,5))) = (((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +... )) & ( card ( Coim (e,((j * 2) - 1)))) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... ))

      proof

        let j;

        let O be odd-valued FinSequence, a be natural-valued FinSequence;

        assume

         A8: ( len O) = ( len p) = ( len a) & p = (O (#) (2 |^ a));

        let sort be DoubleReorganization of ( dom p);

        assume

         A9: (1 = (O . (sort _ (1,1))) & ... & 1 = (O . (sort _ (1,( len (sort . 1)))))) & (3 = (O . (sort _ (2,1))) & ... & 3 = (O . (sort _ (2,( len (sort . 2)))))) & (5 = (O . (sort _ (3,1))) & ... & 5 = (O . (sort _ (3,( len (sort . 3)))))) & for i holds ((2 * i) - 1) = (O . (sort _ (i,1))) & ... & ((2 * i) - 1) = (O . (sort _ (i,( len (sort . i)))));

        

         A10: for j holds ( card ( Coim (e,((j * 2) - 1)))) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +... ))

        proof

          let j;

          ( len (2 |^ a)) = ( len a) by CARD_1:def 7;

          then

           A11: ( dom O) = ( dom p) & ( dom p) = ( dom a) & ( dom (2 |^ a)) = ( dom a) by A8, FINSEQ_3: 29;

          reconsider S = sort as DoubleReorganization of ( dom p);

          

           A12: sort is odd_organization of O by A11, A9, Th4;

          ((2 |^ a) . (sort _ (j,1))) = (((2 |^ a) *. sort) _ (j,1)) by FLEXARY1: 42;

          then (((((2 |^ a) *. S) . j),1) +... ) = (((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),(1 + 1)) +... )) by A11, FLEXARY1: 20;

          hence thesis by A12, A7, A8;

        end;

        ((1 * 2) - 1) = 1 & ((2 * 2) - 1) = 3 & ((3 * 2) - 1) = 5;

        hence thesis by A10;

      end;

      hence thesis by Def5;

    end;

    registration

      cluster one-to-one non-decreasing -> increasing for real-valued Function;

      coherence

      proof

        let f be real-valued Function;

        assume

         A1: f is one-to-one non-decreasing;

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

        proof

          let e1,e2 be ExtReal such that

           A2: e1 in ( dom f) & e2 in ( dom f) & e1 < e2;

          (f . e1) <= (f . e2) by A1, A2, VALUED_0:def 15;

          hence thesis by XXREAL_0: 1, A2, A1;

        end;

        hence thesis by VALUED_0:def 13;

      end;

    end

    theorem :: EULRPART:13

    

     Th13: for O be odd-valued FinSequence, a be natural-valued FinSequence, s be odd_organization of O st ( len O) = ( len a) & (O (#) (2 |^ a)) is one-to-one holds ((a *. s) . i) is one-to-one

    proof

      let O be odd-valued FinSequence, a be natural-valued FinSequence, s be odd_organization of O;

      set p = (O (#) (2 |^ a));

      assume

       A1: ( len O) = ( len a) & p is one-to-one;

      then

      reconsider S = s as DoubleReorganization of ( dom a) by FINSEQ_3: 29;

      

       A2: ((a *. S) . i) = (a * (S . i)) by FLEXARY1: 41;

      thus ((a *. s) . i) is one-to-one

      proof

        assume not ((a *. s) . i) is one-to-one;

        then

        consider x1,x2 be object such that

         A3: x1 in ( dom ((a *. S) . i)) & x2 in ( dom ((a *. S) . i)) & (((a *. S) . i) . x1) = (((a *. S) . i) . x2) & x1 <> x2;

        reconsider x1, x2 as Nat by A3;

        set s1 = (s _ (i,x1)), s2 = (s _ (i,x2));

        

         A4: x1 in ( dom (s . i)) & s1 in ( dom a) & (a . s1) = (((a *. S) . i) . x1) by A2, A3, FUNCT_1: 11, FUNCT_1: 12;

        

         A5: x2 in ( dom (S . i)) & s2 in ( dom a) & (a . s2) = (((a *. S) . i) . x2) by A2, A3, FUNCT_1: 11, FUNCT_1: 12;

        

         A6: ((2 * i) - 1) = (O . (s _ (i,1))) & ... & ((2 * i) - 1) = (O . (s _ (i,( len (s . i))))) by Def4;

        1 <= x1 & x1 <= ( len (s . i)) by A4, FINSEQ_3: 25;

        then

         A7: ((2 * i) - 1) = (O . s1) by A6;

        1 <= x2 & x2 <= ( len (s . i)) by A5, FINSEQ_3: 25;

        then

         A8: ((2 * i) - 1) = (O . s2) by A6;

        O is ( len O) -element by CARD_1:def 7;

        then

         A9: ( len p) = ( len a) by A1, CARD_1:def 7;

        

         A10: 1 <= ((s . i) . x1) & ((s . i) . x1) <= ( len a) by A4, FINSEQ_3: 25;

        1 <= ((s . i) . x2) & ((s . i) . x2) <= ( len a) by A5, FINSEQ_3: 25;

        then

         A11: s2 in ( dom p) & s1 in ( dom p) by A9, A10, FINSEQ_3: 25;

        

         A12: (p . s1) = ((O . s1) * ((2 |^ a) . s1)) by VALUED_1: 5;

        

         A13: ((2 |^ a) . s1) = (2 to_power (a . s1)) by A4, FLEXARY1:def 4;

        (p . s2) = ((O . s2) * ((2 |^ a) . s2)) by VALUED_1: 5;

        then (p . s2) = (p . s1) by A5, FLEXARY1:def 4, A13, A12, A7, A8, A4, A3;

        then s2 = s1 by A11, A1;

        hence thesis by A4, A5, FUNCT_1:def 4, A3;

      end;

    end;

    

     Lm4: for p1,p2 be one-to-one a_partition of n st ( Euler_transformation p1) = ( Euler_transformation p2) holds ( rng p1) c= ( rng p2)

    proof

      let p1,p2 be one-to-one a_partition of n;

      assume

       A1: ( Euler_transformation p1) = ( Euler_transformation p2);

      consider O1 be odd-valued FinSequence, a1 be natural-valued FinSequence such that

       A2: ( len O1) = ( len p1) = ( len a1) & p1 = (O1 (#) (2 |^ a1)) and

       A3: (p1 . 1) = ((O1 . 1) * (2 |^ (a1 . 1))) & ... & (p1 . ( len p1)) = ((O1 . ( len p1)) * (2 |^ (a1 . ( len p1)))) by Th6;

      set s1 = the odd_organization of O1;

      reconsider S1 = s1 as DoubleReorganization of ( dom a1) by FINSEQ_3: 29, A2;

      consider O2 be odd-valued FinSequence, a2 be natural-valued FinSequence such that

       A4: ( len O2) = ( len p2) = ( len a2) & p2 = (O2 (#) (2 |^ a2)) and

       A5: (p2 . 1) = ((O2 . 1) * (2 |^ (a2 . 1))) & ... & (p2 . ( len p2)) = ((O2 . ( len p2)) * (2 |^ (a2 . ( len p2)))) by Th6;

      set s2 = the odd_organization of O2;

      reconsider S2 = s2 as DoubleReorganization of ( dom a2) by FINSEQ_3: 29, A4;

      

       A6: for j holds ( rng ((a1 *. s1) . j)) = ( rng ((a2 *. s2) . j))

      proof

        let j;

        

         A7: ( card ( Coim (( Euler_transformation p1),((j * 2) - 1)))) = (((((2 |^ a1) *. s1) . j),1) +... ) by A2, Th12

        .= ((((2 |^ a1) * (s1 . j)),1) +... ) by FLEXARY1: 41

        .= (((2 |^ (a1 * (s1 . j))),1) +... ) by FLEXARY1: 25

        .= (((2 |^ (a1 * (S1 . j))) . 1) + (((2 |^ (a1 * (S1 . j))),(1 + 1)) +... )) by FLEXARY1: 20;

        

         A8: ((a2 *. S2) . j) = (a2 * (S2 . j)) by FLEXARY1: 41;

        then

         A9: (a2 * (S2 . j)) is one-to-one natural-valued by A4, Th13;

        ((a1 *. S1) . j) = (a1 * (S1 . j)) by FLEXARY1: 41;

        then

         A10: (a1 * (S1 . j)) is one-to-one natural-valued by A2, Th13;

        ( card ( Coim (( Euler_transformation p2),((j * 2) - 1)))) = (((((2 |^ a2) *. s2) . j),1) +... ) by A4, Th12

        .= ((((2 |^ a2) * (s2 . j)),1) +... ) by FLEXARY1: 41

        .= (((2 |^ (a2 * (s2 . j))),1) +... ) by FLEXARY1: 25

        .= (((2 |^ (a2 * (S2 . j))) . 1) + (((2 |^ (a2 * (S2 . j))),(1 + 1)) +... )) by FLEXARY1: 20;

        then ( rng (a2 * (S2 . j))) = ( rng (a1 * (S1 . j))) by A7, A1, FLEXARY1: 30, A9, A10;

        hence thesis by A8, FLEXARY1: 41;

      end;

      let y be object;

      assume y in ( rng p1);

      then

      consider x be object such that

       A11: x in ( dom p1) & (p1 . x) = y by FUNCT_1:def 3;

      reconsider x as Nat by A11;

      1 <= x & x <= ( len p1) by A11, FINSEQ_3: 25;

      then

       A12: (p1 . x) = ((O1 . x) * (2 |^ (a1 . x))) by A3;

      ( dom p1) = ( dom O1) by A2, FINSEQ_3: 29;

      then x in ( Values s1) by FLEXARY1:def 7, A11;

      then

      consider i,j be object such that

       A13: i in ( dom s1) & j in ( dom (s1 . i)) & x = ((s1 . i) . j) by FLEXARY1: 1;

      reconsider i, j as Nat by A13;

      ( len ((a1 *. S1) . i)) = ( len (S1 . i)) by CARD_1:def 7;

      then

       A14: ( dom ((a1 *. S1) . i)) = ( dom (S1 . i)) by FINSEQ_3: 29;

      then (((a1 *. S1) . i) . j) in ( rng ((a1 *. s1) . i)) by A13, FUNCT_1:def 3;

      then (((a1 *. S1) . i) . j) in ( rng ((a2 *. s2) . i)) by A6;

      then

      consider z be object such that

       A15: z in ( dom ((a2 *. S2) . i)) & (((a2 *. S2) . i) . z) = (((a1 *. S1) . i) . j) by FUNCT_1:def 3;

      reconsider z as Nat by A15;

      set Z = ((S2 . i) . z);

      

       A16: ((a1 *. S1) . i) = (a1 * (S1 . i)) by FLEXARY1: 41;

      

       A17: ((a2 *. S2) . i) = (a2 * (S2 . i)) by FLEXARY1: 41;

      

       A18: ( len ((a2 *. S2) . i)) = ( len (S2 . i)) by CARD_1:def 7;

      

       A19: (((a2 *. S2) . i) . z) = (a2 . Z) & Z in ( dom a2) by A17, A15, FUNCT_1: 11, FUNCT_1: 12;

      then

       A20: Z in ( dom p2) by FINSEQ_3: 29, A4;

      1 <= Z & Z <= ( len p2) by A19, A4, FINSEQ_3: 25;

      then

       A21: (p2 . Z) = ((O2 . Z) * (2 |^ (a2 . Z))) by A5;

      

       A22: (p2 . Z) in ( rng p2) by A20, FUNCT_1:def 3;

      

       A23: 1 <= j & j <= ( len (s1 . i)) by A13, FINSEQ_3: 25;

      ((2 * i) - 1) = (O1 . (s1 _ (i,1))) & ... & ((2 * i) - 1) = (O1 . (s1 _ (i,( len (s1 . i))))) by Def4;

      then

       A24: (O1 . (s1 _ (i,j))) = ((2 * i) - 1) by A23;

      

       A25: 1 <= z & z <= ( len (s2 . i)) by FINSEQ_3: 25, A18, A15;

      ((2 * i) - 1) = (O2 . (s2 _ (i,1))) & ... & ((2 * i) - 1) = (O2 . (s2 _ (i,( len (s2 . i))))) by Def4;

      then (O2 . (s2 _ (i,z))) = ((2 * i) - 1) by A25;

      hence thesis by A24, A13, A22, A21, A15, A16, A14, FUNCT_1: 12, A19, A12, A11;

    end;

    theorem :: EULRPART:14

    

     Th14: for p1,p2 be one-to-one a_partition of n st ( Euler_transformation p1) = ( Euler_transformation p2) holds p1 = p2

    proof

      let p1,p2 be one-to-one a_partition of n;

      assume ( Euler_transformation p1) = ( Euler_transformation p2);

      then

       A1: ( rng p1) = ( rng p2) by Lm4;

      then p1 is FinSequence of REAL & p2 is FinSequence of REAL by FINSEQ_1:def 4;

      hence thesis by INTEGRA3: 6, A1;

    end;

    theorem :: EULRPART:15

    

     Th15: for e be odd-valued a_partition of n holds ex p be one-to-one a_partition of n st e = ( Euler_transformation p)

    proof

      let e be odd-valued a_partition of n;

      

       A1: ( Sum e) = n by Def3;

      deffunc h( object) = ( card ( Coim (e,$1)));

      consider H be FinSequence such that

       A2: ( len H) = n & for k st k in ( dom H) holds (H . k) = h(k) from FINSEQ_1:sch 2;

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

        (H . x) = ( card ( Coim (e,x))) by A3, A2;

        hence thesis by A3;

      end;

      then

      reconsider H as natural-valued FinSequence by VALUED_0:def 6;

      

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

      

       A5: ( Sum e) = ( Sum (( idseq n) (#) H))

      proof

        

         A6: for i st i in ( dom e) holds 0 <= (e . i);

        for i holds ( card ( Coim (e,i))) = (H . i)

        proof

          let i;

          per cases by FINSEQ_3: 25;

            suppose i in ( dom H);

            hence thesis by A2;

          end;

            suppose i < 1;

            then

             A8: not i in ( rng e) & not i in ( dom H) by NAT_1: 14, FINSEQ_3: 25;

            then (H . i) = 0 & (e " {i}) = {} by FUNCT_1:def 2, FUNCT_1: 72;

            then ( Coim (e,i)) = {} by RELAT_1:def 17;

            hence thesis by A8, FUNCT_1:def 2;

          end;

            suppose

             A9: i > ( len H);

            then

             A10: not i in ( dom H) by FINSEQ_3: 25;

            ( Coim (e,i)) = {}

            proof

              assume ( Coim (e,i)) <> {} ;

              then (e " {i}) <> {} by RELAT_1:def 17;

              then i in ( rng e) by FUNCT_1: 72;

              then

              consider x be object such that

               A11: x in ( dom e) & (e . x) = i by FUNCT_1:def 3;

              reconsider x as Nat by A11;

              i <= ( Sum e) by A11, A6, MATRPROB: 5;

              hence thesis by Def3, A9, A2;

            end;

            hence thesis by A10, FUNCT_1:def 2;

          end;

        end;

        

        hence ( Sum e) = (((1 * (H . 1)) + (2 * (H . 2))) + (((( id ( dom H)) (#) H),3) +... )) by Th9

        .= (((1 * (H . 1)) + ((( id ( dom H)) (#) H) . 2)) + (((( id ( dom H)) (#) H),3) +... )) by Lm2

        .= ((((( id ( dom H)) (#) H) . 1) + ((( id ( dom H)) (#) H) . 2)) + (((( id ( dom H)) (#) H),3) +... )) by Lm2

        .= (((( id ( dom H)) (#) H) . 1) + (((( id ( dom H)) (#) H) . 2) + (((( id ( dom H)) (#) H),(2 + 1)) +... )))

        .= (((( id ( dom H)) (#) H) . 1) + (((( id ( dom H)) (#) H),2) +... )) by FLEXARY1: 20

        .= ( Sum (( idseq n) (#) H)) by A4, A2, FLEXARY1: 22;

      end;

      defpred F[ Nat, object] means ex f be increasing natural-valued FinSequence st (H . $1) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & $2 = ($1 * (2 |^ f));

      ex p be FinSequence of ( NAT * ) st ( dom p) = ( Seg ( len H)) & for k st k in ( Seg ( len H)) holds F[k, (p . k)]

      proof

        

         A12: for k st k in ( Seg ( len H)) holds ex x be object st F[k, x]

        proof

          let k;

          assume k in ( Seg ( len H));

          consider f be increasing natural-valued FinSequence such that

           A13: (H . k) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) by FLEXARY1: 31;

          take G = (k * (2 |^ f));

          thus thesis by A13;

        end;

        consider p be FinSequence such that

         A14: ( dom p) = ( Seg ( len H)) & for k st k in ( Seg ( len H)) holds F[k, (p . k)] from FINSEQ_1:sch 1( A12);

        ( rng p) c= ( NAT * )

        proof

          let y be object;

          assume y in ( rng p);

          then

          consider x be object such that

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

          reconsider x as Nat by A15;

          consider f be increasing natural-valued FinSequence such that

           A16: (H . x) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . x) = (x * (2 |^ f)) by A15, A14;

          ( rng (x * (2 |^ f))) c= NAT by VALUED_0:def 6;

          then (x * (2 |^ f)) is FinSequence of NAT by FINSEQ_1:def 4;

          hence thesis by FINSEQ_1:def 11, A15, A16;

        end;

        then p is FinSequence of ( NAT * ) by FINSEQ_1:def 4;

        hence thesis by A14;

      end;

      then

      consider p be FinSequence of ( NAT * ) such that

       A17: ( dom p) = ( Seg ( len H)) & for k st k in ( Seg ( len H)) holds F[k, (p . k)];

      

       A18: for k st (p . k) <> {} holds k is odd

      proof

        let k;

        assume

         A19: (p . k) <> {} ;

        then

         A20: k in ( dom p) by FUNCT_1:def 2;

        then

        consider f be increasing natural-valued FinSequence such that

         A21: (H . k) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . k) = (k * (2 |^ f)) by A17;

        consider j be object such that

         A22: j in ( dom (p . k)) by A19, XBOOLE_0:def 1;

        reconsider j as Nat by A22;

        

         A23: ( dom (p . k)) = ( dom (2 |^ f)) by A21, VALUED_1:def 5;

        then j in ( dom f) by A22, FLEXARY1:def 4;

        

        then ((2 |^ f) . j) = (2 to_power (f . j)) by FLEXARY1:def 4

        .= (2 |^ (f . j));

        then

         A24: ((2 |^ f) . j) > 0 by NEWTON: 83;

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

        then

         A25: ( Sum (2 |^ f)) > 0 by A22, A24, A23, RVSUM_1: 85;

        

         A26: ( rng e) c= OddNAT by Def1;

        (H . k) = ( card ( Coim (e,k))) by A20, A4, A17, A2;

        then ( Coim (e,k)) <> {} by FLEXARY1: 22, A25, A21;

        then (e " {k}) <> {} by RELAT_1:def 17;

        then k in OddNAT by FUNCT_1: 72, A26;

        hence thesis by Th2;

      end;

      

       A27: H is n -element complex-valued by A2, CARD_1:def 7;

      ( len p) = n by A17, A2, FINSEQ_1:def 3;

      then

       A28: ( len ( Sum p)) = n by CARD_1:def 7;

      now

        let i;

        assume 1 <= i & i <= n;

        then i in ( Seg ( len H)) by A2;

        then

        consider f be increasing natural-valued FinSequence such that

         A29: (H . i) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . i) = (i * (2 |^ f)) by A17;

        

        thus (( Sum p) . i) = ( Sum (i * (2 |^ f))) by A29, FLEXARY1:def 8

        .= (i * ( Sum (2 |^ f))) by RVSUM_1: 87

        .= (i * (H . i)) by A29, FLEXARY1: 22

        .= ((( idseq n) (#) H) . i) by A4, A2, Lm2;

      end;

      then

       A30: ( Sum p) = (( idseq n) (#) H) by CARD_1:def 7, A27, A28;

      set NC = ( NAT -concatenation ), np = (NC "**" p);

      ( NAT * ) c= ( COMPLEX * ) by NUMBERS: 20, FINSEQ_1: 62;

      then

      reconsider p1 = p as FinSequence of ( COMPLEX * ) by FINSEQ_2: 24;

      ( rng np) c= REAL ;

      then

      reconsider np as FinSequence of REAL by FINSEQ_1:def 4;

      set sp = ( sort_a np);

      ( Sum (( COMPLEX -concatenation ) "**" p1)) = ( Sum np) by FLEXARY1: 5;

      then

       A31: ( Sum np) = n by FLEXARY1: 48, A30, A5, A1;

      

       A32: ( Sum sp) = n by RFINSEQ2:def 6, RFINSEQ: 9, A31;

      

       A33: ( rng sp) = ( rng np) by RFINSEQ2:def 6, CLASSES1: 75;

      

       A34: ( rng np) = ( Values p) by FLEXARY1: 4;

      sp is one-to-one a_partition of n

      proof

         not 0 in ( rng sp)

        proof

          assume 0 in ( rng sp);

          then

          consider x,y be object such that

           A35: x in ( dom p) & y in ( dom (p . x)) & 0 = ((p . x) . y) by A33, A34, FLEXARY1: 1;

          reconsider x, y as Nat by A35;

          consider f be increasing natural-valued FinSequence such that

           A36: (H . x) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . x) = (x * (2 |^ f)) by A35, A17;

          

           A37: 1 <= x by A35, FINSEQ_3: 25;

          

           A38: ((x * (2 |^ f)) . y) = (x * ((2 |^ f) . y)) by RVSUM_1: 45;

          y in ( dom (2 |^ f)) by A35, A36, VALUED_1:def 5;

          then y in ( dom f) by FLEXARY1:def 4;

          

          then ((2 |^ f) . y) = (2 to_power (f . y)) by FLEXARY1:def 4

          .= (2 |^ (f . y));

          then ((2 |^ f) . y) > 0 by NEWTON: 83;

          hence thesis by A35, A36, A37, A38;

        end;

        then

         A39: sp is non-zero by ORDINAL1:def 15;

        

         A40: ( Sum sp) = n by RFINSEQ2:def 6, RFINSEQ: 9, A31;

        

         A41: sp is natural-valued by A34, A33, VALUED_0:def 6;

        sp is one-to-one

        proof

          now

            let x1,x2 be set such that

             A42: x1 in ( dom sp) & x2 in ( dom sp) & (sp . x1) = (sp . x2);

            (sp . x1) in {(sp . x1)} by TARSKI:def 1;

            then

             A43: x1 in (sp " {(sp . x1)}) & x2 in (sp " {(sp . x1)}) by FUNCT_1:def 7, A42;

            assume x1 <> x2;

            then not (sp " {(sp . x1)}) is trivial by A43, SUBSET_1:def 7;

            then

             A44: ( card (sp " {(sp . x1)})) >= 2 by NAT_D: 60;

            ( card ( Coim (sp,(sp . x1)))) = ( card ( Coim (np,(sp . x1)))) by CLASSES1:def 10, RFINSEQ2:def 6;

            then ( card ( Coim (np,(sp . x1)))) >= 2 by A44, RELAT_1:def 17;

            then

             A45: ( card (np " {(sp . x1)})) >= 2 by RELAT_1:def 17;

            then not (np " {(sp . x1)}) is trivial by NAT_D: 60;

            then

            consider d1,d2 be Element of (np " {(sp . x1)}) such that

             A46: d1 <> d2 by SUBSET_1:def 7;

            (np " {(sp . x1)}) is non empty by A45;

            then

             A47: d1 in ( dom np) & (np . d1) in {(sp . x1)} & d2 in ( dom np) & (np . d2) in {(sp . x1)} by FUNCT_1:def 7;

            then

             A48: (np . d1) = (sp . x1) & (np . d2) = (sp . x1) by TARSKI:def 1;

            consider n1,k1 be Nat such that

             A49: (n1 + 1) in ( dom p) & k1 in ( dom (p . (n1 + 1))) & d1 = (k1 + ( len (NC "**" (p | n1)))) by FLEXARY1: 6, A47;

            set n2 = (n1 + 1);

            

             A50: (np . d1) = ((p . n2) . k1) by FLEXARY1: 8, A49;

            consider f be increasing natural-valued FinSequence such that

             A51: (H . n2) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . n2) = (n2 * (2 |^ f)) by A49, A17;

            

             A52: ((p . n2) . k1) = (n2 * ((2 |^ f) . k1)) by A51, RVSUM_1: 45;

            k1 in ( dom (2 |^ f)) by A49, A51, VALUED_1:def 5;

            then

             A53: k1 in ( dom f) by FLEXARY1:def 4;

            

            then

             A54: ((2 |^ f) . k1) = (2 to_power (f . k1)) by FLEXARY1:def 4

            .= (2 |^ (f . k1));

            consider n3,k3 be Nat such that

             A55: (n3 + 1) in ( dom p) & k3 in ( dom (p . (n3 + 1))) & d2 = (k3 + ( len (NC "**" (p | n3)))) by FLEXARY1: 6, A47;

            set n4 = (n3 + 1);

            consider g be increasing natural-valued FinSequence such that

             A56: (H . n4) = (((2 |^ g) . 1) + (((2 |^ g),2) +... )) & (p . n4) = (n4 * (2 |^ g)) by A55, A17;

            k3 in ( dom (2 |^ g)) by A55, A56, VALUED_1:def 5;

            then

             A57: k3 in ( dom g) by FLEXARY1:def 4;

            

            then

             A58: ((2 |^ g) . k3) = (2 to_power (g . k3)) by FLEXARY1:def 4

            .= (2 |^ (g . k3));

            

             A59: (p . n4) <> {} & (p . n2) <> {} by A55, A49;

            then

            consider c2 be Nat such that

             A60: n2 = ((2 * c2) + 1) by A18, ABIAN: 9;

            consider c4 be Nat such that

             A61: n4 = ((2 * c4) + 1) by A59, A18, ABIAN: 9;

            ((p . n2) . k1) = ((p . n4) . k3) by A48, A50, FLEXARY1: 8, A55;

            then

             A62: (n2 * (2 |^ (f . k1))) = (n4 * (2 |^ (g . k3))) by A56, RVSUM_1: 45, A58, A52, A54;

            then

             A63: c2 = c4 & (f . k1) = (g . k3) by A60, A61, CARD_4: 4;

            n4 = n2 by A62, A60, A61, CARD_4: 4;

            then

             A64: f = g by A51, A56, FLEXARY1: 27;

            f is one-to-one;

            hence thesis by A57, A53, A64, A63, A49, A55, A60, A61, A46;

          end;

          hence thesis;

        end;

        hence thesis by Def3, A39, A41, A40;

      end;

      then

      reconsider sp as one-to-one a_partition of n;

      take sp;

      for O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O st ( len O) = ( len sp) = ( len a) & sp = (O (#) (2 |^ a)) holds for j holds ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... )

      proof

        let O be odd-valued FinSequence, a be natural-valued FinSequence, sort be odd_organization of O such that

         A65: ( len O) = ( len sp) = ( len a) & sp = (O (#) (2 |^ a));

        let j;

        

         A66: ( dom a) = ( dom sp) = ( dom O) & ( dom a) = ( dom (2 |^ a)) by FLEXARY1:def 4, FINSEQ_3: 29, A65;

        then

        reconsider S = sort as DoubleReorganization of ( dom (2 |^ a));

        

         A67: ((2 * j) - 1) = (O . (sort _ (j,1))) & ... & ((2 * j) - 1) = (O . (sort _ (j,( len (sort . j))))) by Def4;

        per cases ;

          suppose

           A68: j < 1;

          then j = 0 by NAT_1: 14;

          then not ((2 * j) - 1) in ( rng e);

          then (e " {((2 * j) - 1)}) = {} by FUNCT_1: 72;

          then

           A69: ( Coim (e,((2 * j) - 1))) = {} by RELAT_1:def 17;

           not j in ( dom ((2 |^ a) *. S)) by FINSEQ_3: 25, A68;

          then ( Sum (((2 |^ a) *. S) . j)) = 0 by FUNCT_1:def 2, RVSUM_1: 72;

          hence ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... ) by FLEXARY1: 21, A69;

        end;

          suppose

           A70: ((j * 2) - 1) > n;

          

           A71: ( Coim (e,((j * 2) - 1))) = {}

          proof

            assume ( Coim (e,((j * 2) - 1))) <> {} ;

            then (e " {((j * 2) - 1)}) <> 0 by RELAT_1:def 17;

            then ((2 * j) - 1) in ( rng e) by FUNCT_1: 72;

            then

            consider w be object such that

             A72: w in ( dom e) & (e . w) = ((2 * j) - 1) by FUNCT_1:def 3;

            for i st i in ( dom e) holds 0 <= (e . i);

            hence thesis by A72, MATRPROB: 5, A1, A70;

          end;

          (((2 |^ a) *. S) . j) = {}

          proof

            set L = ( len (S . j)), SjL = ((S . j) . L);

            assume

             A74: (((2 |^ a) *. S) . j) <> {} ;

            ( len (((2 |^ a) *. S) . j)) = L by CARD_1:def 7;

            then

             A75: L >= 1 by A74, NAT_1: 14;

            then

             A76: ((2 * j) - 1) = (O . (sort _ (j,L))) by A67;

            (S . j) <> {} by A74;

            then

             A77: j in ( dom S) by FUNCT_1:def 2;

            L in ( dom (S . j)) by A75, FINSEQ_3: 25;

            then

             A78: SjL in ( Values S) by FLEXARY1: 1, A77;

            then

             A79: SjL in ( dom O) by FLEXARY1:def 7;

            then

             A80: (sp . SjL) = ((O . SjL) * ((2 |^ a) . SjL)) by VALUED_1:def 4, A66, A65;

            

             A81: ((2 |^ a) . SjL) = (2 to_power (a . SjL)) by FLEXARY1:def 4, A66, A79;

            

             A82: for i st i in ( dom sp) holds 0 <= (sp . i);

            (2 |^ (a . SjL)) > 0 by NEWTON: 83;

            then (2 |^ (a . SjL)) >= 1 by NAT_1: 14;

            then

             A83: (sp . SjL) >= (1 * ((2 * j) - 1)) by A76, A80, A81, XREAL_1: 66;

            SjL in ( dom sp) by A78, FLEXARY1:def 7, A66;

            then (sp . SjL) <= n by A82, MATRPROB: 5, A32;

            hence thesis by A83, A70, XXREAL_0: 2;

          end;

          hence ( card ( Coim (e,((j * 2) - 1)))) = (((((2 |^ a) *. sort) . j),1) +... ) by RVSUM_1: 72, FLEXARY1: 21, A71;

        end;

          suppose

           A84: j >= 1 & ((j * 2) - 1) <= n;

          set J = ((j * 2) - 1);

          (2 * j) >= (2 * 1) by A84, XREAL_1: 64;

          then

           A85: J >= (2 - 1) by XREAL_1: 9;

          then

          consider f be increasing natural-valued FinSequence such that

           A86: (H . J) = (((2 |^ f) . 1) + (((2 |^ f),2) +... )) & (p . J) = (J * (2 |^ f)) by A84, FINSEQ_3: 25, A2, A17, A4;

          reconsider j1 = (j - 1) as Nat by A84;

          

           A87: J = ((2 * j1) + 1);

          

           A88: (((2 |^ a) *. S) . j) is FinSequence of REAL by RVSUM_1: 145;

          

           A89: (2 |^ f) is FinSequence of REAL by RVSUM_1: 145;

          for x be object holds ( card ( Coim ((((2 |^ a) *. sort) . j),x))) = ( card ( Coim ((2 |^ f),x)))

          proof

            let y be object;

            set AS = (((2 |^ a) *. sort) . j);

            

             A90: (((2 |^ a) *. S) . j) = ((2 |^ a) * (S . j)) by FLEXARY1: 41;

            

             A91: ((a *. sort) . j) is one-to-one by Th13, A65;

            

             A92: y in ( rng AS) implies y in ( rng (2 |^ f))

            proof

              assume y in ( rng AS);

              then

              consider x be object such that

               A93: x in ( dom (((2 |^ a) *. S) . j)) & ((((2 |^ a) *. S) . j) . x) = y by FUNCT_1:def 3;

              reconsider x as Nat by A93;

              set Sjx = ((S . j) . x);

              

               A94: x in ( dom (S . j)) & Sjx in ( dom (2 |^ a)) by A90, A93, FUNCT_1: 11;

              then

               A95: 1 <= x & x <= ( len (S . j)) by FINSEQ_3: 25;

              J = (O . (sort _ (j,1))) & ... & J = (O . (sort _ (j,( len (sort . j))))) by Def4;

              then

               A96: J = (O . (sort _ (j,x))) by A95;

              Sjx in ( dom a) by A94, FLEXARY1:def 4;

              then

               A97: ((2 |^ a) . Sjx) = (2 to_power (a . Sjx)) by FLEXARY1:def 4;

              (sp . Sjx) in ( Values p) by A66, A94, FUNCT_1:def 3, A33, A34;

              then

              consider u,w be object such that

               A98: u in ( dom p) & w in ( dom (p . u)) & (sp . Sjx) = ((p . u) . w) by FLEXARY1: 1;

              reconsider u, w as Nat by A98;

              (p . u) <> {} by A98;

              then

              consider s be Nat such that

               A99: u = ((2 * s) + 1) by A18, ABIAN: 9;

              consider fu be increasing natural-valued FinSequence such that

               A100: (H . u) = (((2 |^ fu) . 1) + (((2 |^ fu),2) +... )) & (p . u) = (u * (2 |^ fu)) by A17, A98;

              

               A101: ((p . u) . w) = (u * ((2 |^ fu) . w)) by A100, RVSUM_1: 45;

              w in ( dom (2 |^ fu)) by A100, A98, VALUED_1:def 5;

              then w in ( dom fu) by FLEXARY1:def 4;

              then

               A102: ((2 |^ fu) . w) = (2 to_power (fu . w)) by FLEXARY1:def 4;

              then

               A103: (J * (2 |^ (a . Sjx))) = (((2 * s) + 1) * (2 |^ (fu . w))) by A98, A101, A99, A65, VALUED_1: 5, A97, A96;

              then

               A104: j1 = s & (a . Sjx) = (fu . w) by CARD_4: 4, A87;

              

               A105: (u * (2 |^ fu)) = (J * (2 |^ f)) by A103, CARD_4: 4, A87, A100, A86, A99;

              then

               A106: w in ( dom (2 |^ f)) by A98, A100, VALUED_1:def 5;

              (u * ((2 |^ fu) . w)) = (J * ((2 |^ f) . w)) by A105, A100, A101, RVSUM_1: 45;

              then

               A107: ((2 |^ fu) . w) = ((2 |^ f) . w) by A104, A99, XCMPLX_1: 5;

              y = ((2 |^ fu) . w) by A102, A104, A90, A93, FUNCT_1: 12, A97;

              hence thesis by A106, A107, FUNCT_1:def 3;

            end;

            

             A108: y in ( rng (2 |^ f)) implies y in ( rng AS)

            proof

              assume y in ( rng (2 |^ f));

              then

              consider x be object such that

               A109: x in ( dom (2 |^ f)) & ((2 |^ f) . x) = y by FUNCT_1:def 3;

              reconsider x as Nat by A109;

              x in ( dom f) by A109, FLEXARY1:def 4;

              then

               A110: ((2 |^ f) . x) = (2 to_power (f . x)) by FLEXARY1:def 4;

              

               A111: x in ( dom (p . J)) by A86, A109, VALUED_1:def 5;

              set pJx = ((p . J) . x);

              J in ( dom p) by A85, A84, A2, A17;

              then pJx in ( rng sp) by FLEXARY1: 1, A111, A33, A34;

              then

              consider w be object such that

               A112: w in ( dom sp) & (sp . w) = pJx by FUNCT_1:def 3;

              reconsider w as Nat by A112;

              

               A113: (sp . w) = ((O . w) * ((2 |^ a) . w)) by A65, VALUED_1: 5;

              ( Values sort) = ( dom O) by FLEXARY1:def 7;

              then

              consider r,t be object such that

               A114: r in ( dom S) & t in ( dom (S . r)) & ((S . r) . t) = w by FLEXARY1: 1, A112, A66;

              reconsider r, t as Nat by A114;

              1 <= r by A114, FINSEQ_3: 25;

              then

              reconsider r1 = (r - 1) as Nat;

              set R = ((2 * r) - 1);

              

               A115: R = (O . (sort _ (r,1))) & ... & R = (O . (sort _ (r,( len (sort . r))))) by Def4;

              1 <= t & t <= ( len (S . r)) by A114, FINSEQ_3: 25;

              then

               A116: R = (O . (sort _ (r,t))) by A115;

              

               A117: ((2 |^ a) . w) = (2 to_power (a . w)) by A112, A66, FLEXARY1:def 4;

              then (J * (2 |^ (f . x))) = (((2 * r1) + 1) * (2 |^ (a . w))) by A110, A113, A86, RVSUM_1: 45, A112, A116, A114;

              then

               A118: j1 = r1 & (f . x) = (a . w) by CARD_4: 4, A87;

              then

               A119: t in ( dom ((2 |^ a) * (S . j))) by A112, A66, A114, FUNCT_1: 11;

              then (((2 |^ a) * (S . j)) . t) = ((2 |^ f) . x) by A114, A118, FUNCT_1: 12, A110, A117;

              hence thesis by A109, A119, A90, FUNCT_1:def 3;

            end;

            per cases ;

              suppose

               A120: ( Coim (AS,y)) = {} ;

              ( Coim ((2 |^ f),y)) = {}

              proof

                assume ( Coim ((2 |^ f),y)) <> {} ;

                then ((2 |^ f) " {y}) <> {} by RELAT_1:def 17;

                then (AS " {y}) <> {} by FUNCT_1: 72, A108;

                hence thesis by RELAT_1:def 17, A120;

              end;

              hence thesis by A120;

            end;

              suppose ( Coim (AS,y)) <> {} ;

              then

               A121: (AS " {y}) <> {} by RELAT_1:def 17;

              then

               A122: y in ( rng AS) by FUNCT_1: 72;

              

               A123: (2 + 0 ) = 2;

              (((2 |^ a) *. S) . j) = (2 |^ (a * (S . j))) by FLEXARY1: 25, A90

              .= (2 |^ ((a *. S) . j)) by FLEXARY1: 41;

              then ex x st (AS " {y}) = {x} by A91, A123, A122, FUNCT_1: 74;

              then

               A124: ( card ( Coim (AS,y))) = 1 by CARD_2: 42, RELAT_1:def 17;

              ex x st ((2 |^ f) " {y}) = {x} by A121, FUNCT_1: 72, A92, A123, FUNCT_1: 74;

              hence thesis by CARD_2: 42, A124, RELAT_1:def 17;

            end;

          end;

          

          then ( Sum (((2 |^ a) *. S) . j)) = ( Sum (2 |^ f)) by CLASSES1:def 10, A89, A88, RFINSEQ: 9

          .= (((2 |^ f) . 1) + (((2 |^ f),2) +... )) by FLEXARY1: 22

          .= ( card ( Coim (e,J))) by A85, A84, FINSEQ_3: 25, A2, A86;

          hence thesis by FLEXARY1: 21;

        end;

      end;

      hence thesis by Th12;

    end;

    begin

    ::$Notion-Name

    theorem :: EULRPART:16

    ( card the set of all p where p be odd-valued a_partition of n) = ( card the set of all p where p be one-to-one a_partition of n)

    proof

      set OddVall = the set of all p where p be odd-valued a_partition of n;

      set OneToOne = the set of all p where p be one-to-one a_partition of n;

      

       A1: the odd-valued a_partition of n in OddVall;

      ex E be Function of OneToOne, OddVall st for p be one-to-one a_partition of n holds (E . p) = ( Euler_transformation p)

      proof

        defpred P[ object, object] means for p be one-to-one a_partition of n st p = $1 holds $2 = ( Euler_transformation p);

        

         A2: for x be object st x in OneToOne holds ex y be object st y in OddVall & P[x, y]

        proof

          let x be object;

          assume x in OneToOne;

          then ex q be one-to-one a_partition of n st x = q & not contradiction;

          then

          reconsider x as one-to-one a_partition of n;

          take ( Euler_transformation x);

          thus thesis;

        end;

        consider f be Function of OneToOne, OddVall such that

         A3: for x be object st x in OneToOne holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

        take f;

        let p be one-to-one a_partition of n;

        p in OneToOne;

        hence thesis by A3;

      end;

      then

      consider E be Function of OneToOne, OddVall such that

       A4: for p be one-to-one a_partition of n holds (E . p) = ( Euler_transformation p);

      

       A5: ( dom E) = OneToOne by A1, FUNCT_2:def 1;

      OddVall c= ( rng E)

      proof

        let p be object;

        assume p in OddVall;

        then ex o be odd-valued a_partition of n st o = p & not contradiction;

        then

        reconsider p as odd-valued a_partition of n;

        consider q be one-to-one a_partition of n such that

         A6: p = ( Euler_transformation q) by Th15;

        q in ( dom E) & p = (E . q) by A6, A4, A5;

        hence thesis by FUNCT_1:def 3;

      end;

      then

       A7: ( rng E) = OddVall;

      E is one-to-one

      proof

        let p1,p2 be object;

        assume

         A8: p1 in ( dom E) & p2 in ( dom E) & (E . p1) = (E . p2);

        then (ex o be one-to-one a_partition of n st o = p1 & not contradiction) & ex o be one-to-one a_partition of n st o = p2 & not contradiction by A5;

        then

        reconsider p1, p2 as one-to-one a_partition of n;

        (E . p1) = ( Euler_transformation p1) & (E . p2) = ( Euler_transformation p2) by A4;

        hence thesis by Th14, A8;

      end;

      hence thesis by A5, A7, CARD_1: 70;

    end;