prsubset.miz



    begin

    definition

      let x be FinSequence;

      let I be set;

      :: PRSUBSET:def1

      func Seq (x,I) -> FinSequence equals ( Seq (x | I));

      coherence ;

    end

    registration

      let D be set;

      let x be D -valued FinSequence;

      let I be set;

      cluster ( Seq (x,I)) -> D -valued;

      coherence ;

    end

    registration

      let x be real-valued FinSequence;

      let I be set;

      cluster ( Seq (x,I)) -> real-valued;

      coherence ;

    end

    registration

      let D be set;

      let x be D -valued FinSequence;

      let i be Nat;

      cluster (x | i) -> D -valued;

      correctness ;

    end

    registration

      let x be real-valued FinSequence;

      let i be Nat;

      cluster (x | i) -> real-valued;

      correctness ;

    end

    definition

      let x be REAL -valued FinSequence;

      let a be Real;

      :: PRSUBSET:def2

      pred x exist_subset_sum_eq a means ex I be set st I c= ( dom x) & ( Sum ( Seq (x,I))) = a;

    end

    

     LM010: for x be REAL -valued FinSequence holds ex Q be Function of [:( Seg ( len x)), REAL :], BOOLEAN st for i be Nat, s be Real st 1 <= i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (Q . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (Q . (i,s)) = FALSE )

    proof

      let x be REAL -valued FinSequence;

      set L = ( Seg ( len x));

      defpred P1[ object, object, object] means ex i be Nat, s be Real st $1 = i & $2 = s & ((x | i) exist_subset_sum_eq s implies $3 = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies $3 = FALSE );

      

       A1: for u,t be object st u in L & t in REAL holds ex z be object st z in BOOLEAN & P1[u, t, z]

      proof

        let u,t be object;

        assume

         A2: u in L & t in REAL ;

        then

        reconsider i = u as Nat;

        reconsider s = t as Real by A2;

        per cases ;

          suppose

           A3: (x | i) exist_subset_sum_eq s;

          take z = TRUE ;

          thus z in BOOLEAN ;

          thus P1[u, t, z] by A3;

        end;

          suppose

           A4: not (x | i) exist_subset_sum_eq s;

          take z = FALSE ;

          thus z in BOOLEAN ;

          thus P1[u, t, z] by A4;

        end;

      end;

      consider Q be Function of [:L, REAL :], BOOLEAN such that

       A5: for x,y be object st x in L & y in REAL holds P1[x, y, (Q . (x,y))] from BINOP_1:sch 1( A1);

      take Q;

      let i be Nat, s be Real;

      assume

       A6: 1 <= i <= ( len x);

      i in L by A6;

      then ex i0 be Nat, s0 be Real st i = i0 & s = s0 & ((x | i0) exist_subset_sum_eq s0 implies (Q . (i,s)) = TRUE ) & ( not (x | i0) exist_subset_sum_eq s0 implies (Q . (i,s)) = FALSE ) by A5, XREAL_0:def 1;

      hence thesis;

    end;

    

     LM020: for x be REAL -valued FinSequence holds for Q1,Q2 be Function of [:( Seg ( len x)), REAL :], BOOLEAN st (for i be Nat, s be Real st 1 <= i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (Q1 . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (Q1 . (i,s)) = FALSE )) & (for i be Nat, s be Real st 1 <= i & i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (Q2 . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (Q2 . (i,s)) = FALSE )) holds Q1 = Q2

    proof

      let x be REAL -valued FinSequence;

      set L = ( Seg ( len x));

      let Q1,Q2 be Function of [:L, REAL :], BOOLEAN ;

      assume that

       A1: for i be Nat, s be Real st 1 <= i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (Q1 . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (Q1 . (i,s)) = FALSE ) and

       A2: for i be Nat, s be Real st 1 <= i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (Q2 . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (Q2 . (i,s)) = FALSE );

      for i,s be set st i in L & s in REAL holds (Q1 . (i,s)) = (Q2 . (i,s))

      proof

        let i,s be set;

        assume

         A3: i in L & s in REAL ;

        then

        reconsider i0 = i as Nat;

        reconsider s0 = s as Real by A3;

        

         A4: 1 <= i0 & i0 <= ( len x) by A3, FINSEQ_1: 1;

        per cases ;

          suppose

           A5: (x | i0) exist_subset_sum_eq s0;

          

          hence (Q1 . (i,s)) = TRUE by A1, A4

          .= (Q2 . (i,s)) by A2, A4, A5;

        end;

          suppose

           A6: not (x | i0) exist_subset_sum_eq s0;

          

          hence (Q1 . (i,s)) = FALSE by A1, A4

          .= (Q2 . (i,s)) by A2, A4, A6;

        end;

      end;

      hence Q1 = Q2;

    end;

    definition

      let x be REAL -valued FinSequence;

      :: PRSUBSET:def3

      func Q_ex (x) -> Function of [:( Seg ( len x)), REAL :], BOOLEAN means

      : defQ: for i be Nat, s be Real st 1 <= i <= ( len x) holds ((x | i) exist_subset_sum_eq s implies (it . (i,s)) = TRUE ) & ( not (x | i) exist_subset_sum_eq s implies (it . (i,s)) = FALSE );

      existence by LM010;

      uniqueness by LM020;

    end

    registration

      let A be Subset of NAT ;

      let i be Nat, s be Real;

      let f be Function of [:A, REAL :], BOOLEAN ;

      cluster (f . (i,s)) -> boolean;

      correctness ;

    end

    definition

      let a,b be object;

      :: PRSUBSET:def4

      func a _eq_ b -> object equals ( IFEQ (a,b, TRUE , FALSE ));

      correctness ;

    end

    registration

      let a,b be object;

      cluster (a _eq_ b) -> boolean;

      correctness ;

    end

    definition

      let a,b be ExtReal;

      :: PRSUBSET:def5

      func a _le_ b -> object equals ( IFGT (a,b, FALSE , TRUE ));

      correctness ;

    end

    registration

      let a,b be ExtReal;

      cluster (a _le_ b) -> boolean;

      correctness by XXREAL_0:def 11;

    end

    

     Lemacik1: for x be REAL -valued FinSequence st 1 <= ( len x) holds ( dom (x | 1)) = {1}

    proof

      let x be REAL -valued FinSequence;

      assume 1 <= ( len x);

      then

       A3: ( len (x | 1)) = 1 by FINSEQ_1: 59;

      1 in ( Seg 1);

      then ((x | 1) . 1) = (x . 1) by FUNCT_1: 49;

      then (x | 1) = <*(x . 1)*> by FINSEQ_1: 40, A3;

      hence thesis by FINSEQ_1: 2, FINSEQ_1: 38;

    end;

    theorem :: PRSUBSET:1

    for s be Real, x be REAL -valued FinSequence st 1 <= ( len x) holds (( Q_ex x) . (1,s)) = (((x . 1) _eq_ s) 'or' (s _eq_ 0 ))

    proof

      let s be Real, x be REAL -valued FinSequence;

      assume

       A1: 1 <= ( len x);

      then

       Q1: ((x | 1) exist_subset_sum_eq s implies (( Q_ex x) . (1,s)) = TRUE ) & ( not (x | 1) exist_subset_sum_eq s implies (( Q_ex x) . (1,s)) = FALSE ) by defQ;

      

       A3: ( len (x | 1)) = 1 by FINSEQ_1: 59, A1;

      1 in ( Seg 1);

      then

       A4: ((x | 1) . 1) = (x . 1) by FUNCT_1: 49;

      

       A5: {1} = ( dom (x | 1)) by A1, Lemacik1;

      

       A8: ( Seq ((x | 1), {1})) = ((x | 1) | {1}) by A5, FINSEQ_3: 116

      .= <*(x . 1)*> by FINSEQ_1: 40, A3, A5, A4;

      per cases ;

        suppose

         A9: s <> 0 ;

        then

         A10: (s _eq_ 0 ) = FALSE by FUNCOP_1:def 8;

        per cases ;

          suppose

           A11: (x . 1) = s;

          then

           A12: ((x . 1) _eq_ s) = TRUE by FUNCOP_1:def 8;

          ( Sum ( Seq ((x | 1), {1}))) = s by A11, A8, RVSUM_1: 73;

          hence (( Q_ex x) . (1,s)) = (((x . 1) _eq_ s) 'or' (s _eq_ 0 )) by Q1, A12, A5;

        end;

          suppose

           A13: (x . 1) <> s;

           not (x | 1) exist_subset_sum_eq s

          proof

            assume (x | 1) exist_subset_sum_eq s;

            then

            consider I be set such that

             A15: I c= ( dom (x | 1)) & ( Sum ( Seq ((x | 1),I))) = s;

            ( dom (x | 1)) = {1} by A1, Lemacik1;

            per cases by A15, ZFMISC_1: 33;

              suppose I = {} ;

              hence contradiction by A9, A15, RVSUM_1: 72;

            end;

              suppose I = {1};

              hence contradiction by A13, A15, A8, RVSUM_1: 73;

            end;

          end;

          hence (( Q_ex x) . (1,s)) = (((x . 1) _eq_ s) 'or' (s _eq_ 0 )) by A13, A10, Q1, FUNCOP_1:def 8;

        end;

      end;

        suppose

         A20: s = 0 ;

        then

         A21: (s _eq_ 0 ) = TRUE by FUNCOP_1:def 8;

        (x | 1) exist_subset_sum_eq s

        proof

          take {} ;

          thus thesis by A20, RVSUM_1: 72;

        end;

        hence (( Q_ex x) . (1,s)) = (((x . 1) _eq_ s) 'or' (s _eq_ 0 )) by A21, A1, defQ;

      end;

    end;

    

     LM040: for i,k,x be Nat, I be set st I c= ( Seg k) & k < x & x in ( Seg i) holds ( Sgm (I \/ {x})) = (( Sgm I) ^ <*x*>)

    proof

      let i,k,x be Nat, I be set;

      assume that

       A1: I c= ( Seg k) and

       A2: k < x and

       A3: x in ( Seg i);

      

       A5: {x} c= ( Seg i) by A3, ZFMISC_1: 31;

      for m,n be Nat st m in I & n in {x} holds m < n

      proof

        let m,n be Nat;

        assume

         A6: m in I & n in {x};

        then

         A8: n = x by TARSKI:def 1;

        1 <= m & m <= k by A1, A6, FINSEQ_1: 1;

        hence m < n by A8, A2, XXREAL_0: 2;

      end;

      

      hence ( Sgm (I \/ {x})) = (( Sgm I) ^ ( Sgm {x})) by A1, A5, FINSEQ_3: 42

      .= (( Sgm I) ^ <*x*>) by FINSEQ_3: 44, A2;

    end;

    theorem :: PRSUBSET:2

    

     LM050: for f,g be Function, X,Y be set st ( rng g) c= X holds ((f | (X \/ Y)) * g) = ((f | X) * g)

    proof

      let f,g be Function, X,Y be set;

      assume

       A1: ( rng g) c= X;

      

       A2: for i be object holds i in ( dom ((f | (X \/ Y)) * g)) iff i in ( dom g) & (g . i) in ( dom (f | X))

      proof

        let i be object;

        hereby

          assume

           AA: i in ( dom ((f | (X \/ Y)) * g));

          then

           A3: i in ( dom g) & (g . i) in ( dom (f | (X \/ Y))) by FUNCT_1: 11;

          then (g . i) in (( dom f) /\ (X \/ Y)) by RELAT_1: 61;

          then

           P3: (g . i) in ( dom f) & (g . i) in (X \/ Y) by XBOOLE_0:def 4;

          (g . i) in ( rng g) by A3, FUNCT_1: 3;

          then (g . i) in (( dom f) /\ X) by A1, P3, XBOOLE_0:def 4;

          hence i in ( dom g) & (g . i) in ( dom (f | X)) by AA, FUNCT_1: 11, RELAT_1: 61;

        end;

        assume

         A4: i in ( dom g) & (g . i) in ( dom (f | X));

        then (g . i) in (( dom f) /\ X) by RELAT_1: 61;

        then

         A5: (g . i) in ( dom f) & (g . i) in X by XBOOLE_0:def 4;

        then (g . i) in (X \/ Y) by XBOOLE_0:def 3;

        then (g . i) in (( dom f) /\ (X \/ Y)) by A5, XBOOLE_0:def 4;

        then (g . i) in ( dom (f | (X \/ Y))) by RELAT_1: 61;

        hence i in ( dom ((f | (X \/ Y)) * g)) by A4, FUNCT_1: 11;

      end;

      for i be object st i in ( dom ((f | (X \/ Y)) * g)) holds (((f | (X \/ Y)) * g) . i) = ((f | X) . (g . i))

      proof

        let i be object;

        assume

         A7: i in ( dom ((f | (X \/ Y)) * g));

        then i in ( dom g) & (g . i) in ( dom (f | X)) by A2;

        then (g . i) in (( dom f) /\ X) by RELAT_1: 61;

        then (g . i) in ( dom f) & (g . i) in X by XBOOLE_0:def 4;

        then

         A9: (g . i) in (X \/ Y) by XBOOLE_0:def 3;

        

        thus (((f | (X \/ Y)) * g) . i) = ((f | (X \/ Y)) . (g . i)) by A7, FUNCT_1: 12

        .= (f . (g . i)) by FUNCT_1: 49, A9

        .= ((f | X) . (g . i)) by A2, A7, FUNCT_1: 47;

      end;

      hence thesis by FUNCT_1: 10, A2;

    end;

    theorem :: PRSUBSET:3

    

     LM060: for x be REAL -valued FinSequence, i be Nat, I0 be set st I0 c= ( Seg i) & ( Seg (i + 1)) c= ( dom x) holds ( Seq ((x | (i + 1)),(I0 \/ {(i + 1)}))) = (( Seq ((x | i),I0)) ^ <*(x . (i + 1))*>)

    proof

      let x be REAL -valued FinSequence, i be Nat, I0 be set;

      assume

       A1: I0 c= ( Seg i) & ( Seg (i + 1)) c= ( dom x);

      

       A4: ( Seg i) c= ( Seg (i + 1)) by NAT_1: 11, FINSEQ_1: 5;

      then

       A17: I0 c= ( dom x) by A1;

      

       A6: ( dom (x | (i + 1))) = ( Seg (i + 1)) by A1, RELAT_1: 62;

      then

       A7: {(i + 1)} c= ( dom (x | (i + 1))) by FINSEQ_1: 4, ZFMISC_1: 31;

      

       A8: I0 c= ( Seg (i + 1)) by A4, A1;

      then

       A9: (I0 \/ {(i + 1)}) c= ( Seg (i + 1)) by A7, A6, XBOOLE_1: 8;

      

       A10: ( Seq ((x | (i + 1)),(I0 \/ {(i + 1)}))) = ( Seq (x | (I0 \/ {(i + 1)}))) by A8, A7, A6, XBOOLE_1: 8, RELAT_1: 74

      .= ((x | (I0 \/ {(i + 1)})) * ( Sgm ( dom (x | (I0 \/ {(i + 1)})))));

      

       A11: (I0 \/ {(i + 1)}) c= ( dom x) by A1, A9;

      then

       A12: ( dom (x | (I0 \/ {(i + 1)}))) = (I0 \/ {(i + 1)}) by RELAT_1: 62;

      i < (i + 1) & (i + 1) in ( Seg (i + 1)) by FINSEQ_1: 4, NAT_1: 16;

      then

       A13: ( Sgm (I0 \/ {(i + 1)})) = (( Sgm I0) ^ <*(i + 1)*>) by A1, LM040;

      

       A14: ( dom (x | (I0 \/ {(i + 1)}))) = (I0 \/ {(i + 1)}) by RELAT_1: 62, A11;

      ( rng (x | (I0 \/ {(i + 1)}))) c= REAL ;

      then

      reconsider f = (x | (I0 \/ {(i + 1)})) as Function of (I0 \/ {(i + 1)}), REAL by A14, FUNCT_2: 2;

      ( rng ( Sgm I0)) = I0 by FINSEQ_1:def 13, A1;

      then

      reconsider p = ( Sgm I0) as FinSequence of (I0 \/ {(i + 1)}) by FINSEQ_1:def 4, XBOOLE_1: 10;

      (i + 1) in {(i + 1)} by TARSKI:def 1;

      then

      reconsider d = (i + 1) as Element of (I0 \/ {(i + 1)}) by XBOOLE_0:def 3;

      

       A15: ( Seq ((x | (i + 1)),(I0 \/ {(i + 1)}))) = ((f * p) ^ <*(f . d)*>) by FINSEQOP: 8, A13, A10, A12;

      

       A19: ( rng ( Sgm I0)) = I0 by FINSEQ_1:def 13, A1;

      (f * p) = ((x | I0) * ( Sgm I0)) by LM050, A19

      .= ( Seq ((x | I0) | I0)) by A17, RELAT_1: 62

      .= ( Seq ((x | i),I0)) by A1, RELAT_1: 74;

      hence thesis by A15, FUNCT_1: 49;

    end;

    theorem :: PRSUBSET:4

    

     LM080: for x be real-valued FinSequence st x <> {} & x is positive holds 0 < ( Sum x)

    proof

      let x be real-valued FinSequence;

      assume that

       A1: x <> {} and

       A2: x is positive;

      consider i be object such that

       A3: i in ( dom x) by A1, XBOOLE_0:def 1;

      

       A4: 0 < (x . i) by A3, A2;

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

      hence 0 < ( Sum x) by RVSUM_1: 85, A3, A4;

    end;

    theorem :: PRSUBSET:5

    

     LM090: for x be real-valued FinSequence, i be Nat st x is positive & 1 <= i <= ( len x) holds (x | i) is positive & (x | i) <> {}

    proof

      let x be real-valued FinSequence;

      let i be Nat;

      assume that

       A2: x is positive and

       A3: 1 <= i and

       A4: i <= ( len x);

      

       A5: ( dom (x | i)) c= ( dom x) by RELAT_1: 60;

      

       A6: ( len (x | i)) = i by A4, FINSEQ_1: 59;

      for j be Nat st j in ( dom (x | i)) holds 0 < ((x | i) . j)

      proof

        let j be Nat;

        assume

         A7: j in ( dom (x | i));

        then

         A8: 0 < (x . j) by A2, A5;

        ( Seg i) c= ( Seg ( len x)) by A4, FINSEQ_1: 5;

        then ( Seg i) c= ( dom x) by FINSEQ_1:def 3;

        then ( dom (x | i)) = ( Seg i) by RELAT_1: 62;

        then j <= i by A7, FINSEQ_1: 1;

        hence thesis by A8, FINSEQ_3: 112;

      end;

      hence (x | i) is positive & (x | i) <> {} by A3, A6;

    end;

    theorem :: PRSUBSET:6

    

     LM100: for x be real-valued FinSequence, I be set st x is positive & I c= ( dom x) & I <> {} holds ( Seq (x,I)) is positive & ( Seq (x,I)) <> {}

    proof

      let x be real-valued FinSequence;

      let I be set;

      assume that

       A2: x is positive and

       A3: I c= ( dom x) and

       A4: I <> {} ;

      

       A5: ( dom x) meets I by A4, A3, XBOOLE_1: 28;

      for j be Nat st j in ( dom ( Seq (x,I))) holds 0 < (( Seq (x,I)) . j)

      proof

        let j be Nat;

        assume

         A6: j in ( dom ( Seq (x,I)));

        reconsider sfi = ( Seq (x | I)) as real-valued FinSequence;

        

         A9: (( Sgm ( dom (x | I))) . j) in ( dom (x | I)) by A6, FUNCT_1: 11;

        

         A10: ( dom (x | I)) c= ( dom x) by RELAT_1: 60;

        (( Seq (x,I)) . j) = ((x | I) . (( Sgm ( dom (x | I))) . j)) by A6, FUNCT_1: 12

        .= (x . (( Sgm ( dom (x | I))) . j)) by A9, FUNCT_1: 47;

        hence thesis by A10, A2, A9;

      end;

      hence thesis by A5, RELAT_1: 66, FINSEQ_1: 97;

    end;

    theorem :: PRSUBSET:7

    for x be REAL -valued FinSequence st x is positive holds for i be Nat, s be Real st 1 <= i < ( len x) holds (( Q_ex x) . ((i + 1),s)) = ((( Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' (( Q_ex x) . (i,(s - (x . (i + 1)))))))

    proof

      let x be REAL -valued FinSequence;

      assume

       AS0: x is positive;

      let i be Nat, s be Real;

      assume

       A1: 1 <= i < ( len x);

      

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

      

       A3: (i + 1) <= ( len x) by A1, NAT_1: 13;

      then

       A4: (i + 1) in ( Seg ( len x)) by A2;

      s in REAL by XREAL_0:def 1;

      then [(i + 1), s] in [:( Seg ( len x)), REAL :] by ZFMISC_1: 87, A4;

      then (( Q_ex x) . [(i + 1), s]) in BOOLEAN by FUNCT_2: 5;

      then

       A5: (( Q_ex x) . ((i + 1),s)) = TRUE or (( Q_ex x) . ((i + 1),s)) = FALSE by TARSKI:def 2;

      ( Seg i) c= ( Seg ( len x)) by A1, FINSEQ_1: 5;

      then ( Seg i) c= ( dom x) by FINSEQ_1:def 3;

      then

       A8: ( dom (x | i)) = ( Seg i) by RELAT_1: 62;

      

       A9: ( Seg i) c= ( Seg (i + 1)) by NAT_1: 11, FINSEQ_1: 5;

      ( Seg (i + 1)) c= ( Seg ( len x)) by FINSEQ_1: 5, A3;

      then

       A10: ( Seg (i + 1)) c= ( dom x) by FINSEQ_1:def 3;

      then

       A11: ( dom (x | (i + 1))) = ( Seg (i + 1)) by RELAT_1: 62;

      

       A12: ( dom (x | i)) c= ( dom (x | (i + 1))) by A9, A8, A10, RELAT_1: 62;

      

       A14: {(i + 1)} c= ( dom (x | (i + 1))) by A11, FINSEQ_1: 4, ZFMISC_1: 31;

      

       A15: (i + 1) in ( dom x) by A10, FINSEQ_1: 4;

      (( Q_ex x) . ((i + 1),s)) = TRUE iff ((( Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' (( Q_ex x) . (i,(s - (x . (i + 1))))))) = TRUE

      proof

        hereby

          assume (( Q_ex x) . ((i + 1),s)) = TRUE ;

          then (x | (i + 1)) exist_subset_sum_eq s by A2, A3, defQ;

          then

          consider I be set such that

           A18: I c= ( dom (x | (i + 1))) & ( Sum ( Seq ((x | (i + 1)),I))) = s;

          per cases ;

            suppose

             A19: I c= ( dom (x | i));

            then

             A21: I c= ( Seg (i + 1)) by A9, A8;

            ( Seq ((x | (i + 1)),I)) = ( Seq (x | I)) by A21, RELAT_1: 74

            .= ( Seq ((x | i) | I)) by A19, A8, RELAT_1: 74;

            then ( Sum ( Seq ((x | i),I))) = s by A18;

            then (x | i) exist_subset_sum_eq s by A19;

            then (( Q_ex x) . (i,s)) = TRUE by defQ, A1;

            hence ((( Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' (( Q_ex x) . (i,(s - (x . (i + 1))))))) = TRUE ;

          end;

            suppose

             A22: not I c= ( dom (x | i));

            

             A23: (i + 1) in I

            proof

              assume

               A24: not (i + 1) in I;

              I c= ( dom (x | i))

              proof

                let j be object;

                assume

                 A25: j in I;

                then j in ( Seg (i + 1)) by A11, A18;

                then

                reconsider j0 = j as Nat;

                

                 A27: 1 <= j0 & j0 <= (i + 1) by A25, A11, A18, FINSEQ_1: 1;

                j0 < (i + 1) by A24, A25, XXREAL_0: 1, A27;

                then j0 <= i by NAT_1: 13;

                hence j in ( dom (x | i)) by A8, A27;

              end;

              hence contradiction by A22;

            end;

            set I0 = (I \ {(i + 1)});

            

             A28: I = (I0 \/ {(i + 1)}) by A23, ZFMISC_1: 31, XBOOLE_1: 45;

            

             A32: I0 c= ( Seg i)

            proof

              let k be object;

              assume

               W: k in I0;

              then

               A29: k in I & not k in {(i + 1)} by XBOOLE_0:def 5;

              k in ( Seg (i + 1)) by A11, A18, W;

              then

              reconsider j = k as Nat;

              

               A31: 1 <= j & j <= (i + 1) by A29, A11, A18, FINSEQ_1: 1;

              j <> (i + 1) by A29, TARSKI:def 1;

              then j < (i + 1) by A31, XXREAL_0: 1;

              then j <= i by NAT_1: 13;

              hence k in ( Seg i) by A31;

            end;

            

             A34: ( Seq ((x | (i + 1)),I)) = (( Seq ((x | i),I0)) ^ <*(x . (i + 1))*>) by A10, A32, LM060, A28;

            then ( Sum ( Seq ((x | (i + 1)),I))) = (( Sum ( Seq ((x | i),I0))) + (x . (i + 1))) by RVSUM_1: 74;

            then

             A35: (x | i) exist_subset_sum_eq (s - (x . (i + 1))) by A8, A32, A18;

            

             A36: s < (x . (i + 1)) implies s < ( Sum ( Seq ((x | (i + 1)),I)))

            proof

              assume

               A37: s < (x . (i + 1));

              per cases ;

                suppose

                 A38: I0 <> {} ;

                (x | i) is positive & (x | i) <> {} by AS0, A1, LM090;

                then ( Seq ((x | i),I0)) is positive & ( Seq ((x | i),I0)) <> {} by A32, A8, A38, LM100;

                then (s + 0 ) < (( Sum ( Seq ((x | i),I0))) + (x . (i + 1))) by A37, XREAL_1: 8, LM080;

                hence thesis by A34, RVSUM_1: 74;

              end;

                suppose

                 A39: I0 = {} ;

                then

                 A42: (x | I) = { [(i + 1), (x . (i + 1))]} by GRFUNC_1: 28, A15, A28;

                ( Seq ((x | (i + 1)),I)) = <*(x . (i + 1))*> by A42, FINSEQ_3: 157, A11, A14, A28, A39, RELAT_1: 74;

                hence thesis by A37, RVSUM_1: 73;

              end;

            end;

            

             A43: ((x . (i + 1)) _le_ s) = TRUE by A36, A18, XXREAL_0:def 11;

            (( Q_ex x) . (i,(s - (x . (i + 1))))) = TRUE by A35, defQ, A1;

            hence ((( Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' (( Q_ex x) . (i,(s - (x . (i + 1))))))) = TRUE by A43;

          end;

        end;

        assume

         A44: ((( Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' (( Q_ex x) . (i,(s - (x . (i + 1))))))) = TRUE ;

        (( Q_ex x) . (i,s)) = TRUE or (((x . (i + 1)) _le_ s) = TRUE & (( Q_ex x) . (i,(s - (x . (i + 1))))) = TRUE )

        proof

          assume not ((( Q_ex x) . (i,s)) = TRUE or (((x . (i + 1)) _le_ s) = TRUE & (( Q_ex x) . (i,(s - (x . (i + 1))))) = TRUE ));

          then (( Q_ex x) . (i,s)) = FALSE & (((x . (i + 1)) _le_ s) = FALSE or (( Q_ex x) . (i,(s - (x . (i + 1))))) = FALSE ) by XBOOLEAN:def 3;

          hence contradiction by A44;

        end;

        per cases ;

          suppose

           A45: (( Q_ex x) . (i,s)) = TRUE ;

          (x | i) exist_subset_sum_eq s by A1, defQ, A45;

          then

          consider I be set such that

           A46: I c= ( dom (x | i)) & ( Sum ( Seq ((x | i),I))) = s;

          

           A47: I c= ( dom (x | (i + 1))) by A46, A12;

          ( Seq ((x | i),I)) = ( Seq (x | I)) by A46, RELAT_1: 74, A8

          .= ( Seq ((x | (i + 1)),I)) by A11, A47, RELAT_1: 74;

          then (x | (i + 1)) exist_subset_sum_eq s by A47, A46;

          hence (( Q_ex x) . ((i + 1),s)) = TRUE by A2, A3, defQ;

        end;

          suppose (((x . (i + 1)) _le_ s) = TRUE & (( Q_ex x) . (i,(s - (x . (i + 1))))) = TRUE );

          then (x | i) exist_subset_sum_eq (s - (x . (i + 1))) by A1, defQ;

          then

          consider I be set such that

           A49: I c= ( dom (x | i)) & ( Sum ( Seq ((x | i),I))) = (s - (x . (i + 1)));

          set I1 = (I \/ {(i + 1)});

          

           A50: I c= ( dom (x | (i + 1))) by A12, A49;

          ( Seq ((x | (i + 1)),I1)) = (( Seq ((x | i),I)) ^ <*(x . (i + 1))*>) by A10, A49, A8, LM060;

          

          then ( Sum ( Seq ((x | (i + 1)),I1))) = (( Sum ( Seq ((x | i),I))) + (x . (i + 1))) by RVSUM_1: 74

          .= s by A49;

          then (x | (i + 1)) exist_subset_sum_eq s by A50, XBOOLE_1: 8, A14;

          hence (( Q_ex x) . ((i + 1),s)) = TRUE by A2, A3, defQ;

        end;

      end;

      hence thesis by A5, XBOOLEAN:def 3;

    end;