let x be REAL -valued FinSequence; :: thesis: ( x is positive implies for i being Nat
for s being Real st 1 <= i & 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)))))) )
assume AS0: x is positive ; :: thesis: for i being Nat
for s being Real st 1 <= i & 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))))))
let i be Nat; :: thesis: for s being Real st 1 <= i & 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))))))
let s be Real; :: thesis: ( 1 <= i & i < len x implies (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)))))) )
assume A1: ( 1 <= i & i < len x ) ; :: thesis: (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))))))
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 :: thesis: ( ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1)))))) = TRUE implies (Q_ex x) . ((i + 1),s) = TRUE )

assume (Q_ex x) . ((i + 1),s) = TRUE ; :: thesis: ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1)))))) = TRUE
then x | (i + 1) exist_subset_sum_eq s by A2, A3, defQ;
then consider I being set such that
A18: ( I c= dom (x | (i + 1)) & Sum (Seq ((x | (i + 1)),I)) = s ) ;

per cases ( I c= dom (x | i) or not I c= dom (x | i) ) ;

suppose A19: I c= dom (x | i) ; :: thesis: ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1)))))) = TRUE

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 ; :: thesis: verum

end;

suppose A22: not I c= dom (x | i) ; :: thesis: ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1)))))) = TRUE

A23: i + 1 in I

proof

assume A24: not i + 1 in I ; :: thesis: contradiction
I c= dom (x | i)

proof

let j be object ; :: according to TARSKI:def 3 :: thesis: ( not j in I or j in dom (x | i) )
assume A25: j in I ; :: thesis: j in dom (x | 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; :: thesis: verum

end;

hence contradiction by A22; :: thesis: verum

end;

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

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in I \ {(i + 1)} or k in Seg i )
assume W: k in I \ {(i + 1)} ; :: thesis: k in Seg i
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; :: thesis: verum

end;

A34: Seq ((x | (i + 1)),I) = (Seq ((x | i),(I \ {(i + 1)}))) ^ <*(x . (i + 1))*> by A10, A32, LM060, A28;
then Sum (Seq ((x | (i + 1)),I)) = (Sum (Seq ((x | i),(I \ {(i + 1)})))) + (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) ; :: thesis: s < Sum (Seq ((x | (i + 1)),I))

per cases ( I \ {(i + 1)} <> {} or I \ {(i + 1)} = {} ) ;

suppose A38: I \ {(i + 1)} <> {} ; :: thesis: s < Sum (Seq ((x | (i + 1)),I))

( x | i is positive & x | i <> {} ) by AS0, A1, LM090;
then ( Seq ((x | i),(I \ {(i + 1)})) is positive & Seq ((x | i),(I \ {(i + 1)})) <> {} ) by A32, A8, A38, LM100;
then s + 0 < (Sum (Seq ((x | i),(I \ {(i + 1)})))) + (x . (i + 1)) by A37, XREAL_1:8, LM080;
hence s < Sum (Seq ((x | (i + 1)),I)) by A34, RVSUM_1:74; :: thesis: verum

end;

suppose A39: I \ {(i + 1)} = {} ; :: thesis: s < Sum (Seq ((x | (i + 1)),I))

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 s < Sum (Seq ((x | (i + 1)),I)) by A37, RVSUM_1:73; :: thesis: verum

end;

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; :: thesis: verum

end;

end;

end;

assume A44: ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1)))))) = TRUE ; :: thesis: (Q_ex x) . ((i + 1),s) = 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 & not ( (x . (i + 1)) _le_ s = TRUE & (Q_ex x) . (i,(s - (x . (i + 1)))) = TRUE ) ) ; :: thesis: contradiction
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; :: thesis: verum

end;

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

suppose A45: (Q_ex x) . (i,s) = TRUE ; :: thesis: (Q_ex x) . ((i + 1),s) = TRUE

x | i exist_subset_sum_eq s by A1, defQ, A45;
then consider I being 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; :: thesis: verum

end;

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

then x | i exist_subset_sum_eq s - (x . (i + 1)) by A1, defQ;
then consider I being 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)),(I \/ {(i + 1)})) = (Seq ((x | i),I)) ^ <*(x . (i + 1))*> by A10, A49, A8, LM060;
then Sum (Seq ((x | (i + 1)),(I \/ {(i + 1)}))) = (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; :: thesis: verum

end;

end;

end;

hence (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)))))) by A5, XBOOLEAN:def 3; :: thesis: verum