catalan2.miz



    begin

    reserve x,x1,x2,y,X,D for set,

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

p,q for XFinSequence of NAT ,

q9 for XFinSequence,

pd,qd for XFinSequence of D;

    definition

      let p, q;

      :: original: ^

      redefine

      func p ^ q -> XFinSequence of NAT ;

      coherence ;

    end

    theorem :: CATALAN2:1

    

     Th1: ex qd st pd = ((pd | n) ^ qd)

    proof

      consider q9 such that

       A1: pd = ((pd | n) ^ q9) by AFINSQ_1: 60;

      ( rng q9) c= ( rng pd) by A1, AFINSQ_1: 25;

      then ( rng q9) c= D by XBOOLE_1: 1;

      then q9 is XFinSequence of D by RELAT_1:def 19;

      hence thesis by A1;

    end;

    definition

      let p;

      :: CATALAN2:def1

      attr p is dominated_by_0 means ( rng p) c= { 0 , 1} & for k st k <= ( dom p) holds (2 * ( Sum (p | k))) <= k;

    end

    theorem :: CATALAN2:2

    

     Th2: p is dominated_by_0 implies (2 * ( Sum (p | k))) <= k

    proof

      assume

       A1: p is dominated_by_0;

      now

        per cases ;

          suppose k <= ( dom p);

          hence thesis by A1;

        end;

          suppose

           A2: k > ( dom p);

          then ( Segm ( len p)) c= ( Segm k) by NAT_1: 39;

          then

           A3: (p | k) = p by RELAT_1: 68;

          (2 * ( Sum (p | ( len p)))) <= ( dom p) & (p | ( len p)) = p by A1;

          hence thesis by A2, A3, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:3

    

     Th3: p is dominated_by_0 implies (p . 0 ) = 0

    proof

      assume

       A1: p is dominated_by_0;

      now

        per cases ;

          suppose not 0 in ( dom p);

          hence thesis by FUNCT_1:def 2;

        end;

          suppose 0 in ( dom p);

          then ( len p) >= 1 by NAT_1: 14;

          then

           A2: ( Segm 1) c= ( Segm ( len p)) by NAT_1: 39;

           0 in ( Segm 1) by NAT_1: 44;

          then 0 in (( dom p) /\ ( Segm 1)) by A2, XBOOLE_0:def 4;

          then

           A3: ((p | 1) . 0 ) = (p . 0 ) by FUNCT_1: 48;

          

           A4: ( Sum <%(p . 0 )%>) = ( addnat "**" <%(p . 0 )%>) by AFINSQ_2: 51

          .= (p . 0 ) by AFINSQ_2: 37;

          ( len (p | 1)) = 1 by A2, RELAT_1: 62;

          then (p | 1) = <%(p . 0 )%> by A3, AFINSQ_1: 34;

          then (2 * (p . 0 )) <= (1 + 0 qua Nat) by A1, A4, Th2;

          then (2 * (p . 0 )) = 1 or (2 * (p . 0 )) = 0 by NAT_1: 9;

          hence thesis by NAT_1: 15;

        end;

      end;

      hence thesis;

    end;

    registration

      let x;

      let k be Nat;

      cluster (x --> k) -> NAT -valued;

      coherence

      proof

        k in NAT by ORDINAL1:def 12;

        then ( rng (x --> k)) c= {k} & {k} c= NAT by ZFMISC_1: 31;

        then ( rng (x --> k)) c= NAT ;

        hence thesis by RELAT_1:def 19;

      end;

    end

    

     Lm1: n <= m implies ((m --> k) | n) = (n --> k)

    proof

      assume n <= m;

      then ( Segm n) c= ( Segm m) by NAT_1: 39;

      then (n /\ m) = n by XBOOLE_1: 28;

      hence thesis by FUNCOP_1: 12;

    end;

    

     Lm2: (k --> 0 ) is dominated_by_0

    proof

      ( rng (k --> 0 )) c= { 0 } & { 0 } c= { 0 , 1} by FUNCOP_1: 13, ZFMISC_1: 7;

      hence ( rng (k --> 0 )) c= { 0 , 1};

      let n;

      assume n <= ( dom (k --> 0 ));

      then

       A2: ((k --> 0 ) | n) = (n --> 0 ) by Lm1;

      ( Sum (n --> 0 )) = ( 0 * n) by AFINSQ_2: 58;

      hence thesis by A2;

    end;

    registration

      cluster empty dominated_by_0 for XFinSequence of NAT ;

      existence

      proof

        ( 0 --> 0 ) is dominated_by_0 by Lm2;

        hence thesis;

      end;

      cluster non empty dominated_by_0 for XFinSequence of NAT ;

      existence

      proof

        (1 --> 0 ) is dominated_by_0 by Lm2;

        hence thesis;

      end;

    end

    theorem :: CATALAN2:4

    (n --> 0 ) is dominated_by_0 by Lm2;

    theorem :: CATALAN2:5

    

     Th5: n >= m implies ((n --> 0 ) ^ (m --> 1)) is dominated_by_0

    proof

      assume

       A1: n >= m;

      set p = ((n --> 0 ) ^ (m --> 1));

      ( rng (m --> 1)) c= {1} & {1} c= { 0 , 1} by FUNCOP_1: 13, ZFMISC_1: 7;

      then

       A2: ( rng (m --> 1)) c= { 0 , 1};

      ( rng (n --> 0 )) c= { 0 } & { 0 } c= { 0 , 1} by FUNCOP_1: 13, ZFMISC_1: 7;

      then ( rng (n --> 0 )) c= { 0 , 1};

      then (( rng (n --> 0 )) \/ ( rng (m --> 1))) c= { 0 , 1} by A2, XBOOLE_1: 8;

      hence ( rng p) c= { 0 , 1} by AFINSQ_1: 26;

      let k such that

       A3: k <= ( dom p);

      now

        per cases ;

          suppose

           A4: k <= ( dom (n --> 0 ));

          

           A5: ((n --> 0 ) | k) = (k --> 0 ) by A4, Lm1;

          

           A6: ( Sum (k --> 0 )) = ( 0 * k) by AFINSQ_2: 58;

          (p | k) = ((n --> 0 ) | k) by A4, AFINSQ_1: 58;

          hence thesis by A5, A6;

        end;

          suppose k > ( dom (n --> 0 ));

          then

          reconsider kd = (k - ( dom (n --> 0 ))) as Nat by NAT_1: 21;

          k <= (( len (n --> 0 )) + ( len (m --> 1))) by A3, AFINSQ_1: 17;

          then (k - ( len (n --> 0 ))) <= ((( len (m --> 1)) + ( len (n --> 0 ))) - ( len (n --> 0 ))) by XREAL_1: 9;

          then kd <= m;

          then

           A8: ((m --> 1) | kd) = (kd --> 1) by Lm1;

          reconsider m1 = (m --> 1) as XFinSequence of NAT ;

          k = (kd + ( dom (n --> 0 )));

          then (p | k) = ((n --> 0 ) ^ (m1 | kd)) by AFINSQ_1: 59;

          then

           A9: ( Sum (p | k)) = (( Sum (n --> 0 )) + ( Sum (kd --> 1))) by A8, AFINSQ_2: 55;

          ( dom p) = (( len (n --> 0 )) + ( len (m --> 1))) & ( dom (m --> 1)) = m by AFINSQ_1:def 3;

          then (k - n) <= ((m + n) - n) by A3, XREAL_1: 9;

          then (k - n) <= n by A1, XXREAL_0: 2;

          then

           A10: ((k - n) + (k - n)) <= (n + (k - n)) by XREAL_1: 6;

          ( Sum (n --> 0 )) = (n * 0 ) & ( Sum (kd --> 1)) = (kd * 1) by AFINSQ_2: 58;

          hence thesis by A9, A10;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:6

    

     Th6: p is dominated_by_0 implies (p | n) is dominated_by_0

    proof

      assume

       A1: p is dominated_by_0;

      

       A2: for k st k <= ( dom (p | n)) holds (2 * ( Sum ((p | n) | k))) <= k

      proof

        let k;

        assume k <= ( dom (p | n));

        then

         A3: ( Segm k) c= ( Segm ( len (p | n))) by NAT_1: 39;

        ( dom (p | n)) = (( dom p) /\ n) by RELAT_1: 61;

        then ((p | n) | k) = (p | k) by A3, RELAT_1: 74, XBOOLE_1: 18;

        hence thesis by A1, Th2;

      end;

      ( rng (p | n)) c= ( rng p) & ( rng p) c= { 0 , 1} by A1;

      then ( rng (p | n)) c= { 0 , 1};

      hence thesis by A2;

    end;

    theorem :: CATALAN2:7

    

     Th7: p is dominated_by_0 & q is dominated_by_0 implies (p ^ q) is dominated_by_0

    proof

      assume that

       A1: p is dominated_by_0 and

       A2: q is dominated_by_0;

      ( rng p) c= { 0 , 1} & ( rng q) c= { 0 , 1} by A1, A2;

      then (( rng p) \/ ( rng q)) c= { 0 , 1} by XBOOLE_1: 8;

      hence ( rng (p ^ q)) c= { 0 , 1} by AFINSQ_1: 26;

      let k such that k <= ( dom (p ^ q));

      now

        per cases ;

          suppose

           A3: k <= ( dom p);

          then ((p ^ q) | k) = (p | k) by AFINSQ_1: 58;

          hence thesis by A1, A3;

        end;

          suppose k > ( dom p);

          then

          reconsider kd = (k - ( dom p)) as Nat by NAT_1: 21;

          k = (kd + ( dom p));

          then ((p ^ q) | k) = (p ^ (q | kd)) by AFINSQ_1: 59;

          then

           A4: ( Sum ((p ^ q) | k)) = (( Sum p) + ( Sum (q | kd))) by AFINSQ_2: 55;

          (2 * ( Sum (p | ( len p)))) <= ( len p) & (2 * ( Sum (q | kd))) <= kd by A1, A2, Th2;

          then ((2 * ( Sum p)) + (2 * ( Sum (q | kd)))) <= (( dom p) + kd) by XREAL_1: 7;

          hence thesis by A4;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:8

    

     Th8: p is dominated_by_0 implies (2 * ( Sum (p | ((2 * n) + 1)))) < ((2 * n) + 1)

    proof

      assume p is dominated_by_0;

      then

       A1: (2 * ( Sum (p | ((2 * n) + 1)))) <= ((2 * n) + 1) by Th2;

      assume (2 * ( Sum (p | ((2 * n) + 1)))) >= ((2 * n) + 1);

      then (2 * ( Sum (p | ((2 * n) + 1)))) = ((2 * n) + 1) by A1, XXREAL_0: 1;

      then (2 * (( Sum (p | ((2 * n) + 1))) - n)) = 1;

      hence thesis by INT_1: 9;

    end;

    theorem :: CATALAN2:9

    

     Th9: p is dominated_by_0 & n <= (( len p) - (2 * ( Sum p))) implies (p ^ (n --> 1)) is dominated_by_0

    proof

      set q = (n --> 1);

      assume that

       A1: p is dominated_by_0 and

       A2: n <= (( len p) - (2 * ( Sum p)));

      ( rng q) c= {1} & {1} c= { 0 , 1} by FUNCOP_1: 13, ZFMISC_1: 7;

      then

       A3: ( rng q) c= { 0 , 1};

      ( rng p) c= { 0 , 1} by A1;

      then (( rng p) \/ ( rng q)) c= { 0 , 1} by A3, XBOOLE_1: 8;

      hence ( rng (p ^ q)) c= { 0 , 1} by AFINSQ_1: 26;

      let m such that

       A4: m <= ( dom (p ^ q));

      now

        per cases ;

          suppose m <= ( dom p);

          then ((p ^ q) | m) = (p | m) by AFINSQ_1: 58;

          hence thesis by A1, Th2;

        end;

          suppose m > ( dom p);

          then

          reconsider md = (m - ( dom p)) as Nat by NAT_1: 21;

          

           A5: m = (( dom p) + md);

          ( Sum (md --> 1)) = (md * 1) by AFINSQ_2: 58;

          then

           A6: ( Sum (p ^ (md --> 1))) = (( Sum p) + md) by AFINSQ_2: 55;

          ( dom q) = n & ( len q) = ( dom q);

          then ( dom (p ^ q)) = (( len p) + n) by AFINSQ_1:def 3;

          then (md + ( dom p)) <= (n + ( dom p)) by A4;

          then

           A7: md <= n by XREAL_1: 6;

          then (q | md) = (md --> 1) by Lm1;

          then ((p ^ q) | m) = (p ^ (md --> 1)) by A5, AFINSQ_1: 59;

          then (2 * ( Sum ((p ^ q) | m))) = ((((2 * ( Sum p)) + m) - ( dom p)) + md) by A6;

          then

           A8: (2 * ( Sum ((p ^ q) | m))) <= ((((2 * ( Sum p)) + m) - ( dom p)) + n) by A7, XREAL_1: 6;

          (n - n) <= ((( len p) - (2 * ( Sum p))) - n) by A2, XREAL_1: 9;

          then (m - ((( len p) - (2 * ( Sum p))) - n)) <= (m - 0 ) by XREAL_1: 10;

          hence thesis by A8, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:10

    

     Th10: p is dominated_by_0 & n <= ((k + ( len p)) - (2 * ( Sum p))) implies (((k --> 0 ) ^ p) ^ (n --> 1)) is dominated_by_0

    proof

      assume that

       A1: p is dominated_by_0 and

       A2: n <= ((k + ( len p)) - (2 * ( Sum p)));

      set q = (k --> 0 );

      ( dom q) = k & ( len q) = ( dom q);

      then

       A3: ( len (q ^ p)) = (k + ( len p)) by AFINSQ_1: 17;

      ( Sum q) = (k * 0 ) by AFINSQ_2: 58;

      then

       A4: ( Sum (q ^ p)) = ( 0 qua Nat + ( Sum p)) by AFINSQ_2: 55;

      q is dominated_by_0 by Lm2;

      then (q ^ p) is dominated_by_0 by A1, Th7;

      hence thesis by A2, A3, A4, Th9;

    end;

    theorem :: CATALAN2:11

    

     Th11: p is dominated_by_0 & (2 * ( Sum (p | k))) = k implies k <= ( len p) & ( len (p | k)) = k

    proof

      assume

       A1: p is dominated_by_0 & (2 * ( Sum (p | k))) = k;

      

       A2: k <= ( len p)

      proof

        

         A3: (p | ( len p)) = p;

        assume

         A4: k > ( len p);

        then ( Segm ( len p)) c= ( Segm k) by NAT_1: 39;

        then (p | k) = p by RELAT_1: 68;

        hence thesis by A1, A4, A3;

      end;

      then ( Segm k) c= ( Segm ( len p)) by NAT_1: 39;

      then (( dom p) /\ k) = k by XBOOLE_1: 28;

      hence thesis by A2, RELAT_1: 61;

    end;

    theorem :: CATALAN2:12

    

     Th12: p is dominated_by_0 & (2 * ( Sum (p | k))) = k & p = ((p | k) ^ q) implies q is dominated_by_0

    proof

      assume that

       A1: p is dominated_by_0 and

       A2: (2 * ( Sum (p | k))) = k and

       A3: p = ((p | k) ^ q);

      

       A4: ( len (p | k)) = k by A1, A2, Th11;

      ( rng q) c= ( rng p) & ( rng p) c= { 0 , 1} by A1, A3, AFINSQ_1: 25;

      hence ( rng q) c= { 0 , 1};

      let n such that n <= ( dom q);

      (p | (( len (p | k)) + n)) = ((p | k) ^ (q | n)) by A3, AFINSQ_1: 59;

      then

       A5: ( Sum (p | (( len (p | k)) + n))) = (( Sum (p | k)) + ( Sum (q | n))) by AFINSQ_2: 55;

      (2 * ( Sum (p | (( len (p | k)) + n)))) <= (( len (p | k)) + n) by A1, Th2;

      then (k + (2 * ( Sum (q | n)))) <= (( len (p | k)) + n) by A2, A5;

      hence thesis by A4, XREAL_1: 6;

    end;

    theorem :: CATALAN2:13

    

     Th13: p is dominated_by_0 & (2 * ( Sum (p | k))) = k & k = (n + 1) implies (p | k) = ((p | n) ^ (1 --> 1))

    proof

      assume that

       A1: p is dominated_by_0 and

       A2: (2 * ( Sum (p | k))) = k and

       A3: k = (n + 1);

      reconsider q = (p | k) as XFinSequence of NAT ;

      (q . n) = 1

      proof

        ( Sum (p | k)) <> 0 by A2, A3;

        then

        reconsider s = (( Sum (p | k)) - 1) as Nat by NAT_1: 14, NAT_1: 21;

        

         A4: q is dominated_by_0 by A1, Th6;

        then

         A5: ( rng q) c= { 0 , 1};

        ((2 * s) + 1) = n by A2, A3;

        then

         A6: ( Sum <% 0 %>) = 0 & (2 * ( Sum (q | n))) < n by A4, Th8, AFINSQ_2: 53;

        

         A7: ( len q) = (n + 1) by A1, A2, A3, Th11;

        then

         A8: q = ((q | n) ^ <%(q . n)%>) by AFINSQ_1: 56;

        n < (n + 1) by NAT_1: 13;

        then n in ( Segm (n + 1)) by NAT_1: 44;

        then

         A9: (q . n) in ( rng q) by A7, FUNCT_1: 3;

        assume (q . n) <> 1;

        then (q . n) = 0 by A5, A9, TARSKI:def 2;

        then ( Sum q) = (( Sum (q | n)) + ( Sum <% 0 %>)) by A8, AFINSQ_2: 55;

        hence thesis by A2, A3, A6, NAT_1: 13;

      end;

      then

       A10: ( dom <%(q . n)%>) = 1 & ( rng <%(q . n)%>) = {1} by AFINSQ_1: 33;

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

      then ( Segm n) c= ( Segm k) by A3, NAT_1: 39;

      then

       A11: (q | n) = (p | n) by RELAT_1: 74;

      ( len q) = (n + 1) by A1, A2, A3, Th11;

      then q = ((q | n) ^ <%(q . n)%>) by AFINSQ_1: 56;

      hence thesis by A11, A10, FUNCOP_1: 9;

    end;

    theorem :: CATALAN2:14

    

     Th14: for m, p st m = ( min* { N : (2 * ( Sum (p | N))) = N & N > 0 }) & m > 0 & p is dominated_by_0 holds ex q st (p | m) = (((1 --> 0 ) ^ q) ^ (1 --> 1)) & q is dominated_by_0

    proof

      

       A1: ( dom <% 0 %>) = 1 & ( rng <% 0 %>) = { 0 } by AFINSQ_1: 33;

      set q1 = (1 --> 1);

      set q0 = (1 --> 0 );

      let m, p such that

       A2: m = ( min* { N : (2 * ( Sum (p | N))) = N & N > 0 }) & m > 0 and

       A3: p is dominated_by_0;

      reconsider M = { N : (2 * ( Sum (p | N))) = N & N > 0 } as non empty Subset of NAT by A2, NAT_1:def 1;

      ( min* M) in M by NAT_1:def 1;

      then

      consider n be Nat such that

       A4: n = ( min* M) and

       A5: (2 * ( Sum (p | n))) = n and

       A6: n > 0 ;

      reconsider n1 = (n - 1) as Nat by A6, NAT_1: 20;

      ( Sum (p | n)) <> 0 by A5, A6;

      then n >= (2 * 1) by A5, NAT_1: 14, XREAL_1: 64;

      then

       A7: n1 >= (2 - 1) by XREAL_1: 9;

      then

       A8: ( Segm 1) c= ( Segm n1) by NAT_1: 39;

      then

       A9: ((p | n1) | 1) = (p | 1) by RELAT_1: 74;

      

       A10: n1 < (n1 + 1) by NAT_1: 13;

      n <= ( len p) by A3, A5, Th11;

      then

       A11: n1 < ( len p) by A10, XXREAL_0: 2;

      then 1 < ( len p) by A7, XXREAL_0: 2;

      then ( len (p | 1)) = 1 by AFINSQ_1: 11;

      then

       A12: (p | 1) = <%((p | 1) . 0 )%> by AFINSQ_1: 34;

      (p | 1) is dominated_by_0 by A3, Th6;

      then ((p | 1) . 0 ) = 0 by Th3;

      then

       A13: (p | 1) = (1 --> 0 ) by A12, A1, FUNCOP_1: 9;

      consider q such that

       A14: (p | n1) = (((p | n1) | 1) ^ q) by Th1;

      set qq = ((q0 ^ q) ^ q1);

      take q;

      

       A15: (p | (n1 + 1)) = ((p | n1) ^ (1 --> 1)) by A3, A5, Th13;

      hence (p | m) = qq by A2, A4, A14, A8, A13, RELAT_1: 74;

      ( rng q) c= ( rng (q0 ^ q)) & ( rng (q0 ^ q)) c= ( rng qq) by AFINSQ_1: 24, AFINSQ_1: 25;

      then

       A16: ( rng q) c= ( rng qq);

      (p | m) is dominated_by_0 by A3, Th6;

      then ( rng qq) c= { 0 , 1} by A2, A4, A14, A13, A9, A15;

      hence ( rng q) c= { 0 , 1} by A16;

      

       A17: ( dom q0) = 1;

      ( len (p | n1)) = n1 by A11, AFINSQ_1: 11;

      then

       A18: n1 = (( len q0) + ( len q)) by A14, A13, A9, AFINSQ_1: 17;

      let k;

      assume k <= ( dom q);

      then

       A19: (( len q0) + k) <= n1 by A18, XREAL_1: 6;

      then ( Segm (( len q0) + k)) c= ( Segm n1) by NAT_1: 39;

      then

       A20: ((p | n1) | (1 + k)) = (p | (1 + k)) by RELAT_1: 74;

      

       A21: (1 + k) < n by A15, A19, NAT_1: 13;

      

       A22: (2 * ( Sum (p | (1 + k)))) < (1 + k)

      proof

        assume

         A23: (2 * ( Sum (p | (1 + k)))) >= (1 + k);

        (2 * ( Sum (p | (k + 1)))) <= (k + 1) by A3, Th2;

        then (2 * ( Sum (p | (1 + k)))) = (1 + k) by A23, XXREAL_0: 1;

        then (1 + k) in M;

        hence thesis by A4, A21, NAT_1:def 1;

      end;

      ((p | n1) | (1 + k)) = (q0 ^ (q | k)) by A14, A13, A9, A17, AFINSQ_1: 59;

      then

       A24: ( Sum (p | (1 + k))) = (( Sum q0) + ( Sum (q | k))) by A20, AFINSQ_2: 55;

      ( Sum q0) = ( 0 * 1) by AFINSQ_2: 58;

      hence thesis by A24, A22, NAT_1: 13;

    end;

    theorem :: CATALAN2:15

    

     Th15: for p st ( rng p) c= { 0 , 1} & not p is dominated_by_0 holds ex k st ((2 * k) + 1) = ( min* { N : (2 * ( Sum (p | N))) > N }) & ((2 * k) + 1) <= ( dom p) & k = ( Sum (p | (2 * k))) & (p . (2 * k)) = 1

    proof

      let p such that

       A1: ( rng p) c= { 0 , 1} and

       A2: not p is dominated_by_0;

      set M = { N : (2 * ( Sum (p | N))) > N };

      M c= NAT

      proof

        let x be object;

        assume x in M;

        then ex N st x = N & (2 * ( Sum (p | N))) > N;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider M as Subset of NAT ;

      consider k be Nat such that

       A3: k <= ( dom p) and

       A4: (2 * ( Sum (p | k))) > k by A1, A2;

      reconsider k as Nat;

      k in M by A4;

      then

      reconsider M as non empty Subset of NAT ;

      ( min* M) in M by NAT_1:def 1;

      then

      consider n be Nat such that

       A5: ( min* M) = n and

       A6: (2 * ( Sum (p | n))) > n;

      

       A7: ( Sum (p | 0 )) = 0 ;

      ( Sum (p | n)) > 0 by A6;

      then n > 0 by A7;

      then

      reconsider n1 = (n - 1) as Nat by NAT_1: 20;

      reconsider S = ( Sum (p | n1)) as Nat;

      take S;

      k in M by A4;

      then

       A8: k >= n by A5, NAT_1:def 1;

      then

       A9: ( dom p) >= n by A3, XXREAL_0: 2;

      

       A10: (2 * ( Sum (p | n1))) = n1

      proof

        

         A11: n1 < (n1 + 1) by NAT_1: 13;

        then ( Segm n1) c= ( Segm (n1 + 1)) by NAT_1: 39;

        then

         A12: ((p | n) | n1) = (p | n1) by RELAT_1: 74;

        n = ( len p) & (p | ( dom p)) = p or n < ( len p) by A9, XXREAL_0: 1;

        then

         A13: ( len (p | n)) = (n1 + 1) by AFINSQ_1: 11;

        then n1 in ( Segm ( len (p | n))) by A11, NAT_1: 44;

        then

         A14: ((p | n) . n1) in ( rng (p | n)) by FUNCT_1: 3;

        (p | n) = (((p | n) | n1) ^ <%((p | n) . n1)%>) by A13, AFINSQ_1: 56;

        then ( Sum (p | n)) = (( Sum (p | n1)) + ( Sum <%((p | n) . n1)%>)) by A12, AFINSQ_2: 55;

        then

         A15: ((2 * ( Sum (p | n1))) + (2 * ( Sum <%((p | n) . n1)%>))) >= (n + 1) by A6, NAT_1: 13;

        n1 < (n1 + 1) by NAT_1: 13;

        then not n1 in M by A5, NAT_1:def 1;

        then

         A16: (2 * ( Sum (p | n1))) <= n1;

        ((p | n) . n1) in { 0 , 1} by A1, A14;

        then

         A17: ((p | n) . n1) = 0 or ((p | n) . n1) = 1 by TARSKI:def 2;

        assume (2 * ( Sum (p | n1))) <> n1;

        then ( Sum <%((p | n) . n1)%>) = ((p | n) . n1) & (2 * ( Sum (p | n1))) < n1 by A16, AFINSQ_2: 53, XXREAL_0: 1;

        then ((2 * ( Sum (p | n1))) + (2 * ( Sum <%((p | n) . n1)%>))) < (n1 + 2) by A17, XREAL_1: 8;

        hence contradiction by A15;

      end;

      (p . n1) = 1

      proof

        ( Segm n) c= ( Segm ( len p)) by A9, NAT_1: 39;

        then

         A18: ( dom (p | n)) = (n1 + 1) by RELAT_1: 62;

        

         A19: ( Sum <% 0 %>) = 0 & (p | n) = (((p | n) | n1) ^ <%((p | n) . n1)%>) by A18, AFINSQ_1: 56, AFINSQ_2: 53;

        assume

         A20: (p . n1) <> 1;

        

         A21: n1 < (n1 + 1) by NAT_1: 13;

        then n1 < ( len p) by A9, XXREAL_0: 2;

        then

         A22: n1 in ( dom p) by AFINSQ_1: 86;

        ( Segm n1) c= ( Segm n) by A21, NAT_1: 39;

        then

         A23: ((p | n) | n1) = (p | n1) by RELAT_1: 74;

        n1 in ( Segm n) by A21, NAT_1: 44;

        then n1 in (( dom p) /\ n) by A22, XBOOLE_0:def 4;

        then

         A24: ((p | n) . n1) = (p . n1) by FUNCT_1: 48;

        

         A25: n1 < (n1 + 1) by NAT_1: 13;

        (p . n1) in ( rng p) by A22, FUNCT_1: 3;

        then (p . n1) = 0 by A1, A20, TARSKI:def 2;

        then ( Sum (p | n)) = (( Sum (p | n1)) + 0 qua Nat) by A19, A24, A23, AFINSQ_2: 55;

        hence thesis by A6, A10, A25;

      end;

      hence thesis by A3, A5, A8, A10, XXREAL_0: 2;

    end;

    theorem :: CATALAN2:16

    

     Th16: for p, q, k st (p | ((2 * k) + ( len q))) = (((k --> 0 ) ^ q) ^ (k --> 1)) & q is dominated_by_0 & (2 * ( Sum q)) = ( len q) & k > 0 holds ( min* { N : (2 * ( Sum (p | N))) = N & N > 0 }) = ((2 * k) + ( len q))

    proof

      let p, q, k such that

       A1: (p | ((2 * k) + ( len q))) = (((k --> 0 ) ^ q) ^ (k --> 1)) and

       A2: q is dominated_by_0 and

       A3: (2 * ( Sum q)) = ( len q) and

       A4: k > 0 ;

      set k0 = (k --> 0 );

      

       A5: ( Sum k0) = (k * 0 ) by AFINSQ_2: 58;

      then

       A6: (2 * k) > 0 by A4, XREAL_1: 68;

      reconsider k1 = (k --> 1) as XFinSequence of NAT ;

      set M = { N : (2 * ( Sum (p | N))) = N & N > 0 };

      set kqk = ((k0 ^ q) ^ k1);

      ( Sum kqk) = (( Sum (k0 ^ q)) + ( Sum k1)) by AFINSQ_2: 55;

      then

       A7: ( Sum kqk) = ((( Sum k0) + ( Sum q)) + ( Sum k1)) by AFINSQ_2: 55;

      ( Sum k1) = (k * 1) by AFINSQ_2: 58;

      then (2 * ( Sum (p | ((2 * k) + ( len q))))) = (( len q) + (2 * k)) by A1, A3, A7, A5;

      then

       A8: ((2 * k) + ( len q)) in M by A6;

      M c= NAT

      proof

        let y be object;

        assume y in M;

        then ex i be Nat st i = y & (2 * ( Sum (p | i))) = i & i > 0 ;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider M as non empty Subset of NAT by A8;

      ( min* M) = ((2 * k) + ( len q))

      proof

        kqk = (k0 ^ (q ^ k1)) by AFINSQ_1: 27;

        then

         A9: ( len kqk) = (( len k0) + ( len (q ^ k1))) by AFINSQ_1: 17;

        

         A10: ( len kqk) = (k + (( len q) + ( len k1))) by A9, AFINSQ_1: 17;

        assume

         A11: ( min* M) <> ((2 * k) + ( len q));

        ( min* M) in M by NAT_1:def 1;

        then

         A12: ex i be Nat st i = ( min* M) & (2 * ( Sum (p | i))) = i & i > 0 ;

        

         A14: ((2 * k) + ( len q)) >= ( min* M) by A8, NAT_1:def 1;

        then

         A15: ( Segm ( min* M)) c= ( Segm ((2 * k) + ( len q))) by NAT_1: 39;

        then

         A16: (p | ( min* M)) = (kqk | ( min* M)) by A1, RELAT_1: 74;

        now

          per cases ;

            suppose

             A17: ( min* M) <= k;

            k = ( dom k0) & kqk = (k0 ^ (q ^ k1)) by AFINSQ_1: 27;

            then

             A18: (kqk | ( min* M)) = (k0 | ( min* M)) by A17, AFINSQ_1: 58;

            

             A19: ( Sum (( min* M) --> 0 )) = (( min* M) * 0 ) by AFINSQ_2: 58;

            (k0 | ( min* M)) = (( min* M) --> 0 ) by A17, Lm1;

            then ( Sum (p | ( min* M))) = ( Sum (( min* M) --> 0 )) by A1, A15, A18, RELAT_1: 74;

            hence contradiction by A12, A19;

          end;

            suppose ( min* M) > k;

            then

            reconsider mk = (( min* M) - k) as Nat by NAT_1: 21;

            now

              per cases ;

                suppose

                 A20: ( min* M) <= (k + ( len q));

                

                 A21: ( dom k0) = k;

                ( min* M) = (mk + k);

                then

                 A22: ((k0 ^ q) | ( min* M)) = (k0 ^ (q | mk)) by A21, AFINSQ_1: 59;

                ( dom (k0 ^ q)) = (( len k0) + ( len q)) by AFINSQ_1:def 3;

                then (kqk | ( min* M)) = ((k0 ^ q) | ( min* M)) by A20, AFINSQ_1: 58;

                then

                 A23: ( Sum (p | ( min* M))) = (( Sum k0) + ( Sum (q | mk))) by A16, A22, AFINSQ_2: 55;

                

                 A24: 1 <= k by A4, NAT_1: 14;

                ( Sum k0) = (k * 0 ) by AFINSQ_2: 58;

                then (mk + k) <= mk by A2, A12, A23, Th2;

                hence contradiction by A24, NAT_1: 19;

              end;

                suppose ( min* M) > (k + ( len q));

                then

                reconsider mkL = (( min* M) - (k + ( len q))) as Nat by NAT_1: 21;

                

                 A25: (2 * ( Sum (p | ( min* M)))) = ( min* M) by A12;

                ( dom (k0 ^ q)) = (( len k0) + ( len q)) & ( dom k0) = k by AFINSQ_1:def 3;

                then ( min* M) = (( dom (k0 ^ q)) + mkL);

                then (kqk | ( min* M)) = ((k0 ^ q) ^ (k1 | mkL)) by AFINSQ_1: 59;

                then

                 A26: ( Sum (p | ( min* M))) = (( Sum (k0 ^ q)) + ( Sum (k1 | mkL))) by A16, AFINSQ_2: 55;

                ( min* M) < ( len kqk) by A11, A10, A14, XXREAL_0: 1;

                then mkL < (((2 * k) + ( len q)) - (k + ( len q))) by A10, XREAL_1: 9;

                then (k1 | mkL) = (mkL --> 1) by Lm1;

                then

                 A27: ( Sum (k1 | mkL)) = (mkL * 1) by AFINSQ_2: 58;

                ( Sum (k0 ^ q)) = (( Sum k0) + ( Sum q)) & ( Sum k0) = (k * 0 ) by AFINSQ_2: 55, AFINSQ_2: 58;

                hence contradiction by A3, A11, A26, A27, A25;

              end;

            end;

            hence contradiction;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:17

    

     Th17: for p st p is dominated_by_0 & { N : (2 * ( Sum (p | N))) = N & N > 0 } = {} & ( len p) > 0 holds ex q st p = ( <% 0 %> ^ q) & q is dominated_by_0

    proof

      let p such that

       A1: p is dominated_by_0 and

       A2: { N : (2 * ( Sum (p | N))) = N & N > 0 } = {} & ( len p) > 0 ;

      set M = { N : (2 * ( Sum (p | N))) = N & N > 0 };

      consider q such that

       A3: p = ((p | 1) ^ q) by Th1;

      take q;

      

       A4: ( rng p) c= { 0 , 1} by A1;

      ( rng q) c= ( rng p) by A3, AFINSQ_1: 25;

      then

       A5: ( rng q) c= { 0 , 1} by A4;

      ( len p) >= 1 by A2, NAT_1: 14;

      then ( Segm 1) c= ( Segm ( len p)) by NAT_1: 39;

      then

       A6: ( dom (p | 1)) = 1 by RELAT_1: 62;

      

       A7: (p | 1) = <%((p | 1) . 0 )%> by A6, AFINSQ_1: 34;

       0 in ( Segm 1) by NAT_1: 44;

      then

       A8: ((p | 1) . 0 ) = (p . 0 ) by A6, FUNCT_1: 47;

      hence p = ( <% 0 %> ^ q) by A1, A3, A7, Th3;

      assume not q is dominated_by_0;

      then

      consider i such that i <= ( dom q) and

       A9: (2 * ( Sum (q | i))) > i by A5;

      reconsider i as Nat;

      (p | (1 + i)) = ((p | 1) ^ (q | i)) by A3, A6, AFINSQ_1: 59;

      then

       A10: ( Sum (p | (1 + i))) = (( Sum <%(p . 0 )%>) + ( Sum (q | i))) by A7, A8, AFINSQ_2: 55;

      

       A11: (2 * ( Sum (q | i))) >= (i + 1) by A9, NAT_1: 13;

      ( Sum <%(p . 0 )%>) = (p . 0 ) by AFINSQ_2: 53;

      then

       A12: ( Sum (p | (1 + i))) = ( 0 qua Nat + ( Sum (q | i))) by A1, A10, Th3;

      then (1 + i) >= (2 * ( Sum (q | i))) by A1, Th2;

      then (1 + i) = (2 * ( Sum (q | i))) by A11, XXREAL_0: 1;

      then (1 + i) in M by A12;

      hence thesis by A2;

    end;

    theorem :: CATALAN2:18

    

     Th18: p is dominated_by_0 implies ( <% 0 %> ^ p) is dominated_by_0 & { N : (2 * ( Sum (( <% 0 %> ^ p) | N))) = N & N > 0 } = {}

    proof

      reconsider q = (1 --> 0 ) as XFinSequence of NAT ;

      assume

       A1: p is dominated_by_0;

      ( dom q) = 1 & ( len q) = ( dom q);

      then

       A2: q = <%(q . 0 )%> by AFINSQ_1: 34;

      q is dominated_by_0 by Lm2;

      then q is dominated_by_0 & (q . 0 ) = 0 ;

      hence ( <% 0 %> ^ p) is dominated_by_0 by A1, A2, Th7;

      set M = { N : (2 * ( Sum (( <% 0 %> ^ p) | N))) = N & N > 0 };

      assume M <> {} ;

      then

      consider x be object such that

       A3: x in M by XBOOLE_0:def 1;

      consider i be Nat such that x = i and

       A4: (2 * ( Sum (( <% 0 %> ^ p) | i))) = i and

       A5: i > 0 by A3;

      reconsider i1 = (i - 1) as Nat by A5, NAT_1: 20;

      ( dom <% 0 %>) = 1 by AFINSQ_1: 33;

      then i = (( dom <% 0 %>) + i1);

      then (( <% 0 %> ^ p) | i) = ( <% 0 %> ^ (p | i1)) by AFINSQ_1: 59;

      then

       A6: ( Sum (( <% 0 %> ^ p) | i)) = (( Sum <% 0 %>) + ( Sum (p | i1))) by AFINSQ_2: 55;

      ( Sum <% 0 %>) = 0 & i1 < (i1 + 1) by AFINSQ_2: 53, NAT_1: 13;

      hence thesis by A1, A4, A6, Th2;

    end;

    theorem :: CATALAN2:19

    ( rng p) c= { 0 , 1} & ((2 * k) + 1) = ( min* { N : (2 * ( Sum (p | N))) > N }) implies (p | (2 * k)) is dominated_by_0

    proof

      set M = { N : (2 * ( Sum (p | N))) > N };

      set q = (p | (2 * k));

      assume that

       A1: ( rng p) c= { 0 , 1} and

       A2: ((2 * k) + 1) = ( min* M);

      thus ( rng q) c= { 0 , 1} by A1;

      reconsider M as non empty Subset of NAT by A2, NAT_1:def 1;

      let m;

      assume

       A3: m <= ( dom q);

      then

       A4: ( Segm m) c= ( Segm ( len q)) by NAT_1: 39;

      ( len q) <= (2 * k) by AFINSQ_1: 55;

      then ( Segm ( len q)) c= ( Segm (2 * k)) by NAT_1: 39;

      then ( Segm m) c= ( Segm (2 * k)) by A4;

      then m <= (2 * k) by NAT_1: 39;

      then

       A5: m < ((2 * k) + 1) by NAT_1: 13;

      assume

       A6: (2 * ( Sum (q | m))) > m;

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

      (q | m) = (p | m) & m in NAT by A4, RELAT_1: 74, XBOOLE_1: 1, A3;

      then m in M by A6;

      hence thesis by A2, A5, NAT_1:def 1;

    end;

    begin

    definition

      let n,m be Nat;

      :: CATALAN2:def2

      func Domin_0 (n,m) -> Subset of ( { 0 , 1} ^omega ) means

      : Def2: x in it iff ex p be XFinSequence of NAT st p = x & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m;

      existence

      proof

        defpred Q[ object] means ex p st p = $1 & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m;

        consider X such that

         A1: for x be object holds x in X iff x in ( bool [: NAT , NAT :]) & Q[x] from XBOOLE_0:sch 1;

        X c= ( { 0 , 1} ^omega )

        proof

          let x be object;

          assume x in X;

          then

          consider p such that

           A2: p = x and

           A3: p is dominated_by_0 and ( dom p) = n and ( Sum p) = m by A1;

          ( rng p) c= { 0 , 1} by A3;

          then p is XFinSequence of { 0 , 1} by RELAT_1:def 19;

          hence thesis by A2, AFINSQ_1: 42;

        end;

        then

        reconsider X as Subset of ( { 0 , 1} ^omega );

        take X;

        let x;

        thus x in X implies Q[x] by A1;

        given p such that

         A4: p = x & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m;

        p c= [:( dom p), ( rng p):] & [:( dom p), ( rng p):] c= [: NAT , NAT :] by RELAT_1: 7, ZFMISC_1: 96;

        then p c= [: NAT , NAT :];

        hence thesis by A1, A4;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( { 0 , 1} ^omega ) such that

         A5: x in X1 iff ex p st p = x & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m and

         A6: x in X2 iff ex p st p = x & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m;

        for x be object holds x in X1 iff x in X2

        proof

          let x be object;

          x in X1 iff ex p st p = x & p is dominated_by_0 & ( dom p) = n & ( Sum p) = m by A5;

          hence thesis by A6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: CATALAN2:20

    

     Th20: p in ( Domin_0 (n,m)) iff p is dominated_by_0 & ( dom p) = n & ( Sum p) = m

    proof

      thus p in ( Domin_0 (n,m)) implies p is dominated_by_0 & ( dom p) = n & ( Sum p) = m

      proof

        assume p in ( Domin_0 (n,m));

        then ex q st q = p & q is dominated_by_0 & ( dom q) = n & ( Sum q) = m by Def2;

        hence thesis;

      end;

      thus thesis by Def2;

    end;

    theorem :: CATALAN2:21

    

     Th21: ( Domin_0 (n,m)) c= ( Choose (n,m,1, 0 ))

    proof

      let x be object;

      assume x in ( Domin_0 (n,m));

      then

      consider p such that

       A1: p = x and

       A2: p is dominated_by_0 and

       A3: ( dom p) = n & ( Sum p) = m by Def2;

      ( rng p) c= { 0 , 1} by A2;

      hence thesis by A1, A3, CARD_FIN: 40;

    end;

    registration

      let n, m;

      cluster ( Domin_0 (n,m)) -> finite;

      coherence

      proof

        ( Domin_0 (n,m)) c= ( Choose (n,m,1, 0 )) by Th21;

        hence thesis;

      end;

    end

    theorem :: CATALAN2:22

    

     Th22: ( Domin_0 (n,m)) is empty iff (2 * m) > n

    proof

      thus ( Domin_0 (n,m)) is empty implies (2 * m) > n

      proof

        set q = (m --> 1);

        assume

         A1: ( Domin_0 (n,m)) is empty;

        assume

         A2: (2 * m) <= n;

        m <= (m + m) by NAT_1: 12;

        then

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

        set p = (nm --> 0 );

        ((2 * m) - m) <= nm by A2, XREAL_1: 9;

        then

         A3: (p ^ q) is dominated_by_0 by Th5;

        ( dom (p ^ q)) = (( len p) + ( len q)) & ( dom p) = nm by AFINSQ_1:def 3;

        then

         A4: ( dom (p ^ q)) = (nm + m);

        

         A5: ( Sum (p ^ q)) = (( Sum p) + ( Sum q)) by AFINSQ_2: 55;

        ( Sum p) = ( 0 * nm) & ( Sum q) = (1 * m) by AFINSQ_2: 58;

        hence thesis by A1, A5, A4, A3, Def2;

      end;

      assume

       A6: (2 * m) > n;

      assume ( Domin_0 (n,m)) is non empty;

      then

      consider x be object such that

       A7: x in ( Domin_0 (n,m));

      consider p such that p = x and

       A8: p is dominated_by_0 and

       A9: ( dom p) = n and

       A10: ( Sum p) = m by A7, Def2;

      (p | n) = p by A9;

      hence thesis by A6, A8, A10, Th2;

    end;

    theorem :: CATALAN2:23

    

     Th23: ( Domin_0 (n, 0 )) = {(n --> 0 )}

    proof

      set p = (n --> 0 );

      

       A1: ( Domin_0 (n, 0 )) c= {p}

      proof

        let x be object;

        assume x in ( Domin_0 (n, 0 ));

        then

        consider q such that

         A2: x = q and q is dominated_by_0 and

         A3: ( dom q) = n and

         A4: ( Sum q) = 0 by Def2;

        ( len q) = n & q is nonnegative-yielding by A3;

        then q = (n --> 0 ) or (q = {} & n = 0 ) by A4, AFINSQ_2: 62;

        then q = (n --> 0 );

        hence thesis by A2, TARSKI:def 1;

      end;

       {p} c= ( Domin_0 (n, 0 ))

      proof

        

         A5: p is dominated_by_0 by Lm2;

        ( dom p) = n & ( Sum p) = (n * 0 ) by AFINSQ_2: 58;

        then

         A6: p in ( Domin_0 (n, 0 )) by A5, Def2;

        let x be object;

        assume x in {p};

        hence thesis by A6, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: CATALAN2:24

    

     Th24: ( card ( Domin_0 (n, 0 ))) = 1

    proof

      ( Domin_0 (n, 0 )) = {(n --> 0 )} by Th23;

      hence thesis by CARD_1: 30;

    end;

    theorem :: CATALAN2:25

    

     Th25: for p, n st ( rng p) c= { 0 , n} holds ex q st ( len p) = ( len q) & ( rng q) c= { 0 , n} & (for k st k <= ( len p) holds (( Sum (p | k)) + ( Sum (q | k))) = (n * k)) & for k st k in ( len p) holds (q . k) = (n - (p . k))

    proof

      let p, n such that

       A1: ( rng p) c= { 0 , n};

      reconsider nn = n as Element of NAT by ORDINAL1:def 12;

      defpred P[ set, set] means for k st k = $1 holds $2 = (n - (p . k));

      

       A2: for k st k in ( Segm ( len p)) holds ex x be Element of { 0 , n} st P[k, x]

      proof

        let k;

        assume k in ( Segm ( len p));

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

        then (p . k) = 0 or (p . k) = n by A1, TARSKI:def 2;

        then

         A3: (n - (p . k)) in { 0 , n} by TARSKI:def 2;

         P[k, (n - (p . k))];

        hence thesis by A3;

      end;

      consider q be XFinSequence of { 0 , n} such that

       A4: ( dom q) = ( Segm ( len p)) & for k st k in ( Segm ( len p)) holds P[k, (q . k)] from STIRL2_1:sch 5( A2);

      ( rng q) c= { 0 , nn};

      then ( rng q) c= NAT by XBOOLE_1: 1;

      then

      reconsider q as XFinSequence of NAT by RELAT_1:def 19;

      defpred Q[ Nat] means $1 <= ( len p) implies (( Sum (p | $1)) + ( Sum (q | $1))) = (n * $1);

      

       A5: for k st Q[k] holds Q[(k + 1)]

      proof

        let k such that

         A6: Q[k];

        set k1 = (k + 1);

        

         A7: k < (k + 1) by NAT_1: 13;

        then

         A8: ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

        then

         A9: ((p | k1) | k) = (p | k) by RELAT_1: 74;

        

         A10: ((q | k1) | k) = (q | k) by A8, RELAT_1: 74;

        assume

         A11: (k + 1) <= ( len p);

        then

         A12: ( Segm k1) c= ( Segm ( len p)) by NAT_1: 39;

        then

         A13: ( len (q | k1)) = k1 by A4, RELAT_1: 62;

        then

         A14: (q | k1) = (((q | k1) | k) ^ <%((q | k1) . k)%>) by AFINSQ_1: 56;

        ( len (p | k1)) = k1 by A12, RELAT_1: 62;

        then

         A15: k in ( dom (p | k1)) by A7, AFINSQ_1: 86;

        then

         A16: ((p | k1) . k) = (p . k) by FUNCT_1: 47;

        ( len (p | k1)) = k1 by A12, RELAT_1: 62;

        then (p | k1) = (((p | k1) | k) ^ <%((p | k1) . k)%>) by AFINSQ_1: 56;

        then ( Sum (p | k1)) = (( Sum (p | k)) + ( Sum <%(p . k)%>)) by A16, A9, AFINSQ_2: 55;

        then

         A17: ( Sum (p | k1)) = (( Sum (p | k)) + (p . k)) by AFINSQ_2: 53;

        k < ( len p) by A11, NAT_1: 13;

        then k in ( len p) by AFINSQ_1: 86;

        then

         A18: (q . k) = (n - (p . k)) by A4;

        ((q | k1) . k) = (q . k) by A13, A15, FUNCT_1: 47;

        then ( Sum (q | k1)) = (( Sum (q | k)) + ( Sum <%(q . k)%>)) by A14, A10, AFINSQ_2: 55;

        then ( Sum (q | k1)) = (( Sum (q | k)) + (n - (p . k))) by A18, AFINSQ_2: 53;

        hence thesis by A6, A11, A17, NAT_1: 13;

      end;

      take q;

      thus ( len p) = ( len q) by A4;

      thus ( rng q) c= { 0 , n} by RELAT_1:def 19;

      

       A19: Q[ 0 ];

      for k holds Q[k] from NAT_1:sch 2( A19, A5);

      hence thesis by A4;

    end;

    theorem :: CATALAN2:26

    

     Th26: m <= n implies (n choose m) > 0

    proof

      assume

       A1: m <= n;

      then

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

      

       A2: ((m ! ) * (nm ! )) > ((m ! ) * 0 ) by XREAL_1: 68;

      (n ! ) > ( 0 * ((m ! ) * (nm ! )));

      then ((n ! ) / ((m ! ) * (nm ! ))) > 0 by A2, XREAL_1: 81;

      hence thesis by A1, NEWTON:def 3;

    end;

    theorem :: CATALAN2:27

    

     Th27: (2 * (m + 1)) <= n implies ( card (( Choose (n,(m + 1),1, 0 )) \ ( Domin_0 (n,(m + 1))))) = ( card ( Choose (n,m,1, 0 )))

    proof

      defpred P[ object, object] means for p, k st $1 = p & ((2 * k) + 1) = ( min* { N : (2 * ( Sum (p | N))) > N }) holds ex r1,r2 be XFinSequence of NAT st $2 = (r1 ^ r2) & ( len r1) = ((2 * k) + 1) & ( len r1) = ( len (p | ((2 * k) + 1))) & p = ((p | ((2 * k) + 1)) ^ r2) & (for o be Nat st o < ((2 * k) + 1) holds (r1 . o) = (1 - (p . o)));

      assume

       A1: (2 * (m + 1)) <= n;

      

       A2: m <= (m + m) by XREAL_1: 31;

      m <= (m + 1) by NAT_1: 13;

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

      then (2 * m) <= n by A1, XXREAL_0: 2;

      then m <= n by A2, XXREAL_0: 2;

      then (( card n) choose m) > 0 by Th26;

      then

      reconsider W = ( Choose (n,m,1, 0 )) as non empty finite set by CARD_1: 27, CARD_FIN: 16;

      set Z = ( Domin_0 (n,(m + 1)));

      set CH = ( Choose (n,(m + 1),1, 0 ));

      

       A3: for x be object st x in (CH \ Z) holds ex y be object st y in W & P[x, y]

      proof

        let x be object such that

         A4: x in (CH \ Z);

        x in CH by A4, XBOOLE_0:def 5;

        then

        consider p be XFinSequence of NAT such that

         A5: p = x and

         A6: ( dom p) = n and

         A7: ( rng p) c= { 0 , 1} and

         A8: ( Sum p) = (m + 1) by CARD_FIN: 40;

         not p in Z by A4, A5, XBOOLE_0:def 5;

        then not p is dominated_by_0 by A6, A8, Def2;

        then

        consider o be Nat such that

         A9: ((2 * o) + 1) = ( min* { N : (2 * ( Sum (p | N))) > N }) & ((2 * o) + 1) <= ( dom p) & o = ( Sum (p | (2 * o))) & (p . (2 * o)) = 1 by A7, Th15;

        set q = (p | ((2 * o) + 1));

        consider r2 be XFinSequence of NAT such that

         A10: p = (q ^ r2) by Th1;

        ( rng q) c= { 0 , 1} by A7;

        then

        consider r1 be XFinSequence of NAT such that

         A11: ( len q) = ( len r1) and

         A12: ( rng r1) c= { 0 , 1} and

         A13: for i st i <= ( len q) holds (( Sum (q | i)) + ( Sum (r1 | i))) = (1 * i) and

         A14: for i st i in ( len q) holds (r1 . i) = (1 - (q . i)) by Th25;

        take R = (r1 ^ r2);

        ( len p) = (( len r1) + ( len r2)) by A11, A10, AFINSQ_1: 17;

        then

         A15: ( dom R) = n by A6, AFINSQ_1:def 3;

        ( rng r2) c= ( rng p) by A10, AFINSQ_1: 25;

        then ( rng r2) c= { 0 , 1} by A7;

        then (( rng r1) \/ ( rng r2)) c= { 0 , 1} by A12, XBOOLE_1: 8;

        then

         A16: ( rng R) c= { 0 , 1} by AFINSQ_1: 26;

        (q | ( dom q)) = q & (r1 | ( dom r1)) = r1;

        then

         A17: (( Sum q) + ( Sum r1)) = (1 * ( len q)) by A11, A13;

        

         A18: (2 * o) < ((2 * o) + 1) by NAT_1: 13;

        then ( Segm (2 * o)) c= ( Segm ((2 * o) + 1)) by NAT_1: 39;

        then

         A19: (q | (2 * o)) = (p | (2 * o)) by RELAT_1: 74;

        

         A20: ( Segm ((2 * o) + 1)) c= ( Segm ( len p)) by A9, NAT_1: 39;

        then

         A21: ( dom q) = ((2 * o) + 1) by RELAT_1: 62;

        

         A22: ( len q) = ((2 * o) + 1) by A20, RELAT_1: 62;

        then

         A23: q = ((q | (2 * o)) ^ <%(q . (2 * o))%>) by AFINSQ_1: 56;

        (2 * o) in ( Segm ((2 * o) + 1)) by A18, NAT_1: 44;

        then (q . (2 * o)) = (p . (2 * o)) by A22, FUNCT_1: 47;

        then ( Sum q) = (( Sum (p | (2 * o))) + ( Sum <%(p . (2 * o))%>)) by A23, A19, AFINSQ_2: 55;

        then

         A24: ( Sum q) = (o + 1) by A9, AFINSQ_2: 53;

        (m + 1) = (( Sum q) + ( Sum r2)) by A8, A10, AFINSQ_2: 55;

        then (( Sum r1) + ( Sum r2)) = (((m + 1) - ((2 * o) + 1)) + (2 * o)) by A17, A21, A24;

        then ( Sum (r1 ^ r2)) = m by AFINSQ_2: 55;

        hence R in W by A15, A16, CARD_FIN: 40;

        thus P[x, R]

        proof

          let p9 be XFinSequence of NAT , k such that

           A25: x = p9 & ((2 * k) + 1) = ( min* { N : (2 * ( Sum (p9 | N))) > N });

          set q9 = (p9 | ((2 * k) + 1));

          take r1, r2;

          thus R = (r1 ^ r2) & ( len r1) = ((2 * k) + 1) & ( len r1) = ( len q9) & p9 = (q9 ^ r2) by A5, A9, A11, A10, A20, A25, RELAT_1: 62;

          thus for i be Nat st i < ((2 * k) + 1) holds (r1 . i) = (1 - (p9 . i))

          proof

            let i be Nat;

            assume i < ((2 * k) + 1);

            then

             A26: i in ( len q) by A5, A9, A21, A25, AFINSQ_1: 86;

            then (r1 . i) = (1 - (q . i)) by A14;

            hence thesis by A5, A25, A26, FUNCT_1: 47;

          end;

        end;

      end;

      consider F be Function of (CH \ Z), W such that

       A27: for x be object st x in (CH \ Z) holds P[x, (F . x)] from FUNCT_2:sch 1( A3);

      W c= ( rng F)

      proof

        let x be object;

        assume x in W;

        then

        consider p such that

         A28: p = x and

         A29: ( dom p) = n and

         A30: ( rng p) c= { 0 , 1} and

         A31: ( Sum p) = m by CARD_FIN: 40;

        set M = { N : (2 * ( Sum (p | N))) < N };

        m < (m + 1) by NAT_1: 13;

        then (2 * m) < (2 * (m + 1)) by XREAL_1: 68;

        then (2 * m) < n by A1, XXREAL_0: 2;

        then (2 * ( Sum (p | n))) < n & n in NAT by A29, A31, ORDINAL1:def 12;

        then

         A32: n in M;

        M c= NAT

        proof

          let y be object;

          assume y in M;

          then ex i be Nat st i = y & (2 * ( Sum (p | i))) < i;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider M as non empty Subset of NAT by A32;

        ex k st ((2 * k) + 1) = ( min* M) & ( Sum (p | ((2 * k) + 1))) = k & ((2 * k) + 1) <= ( dom p)

        proof

          set mm = ( min* M);

          mm in M by NAT_1:def 1;

          then

           A33: ex o be Nat st mm = o & (2 * ( Sum (p | o))) < o;

          then

          reconsider m1 = (mm - 1) as Nat by NAT_1: 20;

          

           A34: (2 * ( Sum (p | mm))) < (m1 + 1) by A33;

          

           A35: m1 < (m1 + 1) by NAT_1: 13;

          then ( Segm m1) c= ( Segm mm) by NAT_1: 39;

          then

           A36: ((p | mm) | m1) = (p | m1) by RELAT_1: 74;

          mm <= ( dom p) by A29, A32, NAT_1:def 1;

          then

           A37: ( Segm mm) c= ( Segm ( len p)) by NAT_1: 39;

          then ( dom (p | mm)) = mm by RELAT_1: 62;

          then m1 in ( Segm ( dom (p | mm))) by A35, NAT_1: 44;

          then

           A38: ((p | mm) . m1) = (p . m1) by FUNCT_1: 47;

          m1 < (m1 + 1) by NAT_1: 13;

          then not m1 in M by NAT_1:def 1;

          then (2 * ( Sum (p | m1))) >= m1;

          then

           A39: ( Sum <%(p . m1)%>) = (p . m1) & ((2 * ( Sum (p | m1))) + (2 * (p . m1))) >= (m1 + 0 qua Nat) by AFINSQ_2: 53, XREAL_1: 7;

          reconsider S = ( Sum (p | mm)) as Nat;

          take S;

          

           A40: mm <= ( dom p) by A29, A32, NAT_1:def 1;

          ( len (p | mm)) = (m1 + 1) by A37, RELAT_1: 62;

          then (p | mm) = (((p | mm) | m1) ^ <%((p | mm) . m1)%>) by AFINSQ_1: 56;

          then ( Sum (p | mm)) = (( Sum (p | m1)) + ( Sum <%(p . m1)%>)) by A38, A36, AFINSQ_2: 55;

          hence thesis by A40, A39, A34, NAT_1: 9;

        end;

        then

        consider k such that

         A41: ((2 * k) + 1) = ( min* M) and

         A42: ( Sum (p | ((2 * k) + 1))) = k and

         A43: ((2 * k) + 1) <= ( dom p);

        set k1 = ((2 * k) + 1);

        consider q such that

         A44: p = ((p | k1) ^ q) by Th1;

        ( rng (p | k1)) c= { 0 , 1} by A30;

        then

        consider r be XFinSequence of NAT such that

         A45: ( len r) = ( len (p | k1)) and

         A46: ( rng r) c= { 0 , 1} and

         A47: for i st i <= ( len (p | k1)) holds (( Sum ((p | k1) | i)) + ( Sum (r | i))) = (1 * i) and

         A48: for i st i in ( len (p | k1)) holds (r . i) = (1 - ((p | k1) . i)) by Th25;

        set rq = (r ^ q);

        

         A49: ( dom rq) = (( len (p | k1)) + ( len q)) by A45, AFINSQ_1:def 3;

        

         A50: m = (k + ( Sum q)) by A31, A42, A44, AFINSQ_2: 55;

        ( dom rq) = (( len (p | k1)) + ( len q)) by A45, AFINSQ_1:def 3;

        then

         A51: ( dom rq) = ( dom p) by A44, AFINSQ_1:def 3;

        ((p | k1) | ( dom (p | k1))) = (p | k1) & (r | ( dom r)) = r;

        then

         A52: (( Sum (p | k1)) + ( Sum r)) = (1 * ( len (p | k1))) by A45, A47;

        ( rng q) c= ( rng p) by A44, AFINSQ_1: 25;

        then ( rng q) c= { 0 , 1} by A30;

        then (( rng r) \/ ( rng q)) c= { 0 , 1} by A46, XBOOLE_1: 8;

        then

         A53: ( rng rq) c= { 0 , 1} by AFINSQ_1: 26;

        

         A54: ( Segm k1) c= ( Segm ( len p)) by A43, NAT_1: 39;

        then

         A55: ( len (p | k1)) = k1 by RELAT_1: 62;

        then

         A56: ((r ^ q) | k1) = r by A45, AFINSQ_1: 57;

        

         A57: (k1 + 1) > k1 by NAT_1: 13;

        then

         A58: k1 < (2 * ( Sum r)) by A42, A52, A55;

        

         A59: (2 * ( Sum r)) > k1 by A42, A52, A55, A57;

        then

        consider j be Nat such that

         A60: ((2 * j) + 1) = ( min* { N : (2 * ( Sum (rq | N))) > N }) & ((2 * j) + 1) <= ( dom rq) & j = ( Sum (rq | (2 * j))) & (rq . (2 * j)) = 1 by A53, A56, Th2, Th15;

        set j1 = ((2 * j) + 1);

        

         A61: ( len ((p | k1) ^ q)) = (( len (p | k1)) + ( len q)) by AFINSQ_1:def 3;

         not rq is dominated_by_0 by A59, A56, Th2;

        then

         A62: not rq in Z by Th20;

        set rqj = (rq | ((2 * j) + 1));

        ( Sum rq) = (( Sum r) + ( Sum q)) by AFINSQ_2: 55;

        then rq in CH by A29, A42, A52, A55, A51, A53, A50, CARD_FIN: 40;

        then

         A63: rq in (CH \ Z) by A62, XBOOLE_0:def 5;

        then

        consider r1,r2 be XFinSequence of NAT such that

         A64: (F . rq) = (r1 ^ r2) and

         A65: ( len r1) = j1 and

         A66: ( len r1) = ( len rqj) & rq = (rqj ^ r2) and

         A67: for i be Nat st i < j1 holds (r1 . i) = (1 - (rq . i)) by A27, A60;

        

         A68: ( dom rq) = (( len r1) + ( len r2)) by A66, AFINSQ_1:def 3;

        then

         A69: ( len (r1 ^ r2)) = ( len ((p | k1) ^ q)) by A49, A61, AFINSQ_1: 17;

        reconsider K = { N : (2 * ( Sum (rq | N))) > N } as non empty Subset of NAT by A60, NAT_1:def 1;

        (rq | k1) = r by A45, A55, AFINSQ_1: 57;

        then k1 in K by A58;

        then

         A70: k1 >= j1 by A60, NAT_1:def 1;

        then ( Segm j1) c= ( Segm k1) by NAT_1: 39;

        then

         A71: ((p | k1) | j1) = (p | j1) by RELAT_1: 74;

        j1 in K by A60, NAT_1:def 1;

        then

         A72: ex N st N = j1 & (2 * ( Sum (rq | N))) > N;

        (( Sum ((p | k1) | j1)) + ( Sum (r | j1))) = (j1 * 1) by A47, A55, A70;

        then (2 * ( Sum (r | j1))) = ((2 * j1) - (2 * ( Sum (p | j1)))) by A71;

        then (j1 + (j1 - (2 * ( Sum (p | j1))))) > ((2 * ( Sum (p | j1))) + (j1 - (2 * ( Sum (p | j1))))) by A45, A55, A70, A72, AFINSQ_1: 58;

        then j1 > (2 * ( Sum (p | j1))) by XREAL_1: 6;

        then j1 in M;

        then j1 >= k1 by A41, NAT_1:def 1;

        then

         A73: j1 = k1 by A70, XXREAL_0: 1;

        

         A74: ( len ((p | k1) ^ q)) = ( len rq) by A49, AFINSQ_1:def 3;

        now

          let i be Nat such that

           A75: i < ( len (r1 ^ r2));

          now

            per cases ;

              suppose

               A76: i < ( len r1);

              then

               A77: i in ( dom r1) & (r1 . i) = (1 - (rq . i)) by A65, A67, AFINSQ_1: 86;

              

               A78: i in ( len r1) by A76, AFINSQ_1: 86;

              

               A79: ( len r1) = ( len (p | k1)) & i in NAT by A54, A65, A73, ORDINAL1:def 12, RELAT_1: 62;

              then

               A80: (r . i) = (1 - ((p | k1) . i)) by A48, A78;

              (((p | k1) ^ q) . i) = ((p | k1) . i) & (rq . i) = (r . i) by A45, A78, A79, AFINSQ_1:def 3;

              hence ((r1 ^ r2) . i) = (((p | k1) ^ q) . i) by A80, A77, AFINSQ_1:def 3;

            end;

              suppose

               A81: i >= ( len r1);

              then

               A82: (((p | k1) ^ q) . i) = (q . (i - ( len r))) by A45, A55, A65, A73, A69, A75, AFINSQ_1: 19;

              ((r1 ^ r2) . i) = (r2 . (i - ( len r1))) & (rq . i) = (q . (i - ( len r))) by A45, A55, A65, A73, A69, A74, A75, A81, AFINSQ_1: 19;

              hence ((r1 ^ r2) . i) = (((p | k1) ^ q) . i) by A66, A69, A74, A75, A81, A82, AFINSQ_1: 19;

            end;

          end;

          hence ((r1 ^ r2) . i) = (((p | k1) ^ q) . i);

        end;

        then

         A83: (r1 ^ r2) = ((p | k1) ^ q) by A68, A49, A61, AFINSQ_1: 9, AFINSQ_1: 17;

        rq in ( dom F) by A63, FUNCT_2:def 1;

        hence thesis by A28, A44, A64, A83, FUNCT_1: 3;

      end;

      then

       A84: ( rng F) = W;

      

       A85: F is one-to-one

      proof

        let x,y be object such that

         A86: x in ( dom F) and

         A87: y in ( dom F) and

         A88: (F . x) = (F . y);

        x in CH by A86, XBOOLE_0:def 5;

        then

        consider p such that

         A89: p = x and

         A90: ( dom p) = n and

         A91: ( rng p) c= { 0 , 1} and

         A92: ( Sum p) = (m + 1) by CARD_FIN: 40;

         not p in Z by A86, A89, XBOOLE_0:def 5;

        then not p is dominated_by_0 by A90, A92, Def2;

        then

        consider k1 be Nat such that

         A93: ((2 * k1) + 1) = ( min* { N : (2 * ( Sum (p | N))) > N }) & ((2 * k1) + 1) <= ( dom p) & k1 = ( Sum (p | (2 * k1))) & (p . (2 * k1)) = 1 by A91, Th15;

        y in CH by A87, XBOOLE_0:def 5;

        then

        consider q such that

         A94: q = y and

         A95: ( dom q) = n and

         A96: ( rng q) c= { 0 , 1} and

         A97: ( Sum q) = (m + 1) by CARD_FIN: 40;

         not q in Z by A87, A94, XBOOLE_0:def 5;

        then not q is dominated_by_0 by A95, A97, Def2;

        then

        consider k2 be Nat such that

         A98: ((2 * k2) + 1) = ( min* { N : (2 * ( Sum (q | N))) > N }) & ((2 * k2) + 1) <= ( dom q) & k2 = ( Sum (q | (2 * k2))) & (q . (2 * k2)) = 1 by A96, Th15;

        

         A99: ( len q) = n by A95;

        reconsider M = { N : (2 * ( Sum (q | N))) > N } as non empty Subset of NAT by A98, NAT_1:def 1;

        set qk = (q | ((2 * k2) + 1));

        consider s1,s2 be XFinSequence of NAT such that

         A100: (F . y) = (s1 ^ s2) and

         A101: ( len s1) = ((2 * k2) + 1) and

         A102: ( len s1) = ( len qk) and

         A103: q = (qk ^ s2) and

         A104: for i be Nat st i < ((2 * k2) + 1) holds (s1 . i) = (1 - (q . i)) by A27, A87, A94, A98;

        

         A105: ( len q) = (( len qk) + ( len s2)) by A103, AFINSQ_1: 17;

        then

         A106: ( len q) = ( len (s1 ^ s2)) by A102, AFINSQ_1: 17;

        reconsider K = { N : (2 * ( Sum (p | N))) > N } as non empty Subset of NAT by A93, NAT_1:def 1;

        set pk = (p | ((2 * k1) + 1));

        consider r1,r2 be XFinSequence of NAT such that

         A107: (F . x) = (r1 ^ r2) and

         A108: ( len r1) = ((2 * k1) + 1) and

         A109: ( len r1) = ( len (p | ((2 * k1) + 1))) and

         A110: p = ((p | ((2 * k1) + 1)) ^ r2) and

         A111: for i be Nat st i < ((2 * k1) + 1) holds (r1 . i) = (1 - (p . i)) by A27, A86, A89, A93;

        assume x <> y;

        then

        consider i be Nat such that

         A112: i < ( len p) and

         A113: (p . i) <> (q . i) by A89, A90, A94, A95, AFINSQ_1: 9;

        

         A114: ( len p) = (( len pk) + ( len r2)) by A110, AFINSQ_1: 17;

        then

         A115: ( len p) = ( len (r1 ^ r2)) by A109, AFINSQ_1: 17;

        now

          per cases by XXREAL_0: 1;

            suppose

             A116: k1 = k2;

            now

              per cases ;

                suppose

                 A117: i < ( len pk);

                then i in ( len pk) by AFINSQ_1: 86;

                then

                 A118: (r1 . i) = ((r1 ^ r2) . i) & (s1 . i) = ((s1 ^ s2) . i) by A108, A109, A101, A116, AFINSQ_1:def 3;

                (r1 . i) = (1 - (p . i)) & (s1 . i) = (1 - (q . i)) by A108, A109, A111, A104, A116, A117;

                hence contradiction by A88, A107, A100, A113, A118;

              end;

                suppose

                 A119: i >= ( len pk);

                then

                 A120: ((s1 ^ s2) . i) = (s2 . (i - ( len pk))) by A90, A108, A109, A95, A101, A106, A112, A116, AFINSQ_1: 19;

                (p . i) = (r2 . (i - ( len pk))) & (q . i) = (s2 . (i - ( len pk))) by A90, A108, A109, A110, A101, A102, A103, A99, A112, A116, A119, AFINSQ_1: 19;

                hence contradiction by A88, A107, A109, A100, A115, A112, A113, A119, A120, AFINSQ_1: 19;

              end;

            end;

            hence contradiction;

          end;

            suppose

             A121: k1 > k2;

            ( len s1) <= ( len p) by A90, A95, A102, A105, NAT_1: 11;

            then

             A122: ( Segm ( len s1)) c= ( Segm ( len p)) by NAT_1: 39;

            (2 * k2) < (2 * k1) by A121, XREAL_1: 68;

            then

             A123: ( len s1) < ( len r1) by A108, A101, XREAL_1: 6;

            then ((s1 ^ s2) | ( len s1)) = (r1 | ( len s1)) by A88, A107, A100, AFINSQ_1: 58;

            then

             A124: s1 = (r1 | ( len s1)) by AFINSQ_1: 57;

            

             A125: for k be Nat st k < ( len qk) holds (qk . k) = ((p | ( len qk)) . k)

            proof

              let k be Nat such that

               A126: k < ( len qk);

              

               A127: k in ( len s1) by A102, A126, AFINSQ_1: 86;

              then

               A128: k in (( dom q) /\ ( len s1)) by A90, A95, A122, XBOOLE_0:def 4;

              k in (( dom p) /\ ( len s1)) by A122, A127, XBOOLE_0:def 4;

              then

               A129: (p . k) = ((p | ( len qk)) . k) by A102, FUNCT_1: 48;

              

               A130: k < ( len r1) by A102, A123, A126, XXREAL_0: 2;

              then

               A131: (r1 . k) = (1 - (p . k)) by A108, A111;

              k in ( dom r1) by A130, AFINSQ_1: 86;

              then k in (( dom r1) /\ ( len s1)) by A127, XBOOLE_0:def 4;

              then

               A132: (r1 . k) = ((r1 | ( len s1)) . k) by FUNCT_1: 48;

              (s1 . k) = (1 - (q . k)) by A101, A102, A104, A126;

              hence thesis by A101, A124, A131, A132, A128, A129, FUNCT_1: 48;

            end;

            ((2 * k2) + 1) in M by A98, NAT_1:def 1;

            then

             A133: ex N st ((2 * k2) + 1) = N & (2 * ( Sum (q | N))) > N;

            ( len qk) = ( len (p | ( len qk))) by A102, A122, RELAT_1: 62;

            then qk = (p | ( len qk)) by A125, AFINSQ_1: 9;

            then ( len qk) in K by A101, A102, A133;

            hence contradiction by A93, A108, A102, A123, NAT_1:def 1;

          end;

            suppose

             A134: k1 < k2;

            ( len r1) <= ( len q) by A90, A109, A95, A114, NAT_1: 11;

            then

             A135: ( Segm ( len r1)) c= ( Segm ( len q)) by NAT_1: 39;

            (2 * k1) < (2 * k2) by A134, XREAL_1: 68;

            then

             A136: ( len r1) < ( len s1) by A108, A101, XREAL_1: 6;

            then ((r1 ^ r2) | ( len r1)) = (s1 | ( len r1)) by A88, A107, A100, AFINSQ_1: 58;

            then

             A137: r1 = (s1 | ( len r1)) by AFINSQ_1: 57;

            

             A138: for k be Nat st k < ( len pk) holds (pk . k) = ((q | ( len pk)) . k)

            proof

              let k be Nat such that

               A139: k < ( len pk);

              

               A140: k in ( len r1) by A109, A139, AFINSQ_1: 86;

              then

               A141: k in (( dom p) /\ ( len r1)) by A90, A95, A135, XBOOLE_0:def 4;

              k in (( dom q) /\ ( len r1)) by A135, A140, XBOOLE_0:def 4;

              then

               A142: (q . k) = ((q | ( len pk)) . k) by A109, FUNCT_1: 48;

              

               A143: k < ( len s1) by A109, A136, A139, XXREAL_0: 2;

              then

               A144: (s1 . k) = (1 - (q . k)) by A101, A104;

              k in ( dom s1) by A143, AFINSQ_1: 86;

              then k in (( dom s1) /\ ( len r1)) by A140, XBOOLE_0:def 4;

              then

               A145: (s1 . k) = ((s1 | ( len r1)) . k) by FUNCT_1: 48;

              (r1 . k) = (1 - (p . k)) by A108, A109, A111, A139;

              hence thesis by A108, A137, A144, A145, A141, A142, FUNCT_1: 48;

            end;

            ((2 * k1) + 1) in K by A93, NAT_1:def 1;

            then

             A146: ex N st ((2 * k1) + 1) = N & (2 * ( Sum (p | N))) > N;

            ( len pk) = ( len (q | ( len pk))) by A109, A135, RELAT_1: 62;

            then pk = (q | ( len pk)) by A138, AFINSQ_1: 9;

            then ( len pk) in M by A108, A109, A146;

            hence contradiction by A109, A98, A101, A136, NAT_1:def 1;

          end;

        end;

        hence contradiction;

      end;

      ( dom F) = (CH \ Z) by FUNCT_2:def 1;

      then ((CH \ Z),W) are_equipotent by A85, A84, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CATALAN2:28

    

     Th28: (2 * (m + 1)) <= n implies ( card ( Domin_0 (n,(m + 1)))) = ((n choose (m + 1)) - (n choose m))

    proof

      set CH = ( Choose (n,(m + 1),1, 0 ));

      set Z = ( Domin_0 (n,(m + 1)));

      set W = ( Choose (n,m,1, 0 ));

      

       A1: ( card CH) = (( card n) choose (m + 1)) & ( card n) = n by CARD_FIN: 16;

      ( card (CH \ Z)) = (( card CH) - ( card Z)) by Th21, CARD_2: 44;

      then

       A2: ( card Z) = (( card CH) - ( card (CH \ Z)));

      assume (2 * (m + 1)) <= n;

      then ( card Z) = (( card CH) - ( card W)) by A2, Th27;

      hence thesis by A1, CARD_FIN: 16;

    end;

    theorem :: CATALAN2:29

    

     Th29: (2 * m) <= n implies ( card ( Domin_0 (n,m))) = ((((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m))

    proof

      assume

       A1: (2 * m) <= n;

      now

        per cases ;

          suppose

           A2: m = 0 ;

          then (n choose m) = 1 by NEWTON: 19;

          then ((((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)) = 1 by A2, XCMPLX_1: 60;

          hence thesis by A2, Th24;

        end;

          suppose

           A3: m > 0 ;

          

           A4: m <= (m + m) by NAT_1: 11;

          then

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

          reconsider m1 = (m - 1) as Nat by A3, NAT_1: 20;

          set n9 = (n ! );

          set m9 = (m ! );

          set nm19 = ((nm + 1) ! );

          set nm9 = (nm ! );

          m <= n by A1, A4, XXREAL_0: 2;

          then

           A5: (n choose m) = (n9 / (m9 * nm9)) by NEWTON:def 3;

          

           A6: (2 * (m1 + 1)) <= n by A1;

          set m19 = (m1 ! );

          

           A7: (1 / (m19 * nm19)) = (((m1 + 1) * 1) / ((m19 * nm19) * (m1 + 1))) by XCMPLX_1: 91

          .= (m / (nm19 * (m19 * (m1 + 1))))

          .= (m / (nm19 * ((m1 + 1) ! ))) by NEWTON: 15

          .= ( - (( - m) / (nm19 * m9))) by XCMPLX_1: 190;

          (1 / (m9 * nm9)) = (((nm + 1) * 1) / ((m9 * nm9) * (nm + 1))) by XCMPLX_1: 91

          .= ((nm + 1) / (m9 * (nm9 * (nm + 1))))

          .= ((nm + 1) / (m9 * nm19)) by NEWTON: 15;

          

          then

           A8: ((1 / (m9 * nm9)) - (1 / (m19 * nm19))) = (((nm + 1) / (m9 * nm19)) + (( - m) / (m9 * nm19))) by A7

          .= (((nm + 1) + ( - m)) / (m9 * nm19)) by XCMPLX_1: 62

          .= (((n + 1) - (2 * m)) / (m9 * (nm9 * (nm + 1)))) by NEWTON: 15

          .= ((1 * ((n + 1) - (2 * m))) / ((m9 * nm9) * (nm + 1)))

          .= ((1 / (m9 * nm9)) * (((n + 1) - (2 * m)) / (nm + 1))) by XCMPLX_1: 76;

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

          then

           A9: m1 <= n by A1, XXREAL_0: 2;

          (n - m1) = (nm + 1);

          then

           A10: (n choose m1) = (n9 / (m19 * nm19)) by A9, NEWTON:def 3;

          ((n9 / (m9 * nm9)) - (n9 / (m19 * nm19))) = ((n9 * (1 / (m9 * nm9))) - (n9 / (m19 * nm19))) by XCMPLX_1: 99

          .= ((n9 * (1 / (m9 * nm9))) - (n9 * (1 / (m19 * nm19)))) by XCMPLX_1: 99

          .= (n9 * ((1 / (m9 * nm9)) - (1 / (m19 * nm19))))

          .= (n9 * ((1 / (m9 * nm9)) * (((n + 1) - (2 * m)) / (nm + 1)))) by A8

          .= ((n9 * (1 / (m9 * nm9))) * (((n + 1) - (2 * m)) / (nm + 1)))

          .= (((n9 * 1) / (m9 * nm9)) * (((n + 1) - (2 * m)) / (nm + 1))) by XCMPLX_1: 74;

          hence thesis by A5, A10, A6, Th28;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:30

    

     Th30: ( card ( Domin_0 ((2 + k),1))) = (k + 1)

    proof

      ( card ( Domin_0 ((2 + k),1))) = (((((2 + k) + 1) - (2 * 1)) / (((2 + k) + 1) - 1)) * ((2 + k) choose 1)) by Th29, NAT_1: 11

      .= (((k + 1) / (2 + k)) * (2 + k)) by STIRL2_1: 51

      .= (k + 1) by XCMPLX_1: 87;

      hence thesis;

    end;

    theorem :: CATALAN2:31

    ( card ( Domin_0 ((4 + k),2))) = (((k + 1) * (k + 4)) / 2)

    proof

      ( card ( Domin_0 ((4 + k),2))) = (((((4 + k) + 1) - (2 * 2)) / (((4 + k) + 1) - 2)) * ((4 + k) choose 2)) by Th29, NAT_1: 11

      .= (((k + 1) / (k + 3)) * (((4 + k) * ((4 + k) - 1)) / 2)) by STIRL2_1: 51

      .= (((((k + 1) / (k + 3)) * (3 + k)) * (4 + k)) / 2)

      .= (((k + 1) * (4 + k)) / 2) by XCMPLX_1: 87;

      hence thesis;

    end;

    theorem :: CATALAN2:32

    ( card ( Domin_0 ((6 + k),3))) = ((((k + 1) * (k + 5)) * (k + 6)) / 6)

    proof

      ( card ( Domin_0 ((6 + k),3))) = (((((6 + k) + 1) - (2 * 3)) / (((6 + k) + 1) - 3)) * ((6 + k) choose 3)) by Th29, NAT_1: 11

      .= (((k + 1) / (k + 4)) * ((((6 + k) * ((6 + k) - 1)) * ((6 + k) - 2)) / 6)) by STIRL2_1: 51

      .= ((((((k + 1) / (k + 4)) * (4 + k)) * (5 + k)) * (6 + k)) / 6)

      .= ((((k + 1) * (5 + k)) * (6 + k)) / 6) by XCMPLX_1: 87;

      hence thesis;

    end;

    theorem :: CATALAN2:33

    

     Th33: ( card ( Domin_0 ((2 * n),n))) = (((2 * n) choose n) / (n + 1))

    proof

      ( card ( Domin_0 ((2 * n),n))) = (((((2 * n) + 1) - (2 * n)) / (((2 * n) + 1) - n)) * ((2 * n) choose n)) by Th29

      .= ((1 * ((2 * n) choose n)) / (n + 1)) by XCMPLX_1: 74;

      hence thesis;

    end;

    theorem :: CATALAN2:34

    

     Th34: ( card ( Domin_0 ((2 * n),n))) = ( Catalan (n + 1))

    proof

      

       A1: ( Catalan (n + 1)) = ((((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1)) by CATALAN1:def 1;

      (((2 * n) + 2) -' 2) = (((2 * n) + 2) - 2) & ((n + 1) -' 1) = ((n + 1) - 1) by XREAL_0:def 2;

      hence thesis by A1, Th33;

    end;

    definition

      let D;

      :: CATALAN2:def3

      mode OMEGA of D -> functional non empty set means

      : Def3: for x st x in it holds x is XFinSequence of D;

      existence

      proof

        reconsider D9OMEGA = (D ^omega ) as functional non empty set;

        take D9OMEGA;

        thus thesis by AFINSQ_1:def 7;

      end;

    end

    definition

      let D;

      :: original: ^omega

      redefine

      func D ^omega -> OMEGA of D ;

      coherence

      proof

        (D ^omega ) is functional & for x st x in (D ^omega ) holds x is XFinSequence of D by AFINSQ_1:def 7;

        hence thesis by Def3;

      end;

    end

    registration

      let D;

      let F be OMEGA of D;

      cluster -> finiteD -valued Sequence-like for Element of F;

      coherence by Def3;

    end

    reserve pN,qN for Element of ( NAT ^omega );

    theorem :: CATALAN2:35

    ( card { pN : ( dom pN) = (2 * n) & pN is dominated_by_0 }) = ((2 * n) choose n)

    proof

      set D = ( bool ( { 0 , 1} ^omega ));

      set 2n = (2 * n);

      defpred P[ set, set] means for i st i = $1 holds $2 = ( Domin_0 (2n,i));

      set Z = { pN : ( dom pN) = (2 * n) & pN is dominated_by_0 };

      

       A1: for k st k in ( Segm (n + 1)) holds ex x be Element of D st P[k, x]

      proof

        let k such that k in ( Segm (n + 1));

        reconsider Z = ( Domin_0 (2n,k)) as Element of D;

        take Z;

        thus thesis;

      end;

      consider r be XFinSequence of D such that

       A2: ( dom r) = ( Segm (n + 1)) & for k st k in ( Segm (n + 1)) holds P[k, (r . k)] from STIRL2_1:sch 5( A1);

      

       A3: Z c= ( union ( rng r))

      proof

        let x be object;

        assume x in Z;

        then

        consider pN such that

         A4: x = pN and

         A5: ( dom pN) = 2n & pN is dominated_by_0;

        pN in ( Domin_0 ((2 * n),( Sum pN))) by A5, Th20;

        then (2 * ( Sum pN)) <= 2n by Th22;

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

        then ( Sum pN) < (n + 1) by NAT_1: 13;

        then

         A6: ( Sum pN) in ( Segm (n + 1)) by NAT_1: 44;

        then (r . ( Sum pN)) = ( Domin_0 (2n,( Sum pN))) by A2;

        then

         A7: pN in (r . ( Sum pN)) by A5, Th20;

        (r . ( Sum pN)) in ( rng r) by A2, A6, FUNCT_1: 3;

        hence thesis by A4, A7, TARSKI:def 4;

      end;

      

       A8: ( union ( rng r)) c= Z

      proof

        let x be object;

        assume x in ( union ( rng r));

        then

        consider y such that

         A9: x in y and

         A10: y in ( rng r) by TARSKI:def 4;

        consider i be object such that

         A11: i in ( dom r) and

         A12: y = (r . i) by A10, FUNCT_1:def 3;

        reconsider i as Nat by A11;

        y = ( Domin_0 (2n,i)) by A2, A11, A12;

        then

        consider p such that

         A13: p = x & p is dominated_by_0 & ( dom p) = 2n and ( Sum p) = i by A9, Def2;

        p in ( NAT ^omega ) by AFINSQ_1:def 7;

        hence thesis by A13;

      end;

      

       A14: for i,j be Nat st i in ( dom r) & j in ( dom r) & i <> j holds (r . i) misses (r . j)

      proof

        let i,j be Nat such that

         A15: i in ( dom r) and

         A16: j in ( dom r) and

         A17: i <> j;

        assume (r . i) meets (r . j);

        then ((r . i) /\ (r . j)) <> {} ;

        then

        consider x be object such that

         A18: x in ((r . i) /\ (r . j)) by XBOOLE_0:def 1;

        

         A19: x in (r . j) by A18, XBOOLE_0:def 4;

        (r . j) = ( Domin_0 (2n,j)) by A2, A16;

        then

         A20: ex q st q = x & q is dominated_by_0 & ( dom q) = (2 * n) & ( Sum q) = j by A19, Def2;

        

         A21: x in (r . i) by A18, XBOOLE_0:def 4;

        (r . i) = ( Domin_0 (2n,i)) by A2, A15;

        then ex p st p = x & p is dominated_by_0 & ( dom p) = 2n & ( Sum p) = i by A21, Def2;

        hence thesis by A17, A20;

      end;

      

       A22: for i st i in ( dom r) holds (r . i) is finite

      proof

        let i;

        assume i in ( dom r);

        then (r . i) = ( Domin_0 (2n,i)) by A2;

        hence thesis;

      end;

      consider Cardr be XFinSequence of NAT such that

       A23: ( dom Cardr) = ( dom r) and

       A24: for i st i in ( dom Cardr) holds (Cardr . i) = ( card (r . i)) and

       A25: ( card ( union ( rng r))) = ( Sum Cardr) by A22, A14, STIRL2_1: 66;

      

       A26: n < ( dom Cardr) & (Cardr | (n + 1)) = Cardr by A2, A23, NAT_1: 13;

      defpred Q[ Nat] means $1 < ( len Cardr) implies ( Sum (Cardr | ($1 + 1))) = (2n choose $1);

      

       A27: Q[ 0 ]

      proof

         0 in ( Segm (n + 1)) by NAT_1: 44;

        then (r . 0 ) = ( Domin_0 (2n, 0 )) by A2;

        then

         A28: ( card (r . 0 )) = 1 by Th24;

        

         A29: 0 in ( Segm 1) by NAT_1: 44;

        assume

         A30: 0 < ( len Cardr);

        then 1 <= ( len Cardr) by NAT_1: 14;

        then

         A31: ( Segm 1) c= ( Segm ( len Cardr)) by NAT_1: 39;

        then

         A32: ( len (Cardr | 1)) = 1 by RELAT_1: 62;

        ( dom (Cardr | 1)) = 1 by A31, RELAT_1: 62;

        then ((Cardr | 1) . 0 ) = (Cardr . 0 ) by A29, FUNCT_1: 47;

        then

         A33: (Cardr | 1) = <%(Cardr . 0 )%> by A32, AFINSQ_1: 34;

         0 in ( len Cardr) by A30, AFINSQ_1: 86;

        then (Cardr . 0 ) = ( card (r . 0 )) by A24;

        then ( Sum (Cardr | 1)) = 1 by A33, A28, AFINSQ_2: 53;

        hence thesis by NEWTON: 19;

      end;

      

       A34: for i st Q[i] holds Q[(i + 1)]

      proof

        let i such that

         A35: Q[i];

        set i1 = (i + 1);

        assume

         A36: (i + 1) < ( len Cardr);

        then

         A37: i1 in ( dom Cardr) by AFINSQ_1: 86;

        then

         A38: (( Sum (Cardr | i1)) + (Cardr . i1)) = ( Sum (Cardr | (i1 + 1))) & (Cardr . i1) = ( card (r . i1)) by A24, AFINSQ_2: 65;

        i1 <= n by A2, A23, A36, NAT_1: 13;

        then

         A39: (2 * i1) <= 2n by XREAL_1: 64;

        (r . i1) = ( Domin_0 (2n,i1)) by A2, A23, A37;

        then ( Sum (Cardr | (i1 + 1))) = ((2n choose i) + ((2n choose i1) - (2n choose i))) by A35, A36, A38, A39, Th28, NAT_1: 13;

        hence thesis;

      end;

      for i holds Q[i] from NAT_1:sch 2( A27, A34);

      then ( Sum Cardr) = (2n choose n) by A26;

      hence thesis by A25, A3, A8, XBOOLE_0:def 10;

    end;

    theorem :: CATALAN2:36

    

     Th36: for n, m, k, j, l st j = (n - (2 * (k + 1))) & l = (m - (k + 1)) holds ( card { pN : pN in ( Domin_0 (n,m)) & (2 * (k + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) }) = (( card ( Domin_0 ((2 * k),k))) * ( card ( Domin_0 (j,l))))

    proof

      set q1 = (1 --> 1);

      set q0 = (1 --> 0 );

      let n, m, k, j, l such that

       A1: j = (n - (2 * (k + 1))) & l = (m - (k + 1));

      defpred P[ object, object] means ex r1,r2 be XFinSequence of NAT st $1 = (((q0 ^ r1) ^ q1) ^ r2) & ( len ((q0 ^ r1) ^ q1)) = (2 * (k + 1)) & $2 = [r1, r2];

      set Z2 = ( Domin_0 (j,l));

      set Z1 = ( Domin_0 ((2 * k),k));

      set F = { pN : pN in ( Domin_0 (n,m)) & (2 * (k + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) };

      set 2k1 = (2 * (k + 1));

      

       A2: for x be object st x in F holds ex y be object st y in [:Z1, Z2:] & P[x, y]

      proof

        

         A3: ( dom q0) = 1 & ( Sum q0) = ( 0 * 1) by AFINSQ_2: 58;

        let x be object;

        assume x in F;

        then

        consider pN such that

         A4: pN = x & pN in ( Domin_0 (n,m)) & 2k1 = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 });

        2k1 > (2 * 0 ) by XREAL_1: 68;

        then

        reconsider M = { N : (2 * ( Sum (pN | N))) = N & N > 0 } as non empty Subset of NAT by A4, NAT_1:def 1;

        consider r2 be XFinSequence of NAT such that

         A5: pN = ((pN | 2k1) ^ r2) by Th1;

        2k1 > (2 * 0 ) & pN is dominated_by_0 by A4, Th20, XREAL_1: 68;

        then

        consider r1 be XFinSequence of NAT such that

         A6: (pN | 2k1) = ((q0 ^ r1) ^ q1) and

         A7: r1 is dominated_by_0 by A4, Th14;

        

         A8: ( Sum q1) = (1 * 1) by AFINSQ_2: 58;

        2k1 in M by A4, NAT_1:def 1;

        then

         A9: ex o be Nat st o = 2k1 & (2 * ( Sum (pN | o))) = o & o > 0 ;

        then (k + 1) = (( Sum (q0 ^ r1)) + ( Sum q1)) by A6, AFINSQ_2: 55;

        then

         A10: k = (( Sum q0) + ( Sum r1)) by A8, AFINSQ_2: 55;

        pN is dominated_by_0 by A4, Th20;

        then

         A11: r2 is dominated_by_0 by A5, A9, Th12;

        pN is dominated_by_0 by A4, Th20;

        then

         A12: ( len (pN | 2k1)) = 2k1 by A9, Th11;

        ( Sum pN) = m by A4, Th20;

        then

         A13: m = ((k + 1) + ( Sum r2)) by A5, A9, AFINSQ_2: 55;

        take [r1, r2];

        ( dom pN) = n by A4, Th20;

        then n = (2k1 + ( len r2)) by A5, A12, AFINSQ_1:def 3;

        then

         A15: r2 in Z2 by A1, A13, A11, Th20;

        2k1 = (( len (q0 ^ r1)) + ( len q1)) by A6, A12, AFINSQ_1: 17;

        then ((2 * k) + 1) = (( len q0) + ( len r1)) by AFINSQ_1: 17;

        then r1 in Z1 by A7, A10, A3, Th20;

        hence thesis by A4, A5, A6, A12, A15, ZFMISC_1:def 2;

      end;

      consider f be Function of F, [:Z1, Z2:] such that

       A16: for x be object st x in F holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

      

       A17: [:Z1, Z2:] = {} implies F = {}

      proof

        assume [:Z1, Z2:] = {} ;

        then Z1 = {} or Z2 = {} ;

        then (2 * l) > j by Th22;

        then ((2 * m) - (2 * (k + 1))) > (n - (2 * (k + 1))) by A1;

        then

         A18: (2 * m) > n by XREAL_1: 9;

        assume F <> {} ;

        then

        consider x be object such that

         A19: x in F by XBOOLE_0:def 1;

        ex pN st pN = x & pN in ( Domin_0 (n,m)) & 2k1 = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) by A19;

        hence thesis by A18, Th22;

      end;

      then

       A20: ( dom f) = F by FUNCT_2:def 1;

      

       A21: ( rng f) = [:Z1, Z2:]

      proof

        

         A22: ( Sum q0) = (1 * 0 ) & ( Sum q1) = (1 * 1) by AFINSQ_2: 58;

        thus ( rng f) c= [:Z1, Z2:];

        let x be object;

        assume x in [:Z1, Z2:];

        then

        consider x1,x2 be object such that

         A24: x1 in Z1 and

         A25: x2 in Z2 and

         A26: x = [x1, x2] by ZFMISC_1:def 2;

        consider p such that

         A27: p = x1 and

         A28: p is dominated_by_0 and

         A29: ( dom p) = (2 * k) and

         A30: ( Sum p) = k by A24, Def2;

        consider q such that

         A31: q = x2 and

         A32: q is dominated_by_0 and

         A33: ( dom q) = j and

         A34: ( Sum q) = l by A25, Def2;

        set 0p1 = ((q0 ^ p) ^ q1);

        

         A35: ( dom (0p1 ^ q)) = (( len 0p1) + ( len q)) by AFINSQ_1:def 3;

        ( dom 0p1) = (( len (q0 ^ p)) + ( len q1)) & ( dom q1) = 1 by AFINSQ_1:def 3;

        then

         A36: ( dom 0p1) = ((( len q0) + ( len p)) + 1) by AFINSQ_1: 17;

        then ((0p1 ^ q) | ((2 * 1) + ( len p))) = 0p1 by AFINSQ_1: 57;

        then

         A37: ( min* { N : (2 * ( Sum ((0p1 ^ q) | N))) = N & N > 0 }) = ((2 * 1) + ( len p)) by A28, A29, A30, Th16;

        1 <= ((1 + ( len p)) - (2 * ( Sum p))) by A29, A30;

        then 0p1 is dominated_by_0 by A28, Th10;

        then

         A38: (0p1 ^ q) is dominated_by_0 by A32, Th7;

        

         A39: (0p1 ^ q) in ( NAT ^omega ) by AFINSQ_1:def 7;

        0p1 = (q0 ^ (p ^ q1)) by AFINSQ_1: 27;

        then ( Sum 0p1) = (( Sum q0) + ( Sum (p ^ q1))) by AFINSQ_2: 55;

        then ( Sum 0p1) = ( 0 qua Nat + (( Sum p) + 1)) by A22, AFINSQ_2: 55;

        then ( Sum (0p1 ^ q)) = ((k + 1) + l) by A30, A34, AFINSQ_2: 55;

        then (0p1 ^ q) in ( Domin_0 (n,m)) by A1, A29, A33, A38, A36, A35, Th20;

        then

         A40: (0p1 ^ q) in F by A29, A37, A39;

        then

        consider r1,r2 be XFinSequence of NAT such that

         A41: (0p1 ^ q) = (((q0 ^ r1) ^ q1) ^ r2) and

         A42: ( len ((q0 ^ r1) ^ q1)) = 2k1 and

         A43: (f . (0p1 ^ q)) = [r1, r2] by A16;

        

         A44: ((0p1 ^ q) | 2k1) = 0p1 by A29, A36, AFINSQ_1: 57;

        then (q0 ^ p) = (q0 ^ r1) by A41, A42, AFINSQ_1: 28, AFINSQ_1: 57;

        then

         A45: p = r1 by AFINSQ_1: 28;

        ((((q0 ^ r1) ^ q1) ^ r2) | 2k1) = ((q0 ^ r1) ^ q1) by A42, AFINSQ_1: 57;

        then q = r2 by A41, A44, AFINSQ_1: 28;

        hence thesis by A20, A26, A27, A31, A40, A43, A45, FUNCT_1: 3;

      end;

      for x,y be object st x in F & y in F & (f . x) = (f . y) holds x = y

      proof

        let x,y be object such that

         A46: x in F and

         A47: y in F and

         A48: (f . x) = (f . y);

        consider y1,y2 be XFinSequence of NAT such that

         A49: y = (((q0 ^ y1) ^ q1) ^ y2) and ( len ((q0 ^ y1) ^ q1)) = 2k1 and

         A50: (f . y) = [y1, y2] by A16, A47;

        consider x1,x2 be XFinSequence of NAT such that

         A51: x = (((q0 ^ x1) ^ q1) ^ x2) and ( len ((q0 ^ x1) ^ q1)) = 2k1 and

         A52: (f . x) = [x1, x2] by A16, A46;

        x1 = y1 by A48, A52, A50, XTUPLE_0: 1;

        hence thesis by A48, A51, A52, A49, A50, XTUPLE_0: 1;

      end;

      then f is one-to-one by A17, FUNCT_2: 19;

      then (F, [:Z1, Z2:]) are_equipotent by A20, A21, WELLORD2:def 4;

      then ( card F) = ( card [:Z1, Z2:]) by CARD_1: 5;

      hence thesis by CARD_2: 46;

    end;

    theorem :: CATALAN2:37

    

     Th37: for n, m st (2 * m) <= n holds ex CardF be XFinSequence of NAT st ( card { pN : pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} }) = ( Sum CardF) & ( dom CardF) = m & for j st j < m holds (CardF . j) = (( card ( Domin_0 ((2 * j),j))) * ( card ( Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))))

    proof

      let n, m such that

       A1: (2 * m) <= n;

      set Z = ( Domin_0 (n,m));

      defpred P[ set, set] means for j st j = $1 holds $2 = { pN : pN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) };

      set W = { pN : pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} };

      

       A2: for k st k in ( Segm m) holds ex x be Element of ( bool Z) st P[k, x]

      proof

        let k such that k in ( Segm m);

        set NN = { pN : pN in ( Domin_0 (n,m)) & (2 * (k + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) };

        NN c= Z

        proof

          let x be object;

          assume x in NN;

          then ex pN st x = pN & pN in Z & (2 * (k + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 });

          hence thesis;

        end;

        then

        reconsider NN as Element of ( bool Z);

        take NN;

        thus thesis;

      end;

      consider C be XFinSequence of ( bool Z) such that

       A3: ( dom C) = ( Segm m) & for k st k in ( Segm m) holds P[k, (C . k)] from STIRL2_1:sch 5( A2);

      

       A4: W c= ( union ( rng C))

      proof

        let x be object;

        assume x in W;

        then

        consider pN such that

         A5: x = pN & pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} ;

        set I = { N : (2 * ( Sum (pN | N))) = N & N > 0 };

        I c= NAT

        proof

          let y be object;

          assume y in I;

          then ex i be Nat st i = y & (2 * ( Sum (pN | i))) = i & i > 0 ;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider I as non empty Subset of NAT by A5;

        ( min* I) in I by NAT_1:def 1;

        then

        consider M be Nat such that

         A6: ( min* I) = M and

         A7: (2 * ( Sum (pN | M))) = M and

         A8: M > 0 ;

        ( Sum (pN | M)) > 0 by A7, A8;

        then

        reconsider Sum1 = (( Sum (pN | M)) - 1) as Nat by NAT_1: 20;

        consider q such that

         A9: pN = ((pN | M) ^ q) by Th1;

        ( Sum pN) = (( Sum (pN | M)) + ( Sum q)) by A9, AFINSQ_2: 55;

        then m = (( Sum (pN | M)) + ( Sum q)) by A5, Th20;

        then

         A10: m >= ( Sum (pN | M)) by NAT_1: 11;

        (Sum1 + 1) > Sum1 by NAT_1: 13;

        then m > Sum1 by A10, XXREAL_0: 2;

        then

         A11: Sum1 in ( Segm m) by NAT_1: 44;

        then (C . Sum1) = { qN : qN in ( Domin_0 (n,m)) & (2 * (Sum1 + 1)) = ( min* { N : (2 * ( Sum (qN | N))) = N & N > 0 }) } by A3;

        then

         A12: pN in (C . Sum1) by A5, A6, A7;

        (C . Sum1) in ( rng C) by A3, A11, FUNCT_1: 3;

        hence thesis by A5, A12, TARSKI:def 4;

      end;

      

       A13: for i, j st i in ( dom C) & j in ( dom C) & i <> j holds (C . i) misses (C . j)

      proof

        let i, j such that

         A14: i in ( dom C) and

         A15: j in ( dom C) and

         A16: i <> j;

        assume (C . i) meets (C . j);

        then ((C . i) /\ (C . j)) <> {} ;

        then

        consider x be object such that

         A17: x in ((C . i) /\ (C . j)) by XBOOLE_0:def 1;

        

         A18: x in (C . j) by A17, XBOOLE_0:def 4;

        (C . j) = { qN : qN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (qN | N))) = N & N > 0 }) } by A3, A15;

        then

         A19: ex qN st x = qN & qN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (qN | N))) = N & N > 0 }) by A18;

        

         A20: x in (C . i) by A17, XBOOLE_0:def 4;

        (C . i) = { pN : pN in ( Domin_0 (n,m)) & (2 * (i + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) } by A3, A14;

        then ex pN st x = pN & pN in ( Domin_0 (n,m)) & (2 * (i + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) by A20;

        hence thesis by A16, A19;

      end;

      

       A21: for k st k in ( dom C) holds (C . k) is finite

      proof

        let k;

        assume k in ( dom C);

        then

         A22: (C . k) in ( rng C) by FUNCT_1: 3;

        thus thesis by A22;

      end;

      consider CardC be XFinSequence of NAT such that

       A23: ( dom CardC) = ( dom C) and

       A24: for i st i in ( dom CardC) holds (CardC . i) = ( card (C . i)) and

       A25: ( card ( union ( rng C))) = ( Sum CardC) by A21, A13, STIRL2_1: 66;

      take CardC;

      ( union ( rng C)) c= W

      proof

        let x be object;

        assume x in ( union ( rng C));

        then

        consider y such that

         A26: x in y and

         A27: y in ( rng C) by TARSKI:def 4;

        consider j be object such that

         A28: j in ( dom C) and

         A29: (C . j) = y by A27, FUNCT_1:def 3;

        reconsider j as Nat by A28;

        y = { pN : pN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) } by A3, A28, A29;

        then

        consider pN such that

         A30: x = pN & pN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) by A26;

        (2 * (j + 1)) <> 0 ;

        then { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} by A30, NAT_1:def 1;

        hence thesis by A30;

      end;

      hence ( card W) = ( Sum CardC) & ( dom CardC) = m by A3, A23, A25, A4, XBOOLE_0:def 10;

      let j such that

       A31: j < m;

      

       A32: m >= (j + 1) by A31, NAT_1: 13;

      then

       A33: (m -' (j + 1)) = (m - (j + 1)) by XREAL_1: 233;

      set P = { pN : pN in ( Domin_0 (n,m)) & (2 * (j + 1)) = ( min* { N : (2 * ( Sum (pN | N))) = N & N > 0 }) };

      j < ( len C) by A3, A31;

      then

       A34: j in ( dom C) by A3, NAT_1: 44;

      then

       A35: (C . j) = P by A3;

      (2 * (j + 1)) <= (2 * m) by A32, XREAL_1: 64;

      then

       A36: (n -' (2 * (j + 1))) = (n - (2 * (j + 1))) by A1, XREAL_1: 233, XXREAL_0: 2;

      (CardC . j) = ( card (C . j)) by A23, A24, A34;

      hence thesis by A36, A33, A35, Th36;

    end;

    theorem :: CATALAN2:38

    

     Th38: for n st n > 0 holds ( Domin_0 ((2 * n),n)) = { pN : pN in ( Domin_0 ((2 * n),n)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} }

    proof

      let n such that

       A1: n > 0 ;

      set P = { pN : pN in ( Domin_0 ((2 * n),n)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} };

      thus ( Domin_0 ((2 * n),n)) c= P

      proof

        

         A2: (n + n) > ( 0 qua Nat + 0 qua Nat) by A1;

        let x be object such that

         A3: x in ( Domin_0 ((2 * n),n));

        consider p such that

         A4: x = p and p is dominated_by_0 and

         A5: ( dom p) = (2 * n) & ( Sum p) = n by A3, Def2;

        

         A6: p in ( NAT ^omega ) by AFINSQ_1:def 7;

        (2 * ( Sum (p | (2 * n)))) = (2 * n) by A5;

        then (2 * n) in { N : (2 * ( Sum (p | N))) = N & N > 0 } by A2;

        hence thesis by A3, A4, A6;

      end;

      thus P c= ( Domin_0 ((2 * n),n))

      proof

        let x be object;

        assume x in P;

        then ex pN st x = pN & pN in ( Domin_0 ((2 * n),n)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} ;

        hence thesis;

      end;

    end;

    theorem :: CATALAN2:39

    

     Th39: for n st n > 0 holds ex Catal be XFinSequence of NAT st ( Sum Catal) = ( Catalan (n + 1)) & ( dom Catal) = n & for j st j < n holds (Catal . j) = (( Catalan (j + 1)) * ( Catalan (n -' j)))

    proof

      let n such that

       A1: n > 0 ;

      consider CardF be XFinSequence of NAT such that

       A2: ( card { pN : pN in ( Domin_0 ((2 * n),n)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} }) = ( Sum CardF) and

       A3: ( dom CardF) = n and

       A4: for j st j < n holds (CardF . j) = (( card ( Domin_0 ((2 * j),j))) * ( card ( Domin_0 (((2 * n) -' (2 * (j + 1))),(n -' (j + 1)))))) by Th37;

      take CardF;

      ( Sum CardF) = ( card ( Domin_0 ((2 * n),n))) by A1, A2, Th38;

      hence ( Sum CardF) = ( Catalan (n + 1)) & ( dom CardF) = n by A3, Th34;

      let j such that

       A5: j < n;

      (n - j) > (j - j) by A5, XREAL_1: 9;

      then (n -' j) > 0 by A5, XREAL_1: 233;

      then

      reconsider nj = ((n -' j) - 1) as Nat by NAT_1: 20;

      (j + 1) <= n by A5, NAT_1: 13;

      then

       A6: ((2 * n) -' (2 * (j + 1))) = ((2 * n) - (2 * (j + 1))) & (n -' (j + 1)) = (n - (j + 1)) by XREAL_1: 64, XREAL_1: 233;

      

       A7: ( card ( Domin_0 ((2 * j),j))) = ( Catalan (j + 1)) by Th34;

      (n - j) = (n -' j) by A5, XREAL_1: 233;

      

      then ( card ( Domin_0 (((2 * n) -' (2 * (j + 1))),(n -' (j + 1))))) = ( card ( Domin_0 ((2 * nj),nj))) by A6

      .= ( Catalan (nj + 1)) by Th34;

      hence thesis by A4, A5, A7;

    end;

    theorem :: CATALAN2:40

    

     Th40: ( card { pN : pN in ( Domin_0 ((n + 1),m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} }) = ( card ( Domin_0 (n,m)))

    proof

      defpred P[ object, object] means ex p st $1 = ( <% 0 %> ^ p) & $2 = p;

      set F = { pN : pN in ( Domin_0 ((n + 1),m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} };

      set Z = ( Domin_0 (n,m));

      

       A1: for x be object st x in F holds ex y be object st y in Z & P[x, y]

      proof

        

         A2: ( len <% 0 %>) = 1 by AFINSQ_1: 33;

        let x be object;

        

         A3: ( Sum <% 0 %>) = 0 by AFINSQ_2: 53;

        assume x in F;

        then

        consider pN such that

         A4: x = pN & pN in ( Domin_0 ((n + 1),m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} ;

        pN is dominated_by_0 & ( dom pN) = (n + 1) by A4, Th20;

        then

        consider q such that

         A6: pN = ( <% 0 %> ^ q) and

         A7: q is dominated_by_0 by A4, Th17;

        ( dom pN) = (( len <% 0 %>) + ( len q)) by A6, AFINSQ_1:def 3;

        then

         A8: (n + 1) = (( len q) + 1) by A4, A2, Th20;

        take q;

        ( Sum pN) = (( Sum <% 0 %>) + ( Sum q)) by A6, AFINSQ_2: 55;

        then ( Sum q) = m by A4, A3, Th20;

        hence thesis by A4, A6, A7, A8, Th20;

      end;

      consider f be Function of F, Z such that

       A9: for x be object st x in F holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

      

       A10: Z = {} implies F = {}

      proof

        assume Z = {} ;

        then (2 * m) > n by Th22;

        then

         A11: (2 * m) >= (n + 1) by NAT_1: 13;

        assume F <> {} ;

        then

        consider x be object such that

         A12: x in F by XBOOLE_0:def 1;

        consider pN such that

         A13: x = pN & pN in ( Domin_0 ((n + 1),m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} by A12;

        ( dom pN) = (n + 1) by A13, Th20;

        then (pN | (n + 1)) = pN;

        then

         A14: ( Sum (pN | (n + 1))) = m by A13, Th20;

        pN is dominated_by_0 by A13, Th20;

        then (2 * m) <= (n + 1) by A14, Th2;

        then (2 * ( Sum (pN | (n + 1)))) = (n + 1) by A14, A11, XXREAL_0: 1;

        then (n + 1) in { N : (2 * ( Sum (pN | N))) = N & N > 0 };

        hence thesis by A13;

      end;

      then

       A15: ( dom f) = F by FUNCT_2:def 1;

      

       A16: ( rng f) = Z

      proof

        thus ( rng f) c= Z;

        let x be object;

        assume x in Z;

        then

        consider p such that

         A17: p = x and

         A18: p is dominated_by_0 and

         A19: ( dom p) = n and

         A20: ( Sum p) = m by Def2;

        set q = ( <% 0 %> ^ p);

        

         A21: { N : (2 * ( Sum (q | N))) = N & N > 0 } = {} by A18, Th18;

        ( Sum q) = (( Sum <% 0 %>) + ( Sum p)) by AFINSQ_2: 55;

        then

         A22: ( Sum q) = ( 0 qua Nat + m) by A20, AFINSQ_2: 53;

        

         A23: q in ( NAT ^omega ) by AFINSQ_1:def 7;

        ( dom q) = (( len <% 0 %>) + ( len p)) by AFINSQ_1:def 3;

        then

         A24: ( dom q) = (1 + n) by A19, AFINSQ_1: 33;

        q is dominated_by_0 by A18, Th18;

        then q in ( Domin_0 ((n + 1),m)) by A24, A22, Th20;

        then

         A25: q in F by A21, A23;

        then

        consider r be XFinSequence of NAT such that

         A26: q = ( <% 0 %> ^ r) and

         A27: (f . q) = r by A9;

        r = p by A26, AFINSQ_1: 28;

        hence thesis by A15, A17, A25, A27, FUNCT_1: 3;

      end;

      for x,y be object st x in F & y in F & (f . x) = (f . y) holds x = y

      proof

        let x,y be object such that

         A28: x in F & y in F and

         A29: (f . x) = (f . y);

        (ex p st x = ( <% 0 %> ^ p) & (f . x) = p) & ex q st y = ( <% 0 %> ^ q) & (f . y) = q by A9, A28;

        hence thesis by A29;

      end;

      then f is one-to-one by A10, FUNCT_2: 19;

      then (F,Z) are_equipotent by A15, A16, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: CATALAN2:41

    for n, m st (2 * m) <= n holds ex CardF be XFinSequence of NAT st ( card ( Domin_0 (n,m))) = (( Sum CardF) + ( card ( Domin_0 ((n -' 1),m)))) & ( dom CardF) = m & for j st j < m holds (CardF . j) = (( card ( Domin_0 ((2 * j),j))) * ( card ( Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))))

    proof

      let n, m such that

       A1: (2 * m) <= n;

      set Z = ( Domin_0 (n,m));

      set Zne = { pN : pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} };

      

       A2: Zne c= Z

      proof

        let x be object;

        assume x in Zne;

        then ex pN st x = pN & pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} ;

        hence thesis;

      end;

      set Ze = { pN : pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} };

      

       A3: Ze c= Z

      proof

        let x be object;

        assume x in Ze;

        then ex pN st x = pN & pN in ( Domin_0 (n,m)) & { N : (2 * ( Sum (pN | N))) = N & N > 0 } = {} ;

        hence thesis;

      end;

      reconsider Zne as finite set by A2;

      consider C be XFinSequence of NAT such that

       A4: ( card Zne) = ( Sum C) and

       A5: ( dom C) = m and

       A6: for j st j < m holds (C . j) = (( card ( Domin_0 ((2 * j),j))) * ( card ( Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1)))))) by A1, Th37;

      reconsider Ze as finite set by A3;

      take C;

      

       A7: Ze misses Zne

      proof

        assume Ze meets Zne;

        then

        consider x be object such that

         A8: x in Ze and

         A9: x in Zne by XBOOLE_0: 3;

        

         A10: ex qN st qN = x & qN in Z & { N : (2 * ( Sum (qN | N))) = N & N > 0 } = {} by A8;

        ex pN st pN = x & pN in Z & { N : (2 * ( Sum (pN | N))) = N & N > 0 } <> {} by A9;

        hence thesis by A10;

      end;

      

       A11: Z c= (Ze \/ Zne)

      proof

        let x be object such that

         A12: x in Z;

        consider p be XFinSequence of NAT such that

         A13: p = x and p is dominated_by_0 and ( dom p) = n and ( Sum p) = m by A12, Def2;

        reconsider p as Element of ( NAT ^omega ) by AFINSQ_1:def 7;

        set I = { N : (2 * ( Sum (p | N))) = N & N > 0 };

        now

          per cases ;

            suppose I = {} ;

            then p in Ze by A12, A13;

            hence thesis by A13, XBOOLE_0:def 3;

          end;

            suppose I <> {} ;

            then p in Zne by A12, A13;

            hence thesis by A13, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      (Ze \/ Zne) c= Z by A3, A2, XBOOLE_1: 8;

      then

       A14: (Ze \/ Zne) = Z by A11;

      now

        per cases ;

          suppose

           A15: n = 0 ;

          then (2 * m) = 0 by A1;

          then C = {} by A5;

          then

           A16: ( Sum C) = 0 ;

          (n - 1) < (1 - 1) by A15;

          hence ( card Z) = (( Sum C) + ( card ( Domin_0 ((n -' 1),m)))) by A15, A16, XREAL_0:def 2;

        end;

          suppose

           A17: n > 0 ;

          then

          reconsider n1 = (n - 1) as Nat by NAT_1: 20;

          n = (n1 + 1);

          then

           A18: ( card Ze) = ( card ( Domin_0 (n1,m))) by Th40;

          n1 = (n -' 1) by A17, NAT_1: 14, XREAL_1: 233;

          hence ( card Z) = (( Sum C) + ( card ( Domin_0 ((n -' 1),m)))) by A7, A14, A4, A18, CARD_2: 40;

        end;

      end;

      hence thesis by A5, A6;

    end;

    theorem :: CATALAN2:42

    for n, k holds ex p st ( Sum p) = ( card ( Domin_0 ((((2 * n) + 2) + k),(n + 1)))) & ( dom p) = (k + 1) & for i st i <= k holds (p . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n)))

    proof

      let n, k;

      defpred P[ set, set] means for j st $1 = j holds $2 = ( card ( Domin_0 ((((2 * n) + 1) + j),n)));

      

       A1: for i st i in ( Segm (k + 1)) holds ex x be Element of NAT st P[i, x]

      proof

        let i such that i in ( Segm (k + 1));

         P[i, ( card ( Domin_0 ((((2 * n) + 1) + i),n)))];

        hence thesis;

      end;

      consider p such that

       A2: ( dom p) = ( Segm (k + 1)) and

       A3: for i be Nat st i in ( Segm (k + 1)) holds P[i, (p . i)] from STIRL2_1:sch 5( A1);

      take p;

      

       A4: for i st i <= k holds (p . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n)))

      proof

        let i;

        assume i <= k;

        then i < (k + 1) by NAT_1: 13;

        then i in ( Segm (k + 1)) by NAT_1: 44;

        hence thesis by A3;

      end;

      now

        per cases ;

          suppose

           A5: n = 0 ;

          for x be object st x in ( dom p) holds (p . x) = 1

          proof

            let x be object such that

             A6: x in ( dom p);

            reconsider i = x as Nat by A6;

            (p . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n))) by A2, A3, A6;

            hence thesis by A5, Th24;

          end;

          then p = ((k + 1) --> 1) by A2, FUNCOP_1: 11;

          then ( Sum p) = ((k + 1) * 1) by AFINSQ_2: 58;

          hence ( Sum p) = ( card ( Domin_0 ((((2 * n) + 2) + k),(n + 1)))) by A5, Th30;

        end;

          suppose n > 0 ;

          then

          reconsider n1 = (n - 1) as Nat by NAT_1: 20;

          defpred Q[ Nat] means for q st ( dom q) = ($1 + 1) & for i st i <= $1 holds (q . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n))) holds ( Sum q) = ( card ( Domin_0 ((((2 * n) + 2) + $1),(n + 1))));

          

           A7: for j st Q[j] holds Q[(j + 1)]

          proof

            let j such that

             A8: Q[j];

            set CH2 = ((((2 * n) + 2) + j) choose (n1 + 1));

            set CH1 = ((((2 * n) + 2) + j) choose (n + 1));

            set j1 = (j + 1);

            let q such that

             A9: ( dom q) = (j1 + 1) and

             A10: for i st i <= j1 holds (q . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n)));

            

             A11: (2 * (n + 1)) <= ((2 * (n + 1)) + j1) by NAT_1: 11;

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

            then ( Segm j1) c= ( Segm (j1 + 1)) by NAT_1: 39;

            then

             A12: ( dom (q | j1)) = j1 by A9, RELAT_1: 62;

            

             A13: for i st i <= j holds ((q | j1) . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n)))

            proof

              let i;

              assume i <= j;

              then i < j1 by NAT_1: 13;

              then i < ( len (q | j1)) by A12;

              then i in ( dom (q | j1)) & (q . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n))) by A10, A12, AFINSQ_1: 86;

              hence thesis by FUNCT_1: 47;

            end;

            set CH4 = ((((2 * n) + 1) + j1) choose n1);

            set CH3 = ((((2 * n) + 1) + j1) choose n);

            

             A14: (2 * n) <= ((2 * n) + (1 + j1)) & (n1 + 1) = n by NAT_1: 11;

            (q . j1) = ( card ( Domin_0 ((((2 * n) + 1) + j1),n))) by A10;

            then

             A15: (q . j1) = (CH3 - CH4) by A14, Th28;

            j1 < (j1 + 1) by NAT_1: 13;

            then j1 < ( len q) by A9;

            then j1 in ( dom q) by AFINSQ_1: 86;

            then

             A16: ( Sum (q | (j1 + 1))) = (( Sum (q | j1)) + (q . j1)) by AFINSQ_2: 65;

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

            then ( card ( Domin_0 ((((2 * n) + 2) + j),(n + 1)))) = (CH1 - CH2) by Th28;

            then ( Sum (q | j1)) = (CH1 - CH2) by A8, A12, A13;

            

            then (( Sum (q | j1)) + (q . j1)) = ((CH1 + CH2) - (CH3 + CH4)) by A15

            .= ((((((2 * n) + 2) + j) + 1) choose (n + 1)) - (CH3 + CH4)) by NEWTON: 22

            .= (((((2 * n) + 2) + j1) choose (n + 1)) - ((((2 * n) + 2) + j1) choose (n1 + 1))) by NEWTON: 22

            .= ( card ( Domin_0 ((((2 * n) + 2) + j1),(n + 1)))) by A11, Th28;

            hence thesis by A9, A16;

          end;

          

           A17: Q[ 0 ]

          proof

            reconsider 2n1 = ((2 * n) + 1) as Nat;

            set 2CHn = (((2 * n) + 2) choose n);

            set 2CHn91 = (((2 * n) + 2) choose (n + 1));

            set CHn91 = (2n1 choose (n + 1));

            set CHn1 = (2n1 choose n1);

            set CHn = (2n1 choose n);

            let q;

            assume ( dom q) = ( 0 qua Nat + 1) & for i st i <= 0 holds (q . i) = ( card ( Domin_0 ((((2 * n) + 1) + i),n)));

            then

             A18: (q . 0 ) = ( card ( Domin_0 ((((2 * n) + 1) + 0 qua Nat),n))) & ( len q) = 1;

            

             A19: ((2 * n) + 2) = (((2 * n) + 1) + 1);

            then

             A20: 2CHn91 = (CHn91 + CHn) by NEWTON: 22;

            (n1 + 1) = n;

            then

             A21: 2CHn = (CHn + CHn1) by A19, NEWTON: 22;

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

            then

             A22: CHn = CHn91 by NEWTON: 20;

            (2 * (n + 1)) = ((2 * n) + 2);

            then

             A23: ( card ( Domin_0 (((2 * n) + 2),(n + 1)))) = (2CHn91 - 2CHn) by Th28;

            ( card ( Domin_0 (2n1,(n1 + 1)))) = (CHn - CHn1) & ( Sum <%(q . 0 )%>) = (q . 0 ) by Th28, AFINSQ_2: 53, NAT_1: 11;

            hence thesis by A20, A21, A22, A23, A18, AFINSQ_1: 34;

          end;

          for j holds Q[j] from NAT_1:sch 2( A17, A7);

          hence ( Sum p) = ( card ( Domin_0 ((((2 * n) + 2) + k),(n + 1)))) by A2, A4;

        end;

      end;

      hence thesis by A2, A4;

    end;

    begin

    reserve seq1,seq2,seq3,seq4 for Real_Sequence,

r,s,e for Real,

Fr,Fr1,Fr2 for XFinSequence of REAL ;

    

     Lm3: (( dom Fr) = 1 or ( len Fr) = 1) implies ( Sum Fr) = (Fr . 0 )

    proof

      assume ( dom Fr) = 1 or ( len Fr) = 1;

      then ( len Fr) = 1;

      then Fr = <%(Fr . 0 )%> by AFINSQ_1: 34;

      hence thesis by AFINSQ_2: 53;

    end;

    

     Lm4: for Fr1, Fr2 st ( dom Fr1) = ( dom Fr2) & for n st n in ( len Fr1) holds (Fr1 . n) = (Fr2 . (( len Fr1) -' (1 + n))) holds ( Sum Fr1) = ( Sum Fr2)

    proof

      let Fr1, Fr2 such that

       A1: ( dom Fr1) = ( dom Fr2) and

       A2: for n st n in ( len Fr1) holds (Fr1 . n) = (Fr2 . (( len Fr1) -' (1 + n)));

      defpred P[ object, object] means for i st i = $1 holds $2 = (( len Fr1) -' (1 + i));

      

       A3: ( card ( len Fr1)) = ( card ( len Fr1));

      

       A4: for x be object st x in ( len Fr1) holds ex y be object st y in ( len Fr1) & P[x, y]

      proof

        let x be object such that

         A5: x in ( len Fr1);

        reconsider k = x as Nat by A5;

        k < ( len Fr1) by A5, AFINSQ_1: 86;

        then (k + 1) <= ( len Fr1) by NAT_1: 13;

        then

         A6: (( len Fr1) -' (1 + k)) = (( len Fr1) - (1 + k)) by XREAL_1: 233;

        take (( len Fr1) -' (1 + k));

        (( len Fr1) + 0 qua Nat) < (( len Fr1) + (1 + k)) by XREAL_1: 8;

        then (( len Fr1) - (1 + k)) < ((( len Fr1) + (1 + k)) - (1 + k)) by XREAL_1: 9;

        hence thesis by A6, AFINSQ_1: 86;

      end;

      consider P be Function of ( len Fr1), ( len Fr1) such that

       A7: for x be object st x in ( len Fr1) holds P[x, (P . x)] from FUNCT_2:sch 1( A4);

      for x1,x2 be object st x1 in ( len Fr1) & x2 in ( len Fr1) & (P . x1) = (P . x2) holds x1 = x2

      proof

        let x1,x2 be object such that

         A8: x1 in ( len Fr1) and

         A9: x2 in ( len Fr1) and

         A10: (P . x1) = (P . x2);

        reconsider i = x1, j = x2 as Nat by A8, A9;

        j < ( len Fr1) by A9, AFINSQ_1: 86;

        then (j + 1) <= ( len Fr1) by NAT_1: 13;

        then (( len Fr1) -' (1 + j)) = (( len Fr1) - (1 + j)) by XREAL_1: 233;

        then

         A11: (P . x2) = (( len Fr1) - (1 + j)) by A7, A9;

        i < ( len Fr1) by A8, AFINSQ_1: 86;

        then (i + 1) <= ( len Fr1) by NAT_1: 13;

        then (( len Fr1) -' (1 + i)) = (( len Fr1) - (1 + i)) by XREAL_1: 233;

        then (P . x1) = (( len Fr1) - (1 + i)) by A7, A8;

        hence thesis by A10, A11;

      end;

      then

       A12: P is one-to-one by FUNCT_2: 56;

      then P is onto by A3, FINSEQ_4: 63;

      then

      reconsider P as Permutation of ( dom Fr1) by A12;

       A13:

      now

        let x be object such that

         A14: x in ( dom Fr1);

        reconsider k = x as Nat by A14;

        (P . k) = (( len Fr1) -' (1 + k)) by A7, A14;

        hence (Fr1 . x) = (Fr2 . (P . x)) by A2, A14;

      end;

      

       A15: for x be object st x in ( dom Fr1) holds x in ( dom P) & (P . x) in ( dom Fr2)

      proof

        let x be object;

        assume x in ( dom Fr1);

        hence x in ( dom P) by FUNCT_2: 52;

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

        then (P . x) in ( dom Fr1);

        then (P . x) in ( dom P) by FUNCT_2: 52;

        hence thesis by A1;

      end;

      for x be object st x in ( dom P) & (P . x) in ( dom Fr2) holds x in ( dom Fr1);

      then Fr1 = (Fr2 * P) by A15, A13, FUNCT_1: 10;

      

      then ( addreal "**" Fr1) = ( addreal "**" Fr2) by A1, AFINSQ_2: 45

      .= ( Sum Fr2) by AFINSQ_2: 48;

      hence thesis by AFINSQ_2: 48;

    end;

    definition

      let seq1,seq2 be Real_Sequence;

      :: CATALAN2:def4

      func seq1 (##) seq2 -> Real_Sequence means

      : Def4: for k be Nat holds ex Fr be XFinSequence of REAL st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = (it . k);

      existence

      proof

        defpred P[ object, object] means for k be Nat st k = $1 holds ex Fr st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = $2;

        

         A1: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider k = x as Nat;

          defpred Q[ set, set] means for i st i = $1 holds $2 = ((seq1 . i) * (seq2 . (k -' i)));

          

           A2: for i st i in ( Segm (k + 1)) holds ex z be Element of REAL st Q[i, z]

          proof

            let i such that i in ( Segm (k + 1));

            reconsider ss = ((seq1 . i) * (seq2 . (k -' i))) as Element of REAL ;

            take ss;

            thus thesis;

          end;

          consider Fr such that

           A3: ( dom Fr) = ( Segm (k + 1)) and

           A4: for i st i in ( Segm (k + 1)) holds Q[i, (Fr . i)] from STIRL2_1:sch 5( A2);

          take ( Sum Fr);

          for n be Nat st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n))) by A4;

          hence thesis by A3, XREAL_0:def 1;

        end;

        consider seq3 such that

         A5: for x be object st x in NAT holds P[x, (seq3 . x)] from FUNCT_2:sch 1( A1);

        for k be Nat holds ex Fr st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = (seq3 . k) by ORDINAL1:def 12, A5;

        hence thesis;

      end;

      uniqueness

      proof

        let seq3, seq4 such that

         A6: for k be Nat holds ex Fr be XFinSequence of REAL st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = (seq3 . k) and

         A7: for k be Nat holds ex Fr be XFinSequence of REAL st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = (seq4 . k);

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider k = x as Nat;

          consider Fr1 be XFinSequence of REAL such that

           A8: ( dom Fr1) = (k + 1) and

           A9: for n st n in (k + 1) holds (Fr1 . n) = ((seq1 . n) * (seq2 . (k -' n))) and

           A10: ( Sum Fr1) = (seq3 . k) by A6;

          consider Fr2 be XFinSequence of REAL such that

           A11: ( dom Fr2) = (k + 1) and

           A12: for n st n in (k + 1) holds (Fr2 . n) = ((seq1 . n) * (seq2 . (k -' n))) and

           A13: ( Sum Fr2) = (seq4 . k) by A7;

          now

            let n be Nat such that

             A14: n in ( dom Fr1);

            (Fr1 . n) = ((seq1 . n) * (seq2 . (k -' n))) by A8, A9, A14;

            hence (Fr1 . n) = (Fr2 . n) by A8, A12, A14;

          end;

          hence (seq3 . x) = (seq4 . x) by A8, A10, A11, A13, AFINSQ_1: 8;

        end;

        hence seq3 = seq4 by FUNCT_2: 12;

      end;

      commutativity

      proof

        let seq3, seq1, seq2;

        assume

         A15: for k be Nat holds ex Fr be XFinSequence of REAL st ( dom Fr) = (k + 1) & (for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . (k -' n)))) & ( Sum Fr) = (seq3 . k);

        let k be Nat;

        consider Fr1 be XFinSequence of REAL such that

         A16: ( dom Fr1) = (k + 1) and

         A17: for n st n in (k + 1) holds (Fr1 . n) = ((seq1 . n) * (seq2 . (k -' n))) and

         A18: ( Sum Fr1) = (seq3 . k) by A15;

        defpred Q[ set, set] means for i st i = $1 holds $2 = ((seq2 . i) * (seq1 . (k -' i)));

        reconsider k9 = k as Nat;

        

         A19: for i st i in ( Segm (k9 + 1)) holds ex z be Element of REAL st Q[i, z]

        proof

          let i such that i in ( Segm (k9 + 1));

          reconsider ss = ((seq2 . i) * (seq1 . (k -' i))) as Element of REAL ;

          take ss;

          thus thesis;

        end;

        consider Fr2 such that

         A20: ( dom Fr2) = ( Segm (k9 + 1)) and

         A21: for i st i in ( Segm (k9 + 1)) holds Q[i, (Fr2 . i)] from STIRL2_1:sch 5( A19);

        take Fr2;

        thus ( dom Fr2) = (k + 1) & for n st n in (k + 1) holds (Fr2 . n) = ((seq2 . n) * (seq1 . (k -' n))) by A20, A21;

        now

          let n such that

           A22: n in ( len Fr1);

          

           A23: n < (k + 1) by A16, A22, AFINSQ_1: 86;

          then n <= k by NAT_1: 13;

          then

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

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

          then

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

          (n + 1) <= ( len Fr2) by A20, A23, NAT_1: 13;

          then

           A26: (( len Fr2) -' (n + 1)) = ((k + 1) - (n + 1)) by A20, XREAL_1: 233;

          (k - n) <= k & k < (k + 1) by NAT_1: 13, XREAL_1: 43;

          then (k - n) < (k + 1) by XXREAL_0: 2;

          then (( len Fr2) -' (n + 1)) in ( Segm (k + 1)) by A26, NAT_1: 44;

          then (Fr2 . (( len Fr2) -' (n + 1))) = ((seq2 . (k -' n)) * (seq1 . n)) by A21, A26, A24, A25;

          hence (Fr1 . n) = (Fr2 . (( len Fr1) -' (1 + n))) by A16, A17, A20, A22;

        end;

        hence thesis by A16, A18, A20, Lm4;

      end;

    end

    theorem :: CATALAN2:43

    for Fr1, Fr2 st ( dom Fr1) = ( dom Fr2) & for n st n in ( len Fr1) holds (Fr1 . n) = (Fr2 . (( len Fr1) -' (1 + n))) holds ( Sum Fr1) = ( Sum Fr2) by Lm4;

    theorem :: CATALAN2:44

    

     Th44: for Fr1, Fr2 st ( dom Fr1) = ( dom Fr2) & for n st n in ( len Fr1) holds (Fr1 . n) = (r * (Fr2 . n)) holds ( Sum Fr1) = (r * ( Sum Fr2))

    proof

      let Fr1, Fr2 such that

       A1: ( dom Fr1) = ( dom Fr2) and

       A2: for n st n in ( len Fr1) holds (Fr1 . n) = (r * (Fr2 . n));

      

       A3: (Fr1 | ( dom Fr1)) = Fr1 & (Fr2 | ( dom Fr1)) = Fr2 by A1;

      defpred P[ Nat] means $1 <= ( len Fr1) implies ( Sum (Fr1 | $1)) = (r * ( Sum (Fr2 | $1)));

      

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

      proof

        let i such that

         A5: P[i];

        assume

         A6: (i + 1) <= ( len Fr1);

        then i < ( len Fr1) by NAT_1: 13;

        then

         A7: i in ( len Fr1) by AFINSQ_1: 86;

        then

         A8: (Fr1 . i) = (r * (Fr2 . i)) by A2;

        ( Sum (Fr1 | (i + 1))) = ((Fr1 . i) + ( Sum (Fr1 | i))) & ( Sum (Fr2 | (i + 1))) = ((Fr2 . i) + ( Sum (Fr2 | i))) by A1, A7, AFINSQ_2: 65;

        hence thesis by A5, A6, A8, NAT_1: 13;

      end;

      

       A9: P[ 0 ];

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

      hence thesis by A3;

    end;

    theorem :: CATALAN2:45

    (seq1 (##) (r (#) seq2)) = (r (#) (seq1 (##) seq2))

    proof

      set RS = (r (#) seq2);

      set S = (seq1 (##) seq2);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider k = x as Nat;

        consider Fr1 such that

         A1: ( dom Fr1) = (k + 1) and

         A2: for n st n in (k + 1) holds (Fr1 . n) = ((seq1 . n) * (RS . (k -' n))) and

         A3: ( Sum Fr1) = ((seq1 (##) RS) . k) by Def4;

        consider Fr2 such that

         A4: ( dom Fr2) = (k + 1) and

         A5: for n st n in (k + 1) holds (Fr2 . n) = ((seq1 . n) * (seq2 . (k -' n))) and

         A6: ( Sum Fr2) = (S . k) by Def4;

        now

          let n;

          assume n in ( len Fr1);

          then

           A7: (Fr1 . n) = ((seq1 . n) * (RS . (k -' n))) & (Fr2 . n) = ((seq1 . n) * (seq2 . (k -' n))) by A1, A2, A5;

          (RS . (k -' n)) = (r * (seq2 . (k -' n))) by SEQ_1: 9;

          hence (Fr1 . n) = (r * (Fr2 . n)) by A7;

        end;

        then ( Sum Fr1) = (r * ( Sum Fr2)) by A1, A4, Th44;

        hence ((seq1 (##) RS) . x) = ((r (#) S) . x) by A3, A6, SEQ_1: 9;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: CATALAN2:46

    (seq1 (##) (seq2 + seq3)) = ((seq1 (##) seq2) + (seq1 (##) seq3))

    proof

      set S = (seq2 + seq3);

      set S2 = (seq1 (##) seq2);

      set S3 = (seq1 (##) seq3);

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider k = x as Nat;

        consider Fr be XFinSequence of REAL such that

         A1: ( dom Fr) = (k + 1) and

         A2: for n st n in (k + 1) holds (Fr . n) = ((seq1 . n) * (S . (k -' n))) and

         A3: ( Sum Fr) = ((seq1 (##) S) . k) by Def4;

        consider Fr1 be XFinSequence of REAL such that

         A4: ( dom Fr1) = (k + 1) and

         A5: for n st n in (k + 1) holds (Fr1 . n) = ((seq1 . n) * (seq2 . (k -' n))) and

         A6: ( Sum Fr1) = (S2 . k) by Def4;

        

         A7: ( len Fr1) = ( len Fr) by A1, A4;

        consider Fr2 be XFinSequence of REAL such that

         A8: ( dom Fr2) = (k + 1) and

         A9: for n st n in (k + 1) holds (Fr2 . n) = ((seq1 . n) * (seq3 . (k -' n))) and

         A10: ( Sum Fr2) = (S3 . k) by Def4;

        

         A11: for n be Nat st n in ( dom Fr) holds (Fr . n) = ( addreal . ((Fr1 . n),(Fr2 . n)))

        proof

          let n be Nat such that

           A12: n in ( dom Fr);

          

           A13: (Fr . n) = ((seq1 . n) * (S . (k -' n))) by A1, A2, A12;

          

           A14: (S . (k -' n)) = ((seq2 . (k -' n)) + (seq3 . (k -' n))) by SEQ_1: 7;

          (Fr1 . n) = ((seq1 . n) * (seq2 . (k -' n))) & (Fr2 . n) = ((seq1 . n) * (seq3 . (k -' n))) by A1, A5, A9, A12;

          then (Fr . n) = ((Fr1 . n) + (Fr2 . n)) by A13, A14;

          hence thesis by BINOP_2:def 9;

        end;

        ( len Fr1) = ( len Fr2) by A4, A8;

        then ( addreal "**" (Fr1 ^ Fr2)) = ( addreal "**" Fr) by A11, A7, AFINSQ_2: 46;

        then ( Sum Fr) = ( addreal "**" (Fr1 ^ Fr2)) by AFINSQ_2: 48;

        then ( Sum Fr) = ( Sum (Fr1 ^ Fr2)) by AFINSQ_2: 48;

        then ( Sum Fr) = (( Sum Fr1) + ( Sum Fr2)) by AFINSQ_2: 55;

        hence ((seq1 (##) S) . x) = ((S2 + S3) . x) by A3, A6, A10, SEQ_1: 7;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: CATALAN2:47

    

     Th47: ((seq1 (##) seq2) . 0 ) = ((seq1 . 0 ) * (seq2 . 0 ))

    proof

      set S = ((seq1 . 0 ) * (seq2 . 0 ));

      consider Fr such that

       A1: ( dom Fr) = ( 0 qua Nat + 1) and

       A2: for n st n in ( 0 qua Nat + 1) holds (Fr . n) = ((seq1 . n) * (seq2 . ( 0 -' n))) and

       A3: ( Sum Fr) = ((seq1 (##) seq2) . 0 ) by Def4;

      

       A4: ( 0 -' 0 ) = 0 & ( len Fr) = 1 by A1, XREAL_1: 232;

       0 in ( Segm 1) by NAT_1: 44;

      then (Fr . 0 ) = ((seq1 . 0 ) * (seq2 . ( 0 -' 0 ))) by A2;

      then Fr = <%S%> by A4, AFINSQ_1: 34;

      hence thesis by A3, AFINSQ_2: 53;

    end;

    reconsider zz = 0 as Nat;

    theorem :: CATALAN2:48

    

     Th48: for seq1, seq2, n holds ex Fr st (( Partial_Sums (seq1 (##) seq2)) . n) = ( Sum Fr) & ( dom Fr) = (n + 1) & for i st i in (n + 1) holds (Fr . i) = ((seq1 . i) * (( Partial_Sums seq2) . (n -' i)))

    proof

      let seq1, seq2, n;

      set S = (seq1 (##) seq2);

      set P = ( Partial_Sums seq2);

      defpred P[ Nat] means ex Fr st (( Partial_Sums S) . $1) = ( Sum Fr) & ( dom Fr) = ($1 + 1) & for i st i in ($1 + 1) holds (Fr . i) = ((seq1 . i) * (P . ($1 -' i)));

      

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

      proof

        set A = addreal ;

        let n;

        set n1 = (n + 1);

        defpred Q[ set, set] means for i st i = $1 holds $2 = ((seq1 . i) * (P . (n1 -' i)));

        

         A2: (n1 -' n1) = 0 & (P . 0 ) = (seq2 . 0 ) by SERIES_1:def 1, XREAL_1: 232;

        

         A3: for i st i in ( Segm (n1 + 1)) holds ex x be Element of REAL st Q[i, x]

        proof

          let i such that i in ( Segm (n1 + 1));

          reconsider ss = ((seq1 . i) * (( Partial_Sums seq2) . (n1 -' i))) as Element of REAL ;

          take ss;

          thus thesis;

        end;

        consider Fr2 such that

         A4: ( dom Fr2) = ( Segm (n1 + 1)) and

         A5: for i st i in ( Segm (n1 + 1)) holds Q[i, (Fr2 . i)] from STIRL2_1:sch 5( A3);

        assume P[n];

        then

        consider Fr such that

         A6: (( Partial_Sums S) . n) = ( Sum Fr) and

         A7: ( dom Fr) = n1 and

         A8: for i st i in (n + 1) holds (Fr . i) = ((seq1 . i) * (P . (n -' i)));

        consider Fr1 such that

         A9: ( dom Fr1) = (n1 + 1) and

         A10: for i st i in (n1 + 1) holds (Fr1 . i) = ((seq1 . i) * (seq2 . (n1 -' i))) and

         A11: ( Sum Fr1) = (S . n1) by Def4;

        

         A12: (Fr1 | (n1 + 1)) = Fr1 by A9;

        

         A13: for i be Nat st i in ( dom (Fr2 | n1)) holds ((Fr2 | n1) . i) = ( addreal . ((Fr . i),((Fr1 | n1) . i)))

        proof

          let i be Nat such that

           A14: i in ( dom (Fr2 | n1));

          

           A15: i in (( dom Fr2) /\ n1) by A14, RELAT_1: 61;

          then i in ( dom (Fr1 | n1)) by A9, A4, RELAT_1: 61;

          then

           A16: (Fr1 . i) = ((Fr1 | n1) . i) by FUNCT_1: 47;

          

           A17: i in ( Segm n1) by A15, XBOOLE_0:def 4;

          then

           A18: i < n1 by NAT_1: 44;

          then i <= n by NAT_1: 13;

          then

           A19: (n -' i) = (n - i) by XREAL_1: 233;

          i in (n1 + 1) & i in NAT by A4, A15, XBOOLE_0:def 4;

          then

           A20: (Fr1 . i) = ((seq1 . i) * (seq2 . (n1 -' i))) & (Fr2 . i) = ((seq1 . i) * (P . (n1 -' i))) by A10, A5;

          

           A21: (Fr2 . i) = ((Fr2 | n1) . i) by A14, FUNCT_1: 47;

          (n1 -' i) = (n1 - i) by A18, XREAL_1: 233;

          then ((n -' i) + 1) = (n1 -' i) by A19;

          then

           A22: (P . (n1 -' i)) = ((P . (n -' i)) + (seq2 . (n1 -' i))) by SERIES_1:def 1;

          (Fr . i) = ((seq1 . i) * (P . (n -' i))) by A8, A17;

          then (Fr2 . i) = ((Fr . i) + (Fr1 . i)) by A20, A22;

          hence thesis by A16, A21, BINOP_2:def 9;

        end;

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

        then

         A23: ( Segm n1) c= ( Segm (n1 + 1)) by NAT_1: 39;

        then

         A24: ( len (Fr1 | n1)) = ( len Fr) by A7, A9, RELAT_1: 62;

        n1 < (n1 + 1) by NAT_1: 13;

        then

         A25: n1 in ( Segm (n1 + 1)) by NAT_1: 44;

        then

         A26: (Fr1 . n1) = ((seq1 . n1) * (seq2 . (n1 -' n1))) & ( Sum (Fr1 | (n1 + 1))) = ((Fr1 . n1) + ( Sum (Fr1 | n1))) by A9, A10, AFINSQ_2: 65;

        ( len (Fr2 | n1)) = ( len Fr) by A7, A4, A23, RELAT_1: 62;

        

        then (A "**" (Fr2 | n1)) = (A "**" (Fr ^ (Fr1 | n1))) by A13, A24, AFINSQ_2: 46

        .= ( Sum (Fr ^ (Fr1 | n1))) by AFINSQ_2: 48

        .= (( Sum Fr) + ( Sum (Fr1 | n1))) by AFINSQ_2: 55;

        then

         A27: ( Sum (Fr2 | n1)) = (( Sum Fr) + ( Sum (Fr1 | n1))) by AFINSQ_2: 48;

        take Fr2;

        (Fr2 . n1) = ((seq1 . n1) * (P . (n1 -' n1))) & ( Sum (Fr2 | (n1 + 1))) = ((Fr2 . n1) + ( Sum (Fr2 | n1))) by A4, A5, A25, AFINSQ_2: 65;

        then ( Sum Fr2) = ((( Partial_Sums S) . n) + (S . n1)) & n in NAT & n1 in NAT by A6, A11, A4, A27, A2, A26, A12, ORDINAL1:def 12;

        hence thesis by A4, A5, SERIES_1:def 1;

      end;

      

       A28: P[ 0 ]

      proof

        reconsider rr = ((seq1 . 0 ) * (seq2 . 0 )) as Element of REAL ;

        set Fr = (1 --> rr);

        reconsider Fr as XFinSequence of REAL ;

        take Fr;

        

         A29: ( dom Fr) = 1;

        

         A30: ( Sum (Fr | zz)) = 0 ;

        

         A31: 0 in ( Segm 1) by NAT_1: 44;

        then

         A32: (Fr . zz) = ((seq1 . 0 ) * (seq2 . 0 )) by FUNCOP_1: 7;

        

         A33: (( Sum (Fr | zz)) + (Fr . zz)) = ( Sum (Fr | (zz + 1))) by A29, A31, AFINSQ_2: 65;

        ( Sum Fr) = ( Sum (Fr | ( 0 qua Nat + 1)))

        .= (( Sum (Fr | zz)) + (Fr . zz)) by A33

        .= (Fr . zz) by A30

        .= (S . 0 ) by Th47, A32;

        hence (( Partial_Sums S) . 0 ) = ( Sum Fr) & ( dom Fr) = ( 0 qua Nat + 1) by SERIES_1:def 1;

        let i such that

         A34: i in ( 0 qua Nat + 1);

        i in ( Segm 1) by A34;

        then i < 1 by NAT_1: 44;

        then

         A35: i = 0 by NAT_1: 14;

        then ( 0 -' i) = 0 by XREAL_1: 232;

        then (P . ( 0 -' i)) = (seq2 . 0 ) by SERIES_1:def 1;

        hence thesis by A34, A35, FUNCOP_1: 7;

      end;

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

      hence thesis;

    end;

    theorem :: CATALAN2:49

    

     Th49: for seq1, seq2, n st seq2 is summable holds ex Fr st (( Partial_Sums (seq1 (##) seq2)) . n) = ((( Sum seq2) * (( Partial_Sums seq1) . n)) - ( Sum Fr)) & ( dom Fr) = (n + 1) & for i st i in (n + 1) holds (Fr . i) = ((seq1 . i) * ( Sum (seq2 ^\ ((n -' i) + 1))))

    proof

      let seq1, seq2, n such that

       A1: seq2 is summable;

      defpred Q[ set, set] means for i st i = $1 holds $2 = ((seq1 . i) * ( Sum (seq2 ^\ ((n -' i) + 1))));

      set P2 = ( Partial_Sums seq2);

      set P1 = ( Partial_Sums seq1);

      set S = (seq1 (##) seq2);

      

       A2: for i st i in ( Segm (n + 1)) holds ex x be Element of REAL st Q[i, x]

      proof

        let i such that i in ( Segm (n + 1));

        reconsider ss = ((seq1 . i) * ( Sum (seq2 ^\ ((n -' i) + 1)))) as Element of REAL by XREAL_0:def 1;

        take ss;

        thus thesis;

      end;

      consider Fr such that

       A3: ( dom Fr) = ( Segm (n + 1)) and

       A4: for i st i in ( Segm (n + 1)) holds Q[i, (Fr . i)] from STIRL2_1:sch 5( A2);

      consider Fr1 such that

       A5: (( Partial_Sums S) . n) = ( Sum Fr1) and

       A6: ( dom Fr1) = (n + 1) and

       A7: for i st i in (n + 1) holds (Fr1 . i) = ((seq1 . i) * (P2 . (n -' i))) by Th48;

      

       A8: 0 in ( Segm (n + 1)) by NAT_1: 44;

      then

       A9: (Fr1 . 0 ) = ((seq1 . 0 ) * (P2 . (n -' 0 ))) & ( Sum (Fr1 | (zz + 1))) = ((Fr1 . 0 ) + ( Sum (Fr1 | zz))) by A6, A7, AFINSQ_2: 65;

      defpred P[ Nat] means ($1 + 1) <= (n + 1) implies (( Sum (Fr1 | ($1 + 1))) + ( Sum (Fr | ($1 + 1)))) = (( Sum seq2) * (P1 . $1));

      

       A10: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A11: P[k];

        reconsider k1 = (k + 1) as Nat;

        assume

         A12: ((k + 1) + 1) <= (n + 1);

        then k1 < (n + 1) by NAT_1: 13;

        then

         A13: k1 in ( Segm (n + 1)) by NAT_1: 44;

        then

         A14: (Fr . k1) = ((seq1 . k1) * ( Sum (seq2 ^\ ((n -' k1) + 1)))) & ( Sum (Fr1 | (k1 + 1))) = ((Fr1 . k1) + ( Sum (Fr1 | k1))) by A4, A6, AFINSQ_2: 65;

        

         A15: (( Sum (Fr1 | k1)) + ( Sum (Fr | k1))) = (( Sum seq2) * (P1 . k)) by A12, A11, NAT_1: 13;

        ( Sum (Fr | (k1 + 1))) = ((Fr . k1) + ( Sum (Fr | k1))) & (Fr1 . k1) = ((seq1 . k1) * (P2 . (n -' k1))) by A3, A7, A13, AFINSQ_2: 65;

        

        then (( Sum (Fr | (k1 + 1))) + ( Sum (Fr1 | (k1 + 1)))) = (((seq1 . k1) * (( Sum (seq2 ^\ ((n -' k1) + 1))) + (P2 . (n -' k1)))) + (( Sum seq2) * (P1 . k))) by A15, A14

        .= (((seq1 . k1) * ( Sum seq2)) + (( Sum seq2) * (P1 . k))) by A1, SERIES_1: 15

        .= (( Sum seq2) * ((P1 . k) + (seq1 . k1)))

        .= ((P1 . k1) * ( Sum seq2)) by SERIES_1:def 1;

        hence thesis;

      end;

      

       A16: ( Sum (Fr | zz)) = 0 ;

      

       A17: ( Sum (Fr1 | zz)) = 0 ;

      

       A18: ( Sum (Fr | (zz + 1))) = ((Fr . 0 ) + ( Sum (Fr | zz))) & (Fr . 0 ) = ((seq1 . 0 ) * ( Sum (seq2 ^\ ((n -' 0 ) + 1)))) by A3, A4, A8, AFINSQ_2: 65;

      

      then (( Sum (Fr | (zz + 1))) + ( Sum (Fr1 | (zz + 1)))) = (((Fr . 0 ) + ( Sum (Fr | zz))) + ( Sum (Fr1 | (zz + 1))))

      .= ((Fr . 0 ) + ( Sum (Fr1 | (zz + 1)))) by A16

      .= (((seq1 . 0 ) * ( Sum (seq2 ^\ ((n -' 0 ) + 1)))) + ( Sum (Fr1 | (zz + 1)))) by A18

      .= ((((seq1 . 0 ) * ( Sum (seq2 ^\ ((n -' 0 ) + 1)))) + (Fr1 . 0 )) + ( Sum (Fr1 | zz))) by A9

      .= ((((seq1 . 0 ) * ( Sum (seq2 ^\ ((n -' 0 ) + 1)))) + ((seq1 . 0 ) * (P2 . (n -' 0 )))) + ( Sum (Fr1 | zz))) by A9

      .= ((seq1 . 0 ) * (( Sum (seq2 ^\ ((n -' 0 ) + 1))) + (P2 . (n -' 0 )))) by A17

      .= ((seq1 . 0 ) * ( Sum seq2)) by A1, SERIES_1: 15;

      then

       A19: P[ 0 ] by SERIES_1:def 1;

      

       A20: for k holds P[k] from NAT_1:sch 2( A19, A10);

      take Fr;

      

       A21: (Fr1 | (n + 1)) = Fr1 by A6;

      (Fr | (n + 1)) = Fr by A3;

      then (( Sum Fr1) + ( Sum Fr)) = (( Sum seq2) * (P1 . n)) by A20, A21;

      hence thesis by A3, A4, A5;

    end;

    theorem :: CATALAN2:50

    

     Th50: for Fr holds ex absFr be XFinSequence of REAL st ( dom absFr) = ( dom Fr) & |.( Sum Fr).| <= ( Sum absFr) & for i st i in ( dom absFr) holds (absFr . i) = |.(Fr . i).|

    proof

      let Fr;

      defpred P[ object, object] means $2 = |.(Fr . $1).|;

      

       A1: for i st i in ( Segm ( len Fr)) holds ex x be Element of REAL st P[i, x]

      proof

        let i;

        assume i in ( Segm ( len Fr));

        consider x be Real such that

         A2: P[i, x];

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

         P[i, x] by A2;

        hence thesis;

      end;

      consider absFr be XFinSequence of REAL such that

       A3: ( dom absFr) = ( Segm ( len Fr)) and

       A4: for i st i in ( Segm ( len Fr)) holds P[i, (absFr . i)] from STIRL2_1:sch 5( A1);

      defpred Q[ Nat] means $1 <= ( len Fr) implies |.( Sum (Fr | $1)).| <= ( Sum (absFr | $1));

      

       A5: for i st Q[i] holds Q[(i + 1)]

      proof

        let i such that

         A6: Q[i];

        set i1 = (i + 1);

        assume

         A7: i1 <= ( len Fr);

        then i < ( len Fr) by NAT_1: 13;

        then

         A8: i in ( dom Fr) by AFINSQ_1: 86;

        then ( Sum (Fr | i1)) = ((Fr . i) + ( Sum (Fr | i))) & (absFr . i) = |.(Fr . i).| by A4, AFINSQ_2: 65;

        then

         A9: |.( Sum (Fr | i1)).| <= ((absFr . i) + |.( Sum (Fr | i)).|) by COMPLEX1: 56;

        ( Sum (absFr | i1)) = ((absFr . i) + ( Sum (absFr | i))) by A3, A8, AFINSQ_2: 65;

        then ((absFr . i) + |.( Sum (Fr | i)).|) <= ( Sum (absFr | i1)) by A6, A7, NAT_1: 13, XREAL_1: 7;

        hence thesis by A9, XXREAL_0: 2;

      end;

      take absFr;

      

       A10: Q[ 0 ] by COMPLEX1: 44;

      for i holds Q[i] from NAT_1:sch 2( A10, A5);

      then |.( Sum (Fr | ( len Fr))).| <= ( Sum (absFr | ( len Fr)));

      hence thesis by A3, A4;

    end;

    theorem :: CATALAN2:51

    

     Th51: for seq1 st seq1 is summable holds ex r st 0 < r & for k holds |.( Sum (seq1 ^\ k)).| < r

    proof

      let seq1 such that

       A1: seq1 is summable;

      defpred P[ Nat] means ex r st r >= 0 & for i st i <= $1 holds |.( Sum (seq1 ^\ i)).| <= r;

      

       A2: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume P[k];

        then

        consider r such that

         A3: r >= 0 and

         A4: for i st i <= k holds |.( Sum (seq1 ^\ i)).| <= r;

        take M = ( max (r, |.( Sum (seq1 ^\ (k + 1))).|));

        thus M >= 0 by A3, XXREAL_0: 25;

        let i such that

         A5: i <= (k + 1);

        now

          per cases by A5, NAT_1: 8;

            suppose i = (k + 1);

            hence thesis by XXREAL_0: 25;

          end;

            suppose

             A6: i <= k;

            

             A7: r <= M by XXREAL_0: 25;

             |.( Sum (seq1 ^\ i)).| <= r by A4, A6;

            hence thesis by A7, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

      set P = ( Partial_Sums seq1);

      

       A8: ( lim P) = ( Sum seq1) by SERIES_1:def 3;

      P is convergent by A1, SERIES_1:def 2;

      then

      consider n be Nat such that

       A9: for m be Nat st n <= m holds |.((P . m) - ( Sum seq1)).| < 1 by A8, SEQ_2:def 7;

      

       A10: P[ 0 ]

      proof

        take |.( Sum seq1).|;

        thus |.( Sum seq1).| >= 0 by COMPLEX1: 46;

        let i;

        assume i <= 0 ;

        then i = 0 ;

        hence thesis by NAT_1: 47;

      end;

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

      then

      consider r such that

       A11: r >= 0 and

       A12: for i st i <= n holds |.( Sum (seq1 ^\ i)).| <= r;

      take r1 = (r + 1);

      thus r1 > 0 by A11;

      let k;

      now

        per cases ;

          suppose

           A13: k <= n;

          

           A14: ( 0 qua Nat + r) < r1 by XREAL_1: 8;

           |.( Sum (seq1 ^\ k)).| <= r by A12, A13;

          hence thesis by A14, XXREAL_0: 2;

        end;

          suppose

           A15: k > n;

          then

          reconsider k1 = (k - 1) as Nat by NAT_1: 20;

          (k1 + 1) > n by A15;

          then k1 >= n by NAT_1: 13;

          then

           A16: |.((P . k1) - ( Sum seq1)).| < 1 by A9;

          ( Sum seq1) = ((P . k1) + ( Sum (seq1 ^\ (k1 + 1)))) by A1, SERIES_1: 15;

          then |.( - ( Sum (seq1 ^\ (k1 + 1)))).| < 1 by A16;

          then

           A17: |.( Sum (seq1 ^\ (k1 + 1))).| < 1 by COMPLEX1: 52;

          (1 + 0 qua Nat) <= r1 by A11, XREAL_1: 6;

          hence thesis by A17, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: CATALAN2:52

    

     Th52: for seq1, n, m st n <= m & for i holds (seq1 . i) >= 0 holds (( Partial_Sums seq1) . n) <= (( Partial_Sums seq1) . m)

    proof

      let seq1, n, m such that

       A1: n <= m and

       A2: for i holds (seq1 . i) >= 0 ;

      set S = ( Partial_Sums seq1);

      defpred P[ Nat] means (S . n) <= (S . (n + $1));

      

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

      proof

        let i such that

         A4: P[i];

        set ni = (n + i);

        (S . (ni + 1)) = ((S . ni) + (seq1 . (ni + 1))) & (seq1 . (ni + 1)) >= 0 by A2, SERIES_1:def 1;

        then (S . (ni + 1)) >= ((S . ni) + 0 qua Nat) by XREAL_1: 6;

        hence thesis by A4, XXREAL_0: 2;

      end;

      

       A5: P[ 0 ];

      

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

      reconsider m9 = m, n9 = n as Nat;

      

       A7: (n9 + (m9 - n9)) = m9;

      (m9 - n9) is Nat by A1, NAT_1: 21;

      hence thesis by A6, A7;

    end;

    theorem :: CATALAN2:53

    

     Th53: for seq1, seq2 st seq1 is absolutely_summable & seq2 is summable holds (seq1 (##) seq2) is summable & ( Sum (seq1 (##) seq2)) = (( Sum seq1) * ( Sum seq2))

    proof

      let seq1, seq2 such that

       A1: seq1 is absolutely_summable and

       A2: seq2 is summable;

      set S2 = ( Sum seq2);

      set S1 = ( Sum seq1);

      set PA = ( Partial_Sums |.seq1.|);

      set P2 = ( Partial_Sums seq2);

      set P1 = ( Partial_Sums seq1);

      set S = (seq1 (##) seq2);

      set P = ( Partial_Sums S);

      

       A3: for e st 0 < e holds ex n be Nat st for m be Nat st n <= m holds |.((P . m) - (S1 * S2)).| < e

      proof

        seq1 is summable by A1;

        then

         A4: P1 is convergent by SERIES_1:def 2;

        let e such that

         A5: 0 < e;

        set e1 = (e / (3 * ( |.S2.| + 1)));

        ( |.S2.| + 1) > ( 0 qua Nat + 0 qua Nat) by COMPLEX1: 46, XREAL_1: 8;

        then

         A6: (3 * ( |.S2.| + 1)) > (3 * 0 ) by XREAL_1: 68;

        then ( lim P1) = S1 & e1 > 0 by A5, SERIES_1:def 3, XREAL_1: 139;

        then

        consider n0 be Nat such that

         A7: for n be Nat st n0 <= n holds |.((P1 . n) - S1).| < e1 by A4, SEQ_2:def 7;

        set e3 = (e / (3 * (( Sum ( abs seq1)) + 1)));

        ( |.S2.| + 1) > ( 0 qua Nat + 0 qua Nat) by COMPLEX1: 46, XREAL_1: 8;

        then

         A8: (e1 * ( |.S2.| + 1)) = (e / 3) by XCMPLX_1: 92;

        

         A9: P2 is convergent & ( lim P2) = S2 by A2, SERIES_1:def 2, SERIES_1:def 3;

        consider r such that

         A10: 0 < r and

         A11: for k holds |.( Sum (seq2 ^\ k)).| < r by A2, Th51;

        set e2 = (e / (3 * r));

        

         A12: ( |.S2.| + 1) > ( |.S2.| + 0 qua Nat) by XREAL_1: 8;

         A13:

        now

          let n;

           |.(seq1 . n).| = (( abs seq1) . n) by SEQ_1: 12;

          hence (( abs seq1) . n) >= 0 by COMPLEX1: 46;

        end;

        then

         A14: for n be Nat holds ( |.seq1.| . n) >= 0 ;

        

         A15: ( abs seq1) is summable by A1, SERIES_1:def 4;

        then ( Sum ( abs seq1)) >= 0 by A14, SERIES_1: 18;

        then

         A16: ((( Sum ( abs seq1)) + 1) * e3) = (e / 3) by XCMPLX_1: 92;

        

         A17: ( Sum ( abs seq1)) >= 0 by A15, A14, SERIES_1: 18;

        then (3 * (( Sum ( abs seq1)) + 1)) > ( 0 * 3) by XREAL_1: 68;

        then e3 > 0 by A5, XREAL_1: 139;

        then

        consider n2 be Nat such that

         A18: for n be Nat st n2 <= n holds |.((P2 . n) - S2).| < e3 by A9, SEQ_2:def 7;

        (3 * r) > ( 0 * 3) by A10, XREAL_1: 68;

        then e2 > 0 by A5, XREAL_1: 139;

        then

        consider n1 be Nat such that

         A19: for n be Nat st n1 <= n holds |.((PA . n) - (PA . n1)).| < e2 by A15, SERIES_1: 21;

        reconsider M = ( max (( max (1,n0)),( max ((n1 + 1),n2)))) as Nat by TARSKI: 1;

        

         A20: ( max ((n1 + 1),n2)) <= M by XXREAL_0: 25;

        take 2M = (M * 2);

        let m be Nat such that

         A21: 2M <= m;

        

         A22: ( max (1,n0)) <= M by XXREAL_0: 25;

        then 0 < M by XXREAL_0: 25;

        then

        reconsider M1 = (M - 1) as Nat by NAT_1: 20;

        

         A23: M = (M1 + 1);

        

         A24: (n1 + 1) <= ( max ((n1 + 1),n2)) by XXREAL_0: 25;

        then (M1 + 1) >= (n1 + 1) by A20, XXREAL_0: 2;

        then M1 >= n1 by XREAL_1: 8;

        then (PA . M1) >= (PA . n1) by A13, Th52;

        then ((PA . m) - (PA . M1)) <= ((PA . m) - (PA . n1)) by XREAL_1: 10;

        then

         A25: (r * ((PA . m) - (PA . M1))) <= (r * ((PA . m) - (PA . n1))) by A10, XREAL_1: 64;

        consider Fr such that

         A26: (P . m) = ((S2 * (P1 . m)) - ( Sum Fr)) and

         A27: ( dom Fr) = (m + 1) and

         A28: for i st i in (m + 1) holds (Fr . i) = ((seq1 . i) * ( Sum (seq2 ^\ ((m -' i) + 1)))) by A2, Th49;

        consider absFr be XFinSequence of REAL such that

         A29: ( dom absFr) = ( dom Fr) and

         A30: |.( Sum Fr).| <= ( Sum absFr) and

         A31: for i st i in ( dom absFr) holds (absFr . i) = |.(Fr . i).| by Th50;

        

         A32: M <= (M + M) by NAT_1: 11;

        then

         A33: M <= m by A21, XXREAL_0: 2;

        then M < ( len absFr) by A27, A29, NAT_1: 13;

        then

         A34: ( len (absFr | M)) = M by AFINSQ_1: 11;

        (n1 + 1) <= M by A24, A20, XXREAL_0: 2;

        then (n1 + 1) <= m by A33, XXREAL_0: 2;

        then

         A35: n1 <= m by NAT_1: 13;

        then (PA . m) >= (PA . n1) by A13, Th52;

        then ((PA . m) - (PA . n1)) >= ((PA . n1) - (PA . n1)) by XREAL_1: 9;

        then

         A36: |.((PA . m) - (PA . n1)).| = ((PA . m) - (PA . n1)) by ABSVALUE:def 1;

        consider Fr1 such that

         A37: absFr = ((absFr | M) ^ Fr1) by Th1;

        

         A38: (m + 1) = (( len (absFr | M)) + ( len Fr1)) by A27, A29, A37, AFINSQ_1:def 3;

        then

         A39: (Fr1 | ((m - M) + 1)) = Fr1 by A34;

        

         A40: n2 <= ( max ((n1 + 1),n2)) by XXREAL_0: 25;

        then n2 <= M by A20, XXREAL_0: 2;

        then n2 <= 2M by A32, XXREAL_0: 2;

        then n2 <= m & m in NAT by A21, XXREAL_0: 2, ORDINAL1:def 12;

        then

         A41: |.((P2 . m) - S2).| < e3 by A18;

        defpred S[ Nat] means ((M + $1) + 1) <= (m + 1) implies ( Sum (Fr1 | ($1 + 1))) <= (r * ((PA . (M + $1)) - (PA . M1)));

        

         A42: for k st S[k] holds S[(k + 1)]

        proof

          let k such that

           A43: S[k];

          set k1 = (k + 1);

          set Mk1 = (M + k1);

          reconsider Mk = (M + k) as Nat;

          

           A44: |.(seq1 . Mk1).| = (( abs seq1) . Mk1) by SEQ_1: 12;

          assume

           A45: (Mk1 + 1) <= (m + 1);

          then

           A46: Mk1 < (m + 1) by NAT_1: 13;

          then

           A47: Mk1 in ( Segm (m + 1)) by NAT_1: 44;

          then (Fr . Mk1) = ((seq1 . Mk1) * ( Sum (seq2 ^\ ((m -' Mk1) + 1)))) by A28;

          then

           A48: |.(Fr . Mk1).| = ( |.(seq1 . Mk1).| * |.( Sum (seq2 ^\ ((m -' Mk1) + 1))).|) by COMPLEX1: 65;

          Mk1 < (m + 1) by A45, NAT_1: 13;

          then k1 < ( len Fr1) by A38, A34, XREAL_1: 7;

          then k1 in ( len Fr1) by AFINSQ_1: 86;

          then

           A49: ( Sum (Fr1 | (k1 + 1))) = ((Fr1 . k1) + ( Sum (Fr1 | k1))) by AFINSQ_2: 65;

          (m + 1) = ( len absFr) by A27, A29;

          then (absFr . Mk1) = (Fr1 . (Mk1 - M)) by A37, A34, A46, AFINSQ_1: 19, NAT_1: 11;

          then

           A50: (Fr1 . k1) = |.(Fr . Mk1).| by A27, A29, A31, A47;

          

           A51: (( |.seq1.| . (Mk + 1)) + (PA . Mk)) = (PA . (Mk + 1)) by SERIES_1:def 1;

           |.(seq1 . Mk1).| >= 0 & |.( Sum (seq2 ^\ ((m -' Mk1) + 1))).| < r by A11, COMPLEX1: 46;

          then (Fr1 . k1) <= (r * |.(seq1 . Mk1).|) by A50, A48, XREAL_1: 64;

          then ( Sum (Fr1 | (k1 + 1))) <= ((r * ( |.seq1.| . Mk1)) + (r * ((PA . (M + k)) - (PA . M1)))) by A43, A45, A49, A44, NAT_1: 13, XREAL_1: 7;

          then ( Sum (Fr1 | (k1 + 1))) <= (r * ((( |.seq1.| . Mk1) + (PA . (M + k))) - (PA . M1)));

          then ( Sum (Fr1 | (k1 + 1))) <= (r * ((PA . ((M + k) + 1)) - (PA . M1))) by A51;

          hence thesis;

        end;

         |.((PA . m) - (PA . n1)).| < e2 by A19, A35;

        then (r * ((PA . m) - (PA . n1))) <= (r * e2) by A10, A36, XREAL_1: 64;

        then

         A52: (r * ((PA . m) - (PA . M1))) <= (r * e2) by A25, XXREAL_0: 2;

        

         A53: m = (M + (m - M)) & (m - M) = (m -' M) by A21, A32, XREAL_1: 233, XXREAL_0: 2;

        

         A54: S[ 0 ]

        proof

          assume

           A55: ((M + 0 qua Nat) + 1) <= (m + 1);

          then

           A56: M < (m + 1) by NAT_1: 13;

          then

           A57: M in ( Segm (m + 1)) by NAT_1: 44;

          then

           A58: (Fr . M) = ((seq1 . M) * ( Sum (seq2 ^\ ((m -' M) + 1)))) by A28;

          ((M + 1) - M) <= ((m + 1) - M) by A55, XREAL_1: 9;

          then ( Segm 1) c= ( Segm ( len Fr1)) by A38, A34, NAT_1: 39;

          then

           A59: ( dom (Fr1 | 1)) = 1 by RELAT_1: 62;

          (m + 1) = ( len absFr) by A27, A29;

          then (absFr . M) = (Fr1 . (M - M)) by A37, A34, A56, AFINSQ_1: 19;

          then (Fr1 . 0 ) = |.(Fr . M).| by A27, A29, A31, A57;

          then

           A60: (Fr1 . 0 ) = ( |.(seq1 . M).| * |.( Sum (seq2 ^\ ((m -' M) + 1))).|) by A58, COMPLEX1: 65;

          

           A61: |.(seq1 . M).| >= 0 & r > |.( Sum (seq2 ^\ ((m -' M) + 1))).| by A11, COMPLEX1: 46;

           0 in ( Segm 1) by NAT_1: 44;

          then

           A62: ((Fr1 | 1) . 0 ) = (Fr1 . 0 ) by A59, FUNCT_1: 47;

          ((PA . M1) + ( |.seq1.| . (M1 + 1))) = (PA . (M1 + 1)) by SERIES_1:def 1;

          then

           A63: ((PA . M) - (PA . M1)) = |.(seq1 . M).| by SEQ_1: 12;

          ( Sum (Fr1 | 1)) = ((Fr1 | 1) . 0 ) by A59, Lm3;

          hence thesis by A62, A60, A63, A61, XREAL_1: 64;

        end;

        for k holds S[k] from NAT_1:sch 2( A54, A42);

        then ( Sum Fr1) <= (r * ((PA . m) - (PA . M1))) by A39, A53;

        then ( Sum Fr1) <= (r * e2) by A52, XXREAL_0: 2;

        then

         A64: ( Sum Fr1) <= (e / 3) by A10, XCMPLX_1: 92;

        ( |.seq1.| . 0 ) >= 0 by A13;

        then

         A65: (( |.seq1.| . 0 ) * |.((P2 . m) - S2).|) <= (e3 * ( |.seq1.| . 0 )) by A41, XREAL_1: 64;

        

         A66: 0 in ( Segm (m + 1)) by NAT_1: 44;

        then

         A67: (Fr . 0 ) = ((seq1 . 0 ) * ( Sum (seq2 ^\ ((m -' 0 ) + 1)))) by A28;

        (PA . M1) <= ( Sum |.seq1.|) by A14, A15, RSSPACE2: 3;

        then

         A68: (e3 * (PA . M1)) <= (e3 * ( Sum |.seq1.|)) by A5, A17, XREAL_1: 64;

        S2 = ((P2 . (m -' 0 )) + ( Sum (seq2 ^\ ((m -' 0 ) + 1)))) & (m -' 0 ) = m by A2, NAT_D: 40, SERIES_1: 15;

        then

         A69: ( Sum (seq2 ^\ ((m -' 0 ) + 1))) = (S2 - (P2 . m));

        n0 <= ( max (1,n0)) by XXREAL_0: 25;

        then n0 <= M by A22, XXREAL_0: 2;

        then n0 <= m & m in NAT by A33, XXREAL_0: 2, ORDINAL1:def 12;

        then

         A70: |.((P1 . m) - S1).| < e1 by A7;

         |.(S2 * ((P1 . m) - S1)).| = ( |.S2.| * |.((P1 . m) - S1).|) & |.S2.| >= 0 by COMPLEX1: 46, COMPLEX1: 65;

        then

         A71: |.(S2 * ((P1 . m) - S1)).| <= ( |.S2.| * e1) by A70, XREAL_1: 64;

        

         A72: ( Sum absFr) = (( Sum (absFr | M)) + ( Sum Fr1)) by A37, AFINSQ_2: 55;

        defpred Q[ Nat] means ($1 + 1) <= M implies ( Sum (absFr | ($1 + 1))) <= (e3 * (PA . $1));

        

         A73: n2 <= M by A40, A20, XXREAL_0: 2;

        

         A74: for k st Q[k] holds Q[(k + 1)]

        proof

          let k such that

           A75: Q[k];

          reconsider k1 = (k + 1) as Nat;

          

           A76: |.(seq1 . k1).| = (( abs seq1) . k1) by SEQ_1: 12;

          

           A77: (m - M) >= (2M - M) by A21, XREAL_1: 9;

          assume

           A78: ((k + 1) + 1) <= M;

          then

           A79: k1 < M by NAT_1: 13;

          then (m - k1) >= (m - M) by XREAL_1: 10;

          then (m - k1) >= M by A77, XXREAL_0: 2;

          then

           A80: (m - k1) >= n2 by A73, XXREAL_0: 2;

          ((e3 * |.(seq1 . k1).|) + ( Sum (absFr | k1))) <= ((e3 * |.(seq1 . k1).|) + (e3 * (PA . k))) by A75, A78, NAT_1: 13, XREAL_1: 6;

          then ((e3 * |.(seq1 . k1).|) + ( Sum (absFr | k1))) <= (e3 * ((( abs seq1) . k1) + (PA . k))) & k in NAT by A76, ORDINAL1:def 12;

          then

           A81: ((e3 * |.(seq1 . k1).|) + ( Sum (absFr | k1))) <= (e3 * (PA . k1)) by SERIES_1:def 1;

          k1 < m by A33, A79, XXREAL_0: 2;

          then k1 < (m + 1) by NAT_1: 13;

          then

           A82: k1 in ( Segm (m + 1)) by NAT_1: 44;

          then

           A83: ( Sum (absFr | (k1 + 1))) = ((absFr . k1) + ( Sum (absFr | k1))) by A27, A29, AFINSQ_2: 65;

          (m - k1) = (m -' k1) by A33, A79, XREAL_1: 233, XXREAL_0: 2;

          then |.((P2 . (m -' k1)) - S2).| < e3 by A18, A80;

          then

           A84: |.(S2 - (P2 . (m -' k1))).| < e3 by COMPLEX1: 60;

          

           A85: S2 = ((P2 . (m -' k1)) + ( Sum (seq2 ^\ ((m -' k1) + 1)))) by A2, SERIES_1: 15;

           |.(seq1 . k1).| >= 0 by COMPLEX1: 46;

          then ( |.(S2 - (P2 . (m -' k1))).| * |.(seq1 . k1).|) <= (e3 * |.(seq1 . k1).|) by A84, XREAL_1: 64;

          then

           A86: |.((seq1 . k1) * ( Sum (seq2 ^\ ((m -' k1) + 1)))).| <= (e3 * |.(seq1 . k1).|) by A85, COMPLEX1: 65;

          (Fr . k1) = ((seq1 . k1) * ( Sum (seq2 ^\ ((m -' k1) + 1)))) & |.(Fr . k1).| = (absFr . k1) by A27, A28, A29, A31, A82;

          then ( Sum (absFr | (k1 + 1))) <= ((e3 * |.(seq1 . k1).|) + ( Sum (absFr | k1))) by A83, A86, XREAL_1: 6;

          hence thesis by A81, XXREAL_0: 2;

        end;

        

         A87: ( Sum (absFr | zz)) = 0 ;

        ( Sum (absFr | (zz + 1))) = ((absFr . 0 ) + ( Sum (absFr | zz))) & (absFr . 0 ) = |.(Fr . 0 ).| by A27, A29, A31, A66, AFINSQ_2: 65;

        

        then ( Sum (absFr | (zz + 1))) = ( |.(seq1 . 0 ).| * |.( Sum (seq2 ^\ ((m -' 0 ) + 1))).|) by A67, A87, COMPLEX1: 65

        .= ((( abs seq1) . 0 ) * |.( Sum (seq2 ^\ ((m -' 0 ) + 1))).|) by SEQ_1: 12

        .= ((( abs seq1) . 0 ) * |.((P2 . m) - S2).|) by A69, COMPLEX1: 60;

        then

         A88: Q[ 0 ] by A65, SERIES_1:def 1;

        for k holds Q[k] from NAT_1:sch 2( A88, A74);

        then

         A89: ( Sum (absFr | M)) <= (e3 * (PA . M1)) by A23;

        (( Sum ( abs seq1)) + 1) > (( Sum ( abs seq1)) + 0 qua Nat) by XREAL_1: 8;

        then (e3 * (( Sum ( abs seq1)) + 1)) >= (e3 * ( Sum ( abs seq1))) by A5, A17, XREAL_1: 64;

        then (e3 * (PA . M1)) <= (e / 3) by A68, A16, XXREAL_0: 2;

        then ( Sum (absFr | M)) <= (e / 3) by A89, XXREAL_0: 2;

        then (( Sum (absFr | M)) + ( Sum Fr1)) <= ((e / 3) + (e / 3)) by A64, XREAL_1: 7;

        then

         A90: |.( Sum Fr).| <= ((e / 3) + (e / 3)) by A30, A72, XXREAL_0: 2;

        ((P . m) - (S1 * S2)) = ((S2 * ((P1 . m) - S1)) - ( Sum Fr)) by A26;

        then

         A91: |.((P . m) - (S1 * S2)).| <= ( |.(S2 * ((P1 . m) - S1)).| + |.( Sum Fr).|) by COMPLEX1: 57;

        e1 > 0 by A5, A6, XREAL_1: 139;

        then (e1 * ( |.S2.| + 1)) > (e1 * |.S2.|) by A12, XREAL_1: 68;

        then |.(S2 * ((P1 . m) - S1)).| < (e / 3) by A8, A71, XXREAL_0: 2;

        then ( |.(S2 * ((P1 . m) - S1)).| + |.( Sum Fr).|) < ((e / 3) + ((e / 3) + (e / 3))) by A90, XREAL_1: 8;

        hence thesis by A91, XXREAL_0: 2;

      end;

      then

       A92: P is convergent by SEQ_2:def 6;

      hence S is summable by SERIES_1:def 2;

      ( lim P) = (S1 * S2) by A3, A92, SEQ_2:def 7;

      hence thesis by SERIES_1:def 3;

    end;

    begin

    theorem :: CATALAN2:54

    for r holds ex Catal be Real_Sequence st (for n holds (Catal . n) = (( Catalan (n + 1)) * (r |^ n))) & ( |.r.| < (1 / 4) implies Catal is absolutely_summable & ( Sum Catal) = (1 + (r * (( Sum Catal) |^ 2))) & ( Sum Catal) = (2 / (1 + ( sqrt (1 - (4 * r))))) & (r <> 0 implies ( Sum Catal) = ((1 - ( sqrt (1 - (4 * r)))) / (2 * r))))

    proof

      defpred E[ object, object] means for r st $1 = r holds ex Catal be Real_Sequence st (for n holds (Catal . n) = (( Catalan (n + 1)) * (r |^ n))) & ( |.r.| < (1 / 4) implies Catal is absolutely_summable & ( Sum Catal) = (1 + (r * (( Sum Catal) |^ 2))) & $2 = ( Sum Catal));

      

       A1: for x be object st x in REAL holds ex y be object st y in REAL & E[x, y]

      proof

        let x be object;

        

         A2: |.1.| = 1 by ABSVALUE:def 1;

        assume x in REAL ;

        then

        reconsider r = x as Real;

        set a = (4 * |.r.|);

        deffunc C( Nat) = ( In ((( Catalan ($1 + 1)) * (r |^ $1)), REAL ));

        consider Cat be Real_Sequence such that

         A3: for n be Element of NAT holds (Cat . n) = C(n) from FUNCT_2:sch 4;

        set G = (a GeoSeq );

        defpred P[ Nat] means (( abs Cat) . $1) <= (G . $1);

        

         A4: for n st P[n] holds P[(n + 1)]

        proof

          

           A5: |.r.| >= 0 by COMPLEX1: 46;

          let n;

          assume P[n];

          then

           A6: (a * (( abs Cat) . n)) <= (a * (G . n)) by A5, XREAL_1: 64;

          set n1 = (n + 1);

          

           A7: |.(r |^ n1).| >= 0 & (r |^ n1) = (r * (r |^ n)) by COMPLEX1: 46, NEWTON: 6;

          ( Catalan (n1 + 1)) >= 0 by CATALAN1: 17;

          then

           A8: |.( Catalan (n1 + 1)).| = ( Catalan (n1 + 1)) by ABSVALUE:def 1;

          ( Catalan n1) >= 0 by CATALAN1: 17;

          then |.( Catalan n1).| = ( Catalan n1) by ABSVALUE:def 1;

          then |.( Catalan (n1 + 1)).| < (4 * |.( Catalan n1).|) by A8, CATALAN1: 21;

          then

           A9: ( |.(r |^ n1).| * |.( Catalan (n1 + 1)).|) <= ((4 * |.( Catalan n1).|) * |.(r * (r |^ n)).|) by A7, XREAL_1: 64;

           |.(r * (r |^ n)).| = ( |.r.| * |.(r |^ n).|) by COMPLEX1: 65;

          then |. C(n1).| <= (a * ( |.( Catalan n1).| * |.(r |^ n).|)) by A9, COMPLEX1: 65;

          then |.(Cat . n1).| <= (a * ( |.( Catalan n1).| * |.(r |^ n).|)) by A3;

          then |.(Cat . n1).| <= (a * |. C(n).|) & n in NAT by COMPLEX1: 65, ORDINAL1:def 12;

          then

           A10: |.(Cat . n1).| <= (a * |.(Cat . n).|) by A3;

           |.(Cat . n).| = (( abs Cat) . n) by SEQ_1: 12;

          then (( abs Cat) . n1) <= (a * (( abs Cat) . n)) by A10, SEQ_1: 12;

          then (( abs Cat) . n1) <= (a * (G . n)) by A6, XXREAL_0: 2;

          hence thesis by PREPOWER: 3;

        end;

        (Cat . 0 ) = C(0) by A3;

        then

         A11: (( abs Cat) . 0 ) = |.(r |^ 0 ).| by CATALAN1: 11, SEQ_1: 12;

        (r |^ 0 ) = 1 & (a |^ 0 ) = 1 by NEWTON: 4;

        then

         A12: P[ 0 ] by A11, A2, PREPOWER:def 1;

        for n holds P[n] from NAT_1:sch 2( A12, A4);

        then

         A13: for n be Nat holds P[n];

         A14:

        now

          let n be Nat;

          (( abs Cat) . n) = |.(Cat . n).| by SEQ_1: 12;

          hence (( abs Cat) . n) >= 0 by COMPLEX1: 46;

        end;

        take ( Sum Cat);

        thus ( Sum Cat) in REAL by XREAL_0:def 1;

        let s such that

         A15: x = s;

        for y be object st y in NAT holds ((Cat ^\ 1) . y) = ((Cat (##) (r (#) Cat)) . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider n = y as Nat;

          set n1 = (n + 1);

          consider Fr1 such that

           A16: ( dom Fr1) = n1 and

           A17: for i st i in (n + 1) holds (Fr1 . i) = ((Cat . i) * ((r (#) Cat) . (n -' i))) and

           A18: ( Sum Fr1) = ((Cat (##) (r (#) Cat)) . n) by Def4;

          consider Catal be XFinSequence of NAT such that

           A19: ( Sum Catal) = ( Catalan (n1 + 1)) and

           A20: ( dom Catal) = n1 and

           A21: for j st j < n1 holds (Catal . j) = (( Catalan (j + 1)) * ( Catalan (n1 -' j))) by Th39;

          ( rng Catal) c= REAL by NUMBERS: 19;

          then

          reconsider CatalR = Catal as XFinSequence of REAL by RELAT_1:def 19;

          defpred Q[ set, set] means for k st k = $1 holds $2 = ((r |^ n1) * (Catal . k));

          

           A22: for k st k in ( Segm n1) holds ex x be Element of REAL st Q[k, x]

          proof

            let k such that k in ( Segm n1);

            reconsider rr = ((r |^ n1) * (Catal . k)) as Element of REAL by XREAL_0:def 1;

            take rr;

            thus thesis;

          end;

          consider Fr2 such that

           A23: ( dom Fr2) = ( Segm n1) and

           A24: for k be Nat st k in ( Segm n1) holds Q[k, (Fr2 . k)] from STIRL2_1:sch 5( A22);

           A25:

          now

            let k be Nat such that

             A26: k in ( dom Fr2);

            k < ( len Fr2) by A26, AFINSQ_1: 86;

            then

             A27: k < (n + 1) by A23;

            then

             A28: (n1 -' k) = (n1 - k) by XREAL_1: 233;

            

             A29: n = (k + (n - k));

            k <= n by A27, NAT_1: 13;

            then

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

            

            then (Fr1 . k) = ((Cat . k) * ((r (#) Cat) . (n - k))) by A17, A23, A26

            .= ( C(k) * ((r (#) Cat) . (n - k))) by A26, A3

            .= ((( Catalan (k + 1)) * (r |^ k)) * ((r (#) Cat) . (n - k)))

            .= ((( Catalan (k + 1)) * (r |^ k)) * (r * (Cat . (n - k)))) by A30, SEQ_1: 9

            .= ((( Catalan (k + 1)) * (r |^ k)) * (r * C(-'))) by A3, A30

            .= (((( Catalan (k + 1)) * ( Catalan (n1 -' k))) * r) * ((r |^ k) * (r |^ (n -' k)))) by A30, A28

            .= (((( Catalan (k + 1)) * ( Catalan (n1 -' k))) * r) * (r |^ n)) by A30, A29, NEWTON: 8

            .= (((Catal . k) * r) * (r |^ n)) by A21, A27

            .= ((Catal . k) * (r * (r |^ n)))

            .= ((Catal . k) * (r |^ n1)) by NEWTON: 6

            .= (Fr2 . k) by A23, A24, A26;

            hence (Fr1 . k) = (Fr2 . k);

          end;

          for k st k in ( len Fr2) holds (Fr2 . k) = ((r |^ n1) * (CatalR . k)) by A23, A24;

          

          then ( Sum Fr2) = ((r |^ n1) * ( Sum CatalR)) by A20, A23, Th44

          .= C(n1) by A19

          .= (Cat . n1) by A3

          .= ((Cat ^\ 1) . n) by NAT_1:def 3;

          hence thesis by A16, A18, A23, A25, AFINSQ_1: 8;

        end;

        then

         A31: (Cat ^\ 1) = (Cat (##) (r (#) Cat)) by FUNCT_2: 12;

         |.r.| >= 0 by COMPLEX1: 46;

        then

         A32: |.a.| = a by ABSVALUE:def 1;

        take Cat;

        hereby

          let n;

          n in NAT by ORDINAL1:def 12;

          

          hence (Cat . n) = C(n) by A3

          .= (( Catalan (n + 1)) * (s |^ n)) by A15;

        end;

        

         A33: (r |^ 0 ) = 1 by NEWTON: 4;

        (Cat . 0 ) = C(0) by A3

        .= (( Catalan ( 0 qua Nat + 1)) * (r |^ 0 ));

        then

         A34: (( Partial_Sums Cat) . 0 ) = 1 by A33, CATALAN1: 11, SERIES_1:def 1;

        assume |.s.| < (1 / 4);

        then a < (4 * (1 / 4)) by A15, XREAL_1: 68;

        then G is summable by A32, SERIES_1: 24;

        then ( abs Cat) is summable by A14, A13, SERIES_1: 20;

        hence

         A35: Cat is absolutely_summable by SERIES_1:def 4;

        then Cat is summable;

        then (r (#) Cat) is summable & ( Sum (r (#) Cat)) = (r * ( Sum Cat)) by SERIES_1: 10;

        then ( Sum (Cat ^\ ( 0 qua Nat + 1))) = (( Sum Cat) * (r * ( Sum Cat))) by A35, A31, Th53;

        then ( Sum Cat) = (1 + (r * (( Sum Cat) * ( Sum Cat)))) by A35, A34, SERIES_1: 15;

        hence thesis by A15, WSIERP_1: 1;

      end;

      consider SumC be Function of REAL , REAL such that

       A36: for x be object st x in REAL holds E[x, (SumC . x)] from FUNCT_2:sch 1( A1);

      

       A37: for r, s st 0 < s & s <= r & r < (1 / 4) holds (SumC . s) <= (SumC . r)

      proof

        let r, s such that

         A38: 0 < s and

         A39: s <= r and

         A40: r < (1 / 4);

        r in REAL by XREAL_0:def 1;

        then

        consider Cr be Real_Sequence such that

         A41: for n holds (Cr . n) = (( Catalan (n + 1)) * (r |^ n)) and

         A42: |.r.| < (1 / 4) implies Cr is absolutely_summable & ( Sum Cr) = (1 + (r * (( Sum Cr) |^ 2))) & (SumC . r) = ( Sum Cr) by A36;

        s in REAL by XREAL_0:def 1;

        then

        consider Cs be Real_Sequence such that

         A43: for n holds (Cs . n) = (( Catalan (n + 1)) * (s |^ n)) and

         A44: |.s.| < (1 / 4) implies Cs is absolutely_summable & ( Sum Cs) = (1 + (s * (( Sum Cs) |^ 2))) & (SumC . s) = ( Sum Cs) by A36;

         A45:

        now

          let n be Nat;

          (s |^ n) <= (r |^ n) & ( Catalan (n + 1)) >= 0 by A38, A39, CATALAN1: 17, PREPOWER: 9;

          then

           A46: (( Catalan (n + 1)) * (s |^ n)) <= (( Catalan (n + 1)) * (r |^ n)) by XREAL_1: 64;

          (( Catalan (n + 1)) * (r |^ n)) = (Cr . n) by A41;

          hence (Cs . n) <= (Cr . n) by A43, A46;

        end;

        

         A47: s < (1 / 4) by A39, A40, XXREAL_0: 2;

        thus thesis by A38, A39, A40, A47, A44, A42, A45, ABSVALUE:def 1, TIETZE: 5;

      end;

      set R = { r where r be Real : 0 < r & r < (1 / 4) & (SumC . r) = ((1 + ( sqrt (1 - (4 * r)))) / (2 * r)) };

      

       A48: for r st r <> 0 & |.r.| < (1 / 4) holds (SumC . r) = ((1 - ( sqrt (1 - (4 * r)))) / (2 * r)) or (SumC . r) = ((1 + ( sqrt (1 - (4 * r)))) / (2 * r))

      proof

        let r such that

         A49: r <> 0 and

         A50: |.r.| < (1 / 4);

        r <= (1 / 4) by A50, ABSVALUE: 5;

        then (4 * r) <= ((1 / 4) * 4) by XREAL_1: 64;

        then

         A51: ((4 * r) - (4 * r)) <= (1 - (4 * r)) by XREAL_1: 9;

        r in REAL by XREAL_0:def 1;

        then

        consider Catal be Real_Sequence such that for n holds (Catal . n) = (( Catalan (n + 1)) * (r |^ n)) and

         A52: |.r.| < (1 / 4) implies Catal is absolutely_summable & ( Sum Catal) = (1 + (r * (( Sum Catal) |^ 2))) & (SumC . r) = ( Sum Catal) by A36;

        set S = ( Sum Catal);

        S = (1 + (r * (S ^2 ))) by A50, A52, WSIERP_1: 1;

        then

         A53: (((r * (S ^2 )) + (( - 1) * S)) + 1) = 0 ;

        ( delta (r,( - 1),1)) = (1 - (4 * r)) & ( - ( - 1)) = 1;

        hence thesis by A49, A50, A52, A53, A51, FIB_NUM: 6;

      end;

      

       A54: for r, s st 0 < r & r < s & s < (1 / 4) holds ((1 + ( sqrt (1 - (4 * r)))) / (2 * r)) > ((1 + ( sqrt (1 - (4 * s)))) / (2 * s))

      proof

        let r, s such that

         A55: 0 < r and

         A56: r < s and

         A57: s < (1 / 4);

        (4 * s) < (4 * (1 / 4)) by A57, XREAL_1: 68;

        then

         A58: ((4 * s) - (4 * s)) < (1 - (4 * s)) by XREAL_1: 9;

        then

         A59: ( sqrt (1 - (4 * s))) > 0 by SQUARE_1: 25;

        (4 * r) < (4 * s) by A56, XREAL_1: 68;

        then (1 - (4 * r)) >= (1 - (4 * s)) by XREAL_1: 10;

        then ( sqrt (1 - (4 * r))) >= ( sqrt (1 - (4 * s))) by A58, SQUARE_1: 26;

        then (1 + ( sqrt (1 - (4 * r)))) >= (1 + ( sqrt (1 - (4 * s)))) by XREAL_1: 7;

        then

         A60: ((1 + ( sqrt (1 - (4 * r)))) / (2 * r)) >= ((1 + ( sqrt (1 - (4 * s)))) / (2 * r)) by A55, XREAL_1: 72;

        (2 * r) > (2 * 0 ) & (2 * r) < (2 * s) by A55, A56, XREAL_1: 68;

        then ((1 + ( sqrt (1 - (4 * s)))) / (2 * r)) > ((1 + ( sqrt (1 - (4 * s)))) / (2 * s)) by A59, XREAL_1: 76;

        hence thesis by A60, XXREAL_0: 2;

      end;

      

       A61: R = {}

      proof

        assume R <> {} ;

        then

        consider x be object such that

         A62: x in R by XBOOLE_0:def 1;

        consider r be Real such that x = r and

         A63: 0 < r and

         A64: r < (1 / 4) and

         A65: (SumC . r) = ((1 + ( sqrt (1 - (4 * r)))) / (2 * r)) by A62;

        consider s be Real such that

         A66: r < s and

         A67: s < (1 / 4) by A64, XREAL_1: 5;

        

         A68: |.s.| = s by A63, A66, ABSVALUE:def 1;

        (4 * s) < (4 * (1 / 4)) by A67, XREAL_1: 68;

        then ((4 * s) - (4 * s)) < (1 - (4 * s)) by XREAL_1: 9;

        then ( sqrt (1 - (4 * s))) > 0 by SQUARE_1: 25;

        then (1 - ( sqrt (1 - (4 * s)))) <= (1 - 0 ) by XREAL_1: 10;

        then

         A69: ((1 - ( sqrt (1 - (4 * s)))) / (2 * s)) <= (1 / (2 * s)) by A63, A66, XREAL_1: 72;

        

         A70: (2 * r) > (2 * 0 ) by A63, XREAL_1: 68;

        R c= {r}

        proof

          assume not R c= {r};

          then (R \ {r}) <> {} by XBOOLE_1: 37;

          then

          consider y be object such that

           A71: y in (R \ {r}) by XBOOLE_0:def 1;

          y in R by A71;

          then

          consider s be Real such that

           A72: y = s and

           A73: 0 < s and

           A74: s < (1 / 4) and

           A75: (SumC . s) = ((1 + ( sqrt (1 - (4 * s)))) / (2 * s));

          

           A76: r <> s by A71, A72, ZFMISC_1: 56;

          now

            per cases by A76, XXREAL_0: 1;

              suppose

               A77: r > s;

              then (SumC . s) > (SumC . r) by A54, A64, A65, A73, A75;

              hence contradiction by A37, A64, A73, A77;

            end;

              suppose

               A78: r < s;

              then (SumC . r) > (SumC . s) by A54, A63, A65, A74, A75;

              hence contradiction by A37, A63, A74, A78;

            end;

          end;

          hence contradiction;

        end;

        then not s in R by A66, TARSKI:def 1;

        then (SumC . s) <> ((1 + ( sqrt (1 - (4 * s)))) / (2 * s)) by A63, A66, A67;

        then

         A79: (SumC . s) = ((1 - ( sqrt (1 - (4 * s)))) / (2 * s)) by A48, A63, A66, A67, A68;

        (4 * r) < (4 * (1 / 4)) by A64, XREAL_1: 68;

        then ((4 * r) - (4 * r)) < (1 - (4 * r)) by XREAL_1: 9;

        then ( sqrt (1 - (4 * r))) > 0 by SQUARE_1: 25;

        then (1 + 0 qua Nat) < (1 + ( sqrt (1 - (4 * r)))) by XREAL_1: 8;

        then

         A80: (1 / (2 * r)) < (SumC . r) by A65, A70, XREAL_1: 74;

        (2 * r) < (2 * s) by A66, XREAL_1: 68;

        then (1 / (2 * s)) < (1 / (2 * r)) by A70, XREAL_1: 76;

        then (SumC . s) < (1 / (2 * r)) by A79, A69, XXREAL_0: 2;

        then (SumC . s) < (SumC . r) by A80, XXREAL_0: 2;

        hence thesis by A37, A63, A66, A67;

      end;

      

       A81: for r st 0 < r & |.r.| < (1 / 4) holds (SumC . r) = ((1 - ( sqrt (1 - (4 * r)))) / (2 * r))

      proof

        let r such that

         A82: 0 < r and

         A83: |.r.| < (1 / 4);

        assume (SumC . r) <> ((1 - ( sqrt (1 - (4 * r)))) / (2 * r));

        then

         A84: (SumC . r) = ((1 + ( sqrt (1 - (4 * r)))) / (2 * r)) by A48, A82, A83;

         |.r.| = r by A82, ABSVALUE:def 1;

        then r in R by A82, A83, A84;

        hence thesis by A61;

      end;

      

       A85: for r st r < 0 & |.r.| < (1 / 4) holds (SumC . r) = ((1 - ( sqrt (1 - (4 * r)))) / (2 * r))

      proof

        let r such that

         A86: r < 0 and

         A87: |.r.| < (1 / 4);

        (2 * r) < (2 * 0 ) by A86, XREAL_1: 68;

        then

         A88: |.(2 * r).| = ( - (2 * r)) & ( 0 qua Nat - (2 * r)) > ( 0 qua Nat - 0 ) by ABSVALUE:def 1;

        

         A89: |.( - r).| < (1 / 4) by A87, COMPLEX1: 52;

        then (1 / 4) >= ( - r) by ABSVALUE: 5;

        then (4 * (1 / 4)) >= (4 * ( - r)) by XREAL_1: 64;

        then (1 - (4 * ( - r))) >= ((4 * ( - r)) - (4 * ( - r))) by XREAL_1: 9;

        then ( sqrt (1 - (4 * ( - r)))) >= 0 by SQUARE_1:def 2;

        then

         A90: (1 - ( sqrt (1 - (4 * ( - r))))) <= (1 - 0 ) by XREAL_1: 10;

        

         A91: ( sqrt (1 - (4 * r))) > 0 by A86, SQUARE_1: 25;

        then (1 + ( sqrt (1 - (4 * r)))) > (1 + 0 qua Nat) by XREAL_1: 8;

        then

         A92: (1 - ( sqrt (1 - (4 * ( - r))))) < (1 + ( sqrt (1 - (4 * r)))) by A90, XXREAL_0: 2;

        (1 + ( sqrt (1 - (4 * r)))) = |.(1 + ( sqrt (1 - (4 * r)))).| by A91, ABSVALUE:def 1;

        then

         A93: ((1 - ( sqrt (1 - (4 * ( - r))))) / (2 * ( - r))) < ( |.(1 + ( sqrt (1 - (4 * r)))).| / |.(2 * r).|) by A92, A88, XREAL_1: 74;

        ( - r) in REAL by XREAL_0:def 1;

        then E[( - r), (SumC . ( - r))] by A36;

        then for s st ( - r) = s holds ex Catal be Real_Sequence st (for n holds (Catal . n) = (( Catalan (n + 1)) * (s |^ n))) & ( |.s.| < (1 / 4) implies Catal is absolutely_summable & ( Sum Catal) = (1 + (s * (( Sum Catal) |^ 2))) & (SumC . ( - r)) = ( Sum Catal));

        then

        consider CR be Real_Sequence such that

         A94: for n holds (CR . n) = (( Catalan (n + 1)) * (( - r) |^ n)) and

         A95: |.( - r).| < (1 / 4) implies CR is absolutely_summable & ( Sum CR) = (1 + (( - r) * (( Sum CR) |^ 2))) & (SumC . ( - r)) = ( Sum CR);

        assume

         A96: (SumC . r) <> ((1 - ( sqrt (1 - (4 * r)))) / (2 * r));

        r in REAL by XREAL_0:def 1;

        then

        consider Cr be Real_Sequence such that

         A97: for n holds (Cr . n) = (( Catalan (n + 1)) * (r |^ n)) and

         A98: |.r.| < (1 / 4) implies Cr is absolutely_summable & ( Sum Cr) = (1 + (r * (( Sum Cr) |^ 2))) & (SumC . r) = ( Sum Cr) by A36;

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Element of NAT ;

          (( - r) |^ n) = ((( - 1) * r) |^ n)

          .= ((( - 1) |^ n) * (r |^ n)) by NEWTON: 7;

          

          then

           A99: |.(( - r) |^ n).| = ( |.(( - 1) |^ n).| * |.(r |^ n).|) by COMPLEX1: 65

          .= (1 * |.(r |^ n).|) by SERIES_2: 1;

          ( Catalan (n + 1)) >= 0 by CATALAN1: 17;

          then

           A100: |.( Catalan (n + 1)).| = ( Catalan (n + 1)) by ABSVALUE:def 1;

          (( - r) |^ n) >= 0 by A86, POWER: 3;

          then |.(( - r) |^ n).| = (( - r) |^ n) by ABSVALUE:def 1;

          

          then (CR . n) = ( |.(r |^ n).| * |.( Catalan (n + 1)).|) by A94, A99, A100

          .= |.((r |^ n) * ( Catalan (n + 1))).| by COMPLEX1: 65

          .= |.(Cr . n).| by A97

          .= (( abs Cr) . n) by SEQ_1: 12;

          hence (( abs Cr) . x) = (CR . x);

        end;

        then

         A101: ( abs Cr) = CR by FUNCT_2: 12;

        ( 0 qua Nat - r) > ( 0 qua Nat - 0 ) by A86;

        then

         A102: ( Sum CR) = ((1 - ( sqrt (1 - (4 * ( - r))))) / (2 * ( - r))) by A81, A95, A89;

         |.( Sum Cr).| <= ( Sum ( abs Cr)) by A87, A98, TIETZE: 6;

        then |.((1 + ( sqrt (1 - (4 * r)))) / (2 * r)).| <= ( Sum CR) by A48, A86, A87, A98, A101, A96;

        hence thesis by A102, A93, COMPLEX1: 67;

      end;

      let r;

      r in REAL by XREAL_0:def 1;

      then

      consider Cat be Real_Sequence such that

       A103: for n holds (Cat . n) = (( Catalan (n + 1)) * (r |^ n)) and

       A104: |.r.| < (1 / 4) implies Cat is absolutely_summable & ( Sum Cat) = (1 + (r * (( Sum Cat) |^ 2))) & (SumC . r) = ( Sum Cat) by A36;

      set s = ( sqrt (1 - (4 * r)));

      take Cat;

      thus for n holds (Cat . n) = (( Catalan (n + 1)) * (r |^ n)) by A103;

      assume

       A105: |.r.| < (1 / 4);

      hence Cat is absolutely_summable & ( Sum Cat) = (1 + (r * (( Sum Cat) |^ 2))) by A104;

      

       A106: r <> 0 implies ( Sum Cat) = ((1 - ( sqrt (1 - (4 * r)))) / (2 * r))

      proof

        assume r <> 0 ;

        then r > 0 or r < 0 ;

        hence thesis by A81, A85, A104, A105;

      end;

      now

        per cases ;

          suppose r = 0 ;

          hence (2 / (1 + s)) = ( Sum Cat) by A104, A105, SQUARE_1: 18;

        end;

          suppose

           A107: r <> 0 ;

          then

           A108: (2 * r) <> 0 ;

          r <= (1 / 4) by A105, ABSVALUE: 5;

          then (4 * r) <= (4 * (1 / 4)) by XREAL_1: 64;

          then

           A109: (1 - (4 * r)) >= ((4 * r) - (4 * r)) by XREAL_1: 9;

          then s >= 0 by SQUARE_1:def 2;

          then ((1 + s) / (1 + s)) = 1 by XCMPLX_1: 60;

          

          then ((1 - s) / (2 * r)) = (((1 - s) / (2 * r)) * ((1 + s) / (1 + s)))

          .= (((1 - s) * (1 + s)) / ((2 * r) * (1 + s))) by XCMPLX_1: 76

          .= (((1 ^2 ) - (s ^2 )) / ((2 * r) * (1 + s)))

          .= ((1 - (1 - (4 * r))) / ((2 * r) * (1 + s))) by A109, SQUARE_1:def 2

          .= (((2 * r) * 2) / ((2 * r) * (1 + s)))

          .= (((2 * r) / (2 * r)) * (2 / (1 + s))) by XCMPLX_1: 76

          .= (1 * (2 / (1 + s))) by A108, XCMPLX_1: 60;

          hence ( Sum Cat) = (2 / (1 + s)) by A106, A107;

        end;

      end;

      hence thesis by A106;

    end;