let s be Real; :: thesis: for x being REAL -valued FinSequence st 1 <= len x holds
(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)
let x be REAL -valued FinSequence; :: thesis: ( 1 <= len x implies (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0) )
assume A1: 1 <= len x ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)
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 ( s <> 0 or s = 0 ) ;

suppose A9: s <> 0 ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

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

per cases ( x . 1 = s or x . 1 <> s ) ;

suppose A11: x . 1 = s ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

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

end;

suppose A13: x . 1 <> s ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

not x | 1 exist_subset_sum_eq s

proof

assume x | 1 exist_subset_sum_eq s ; :: thesis: contradiction
then consider I being set such that
A15: ( I c= dom (x | 1) & Sum (Seq ((x | 1),I)) = s ) ;
dom (x | 1) = {1} by A1, Lemacik1;

per cases then ( I = {} or I = {1} ) by A15, ZFMISC_1:33;

suppose I = {} ; :: thesis: contradiction

hence contradiction by A9, A15, RVSUM_1:72; :: thesis: verum

end;

suppose I = {1} ; :: thesis: contradiction

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

end;

end;

end;

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

end;

end;

end;

suppose A20: s = 0 ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

then A21: s _eq_ 0 = TRUE by FUNCOP_1:def 8;
x | 1 exist_subset_sum_eq s

proof

take {} ; :: according to PRSUBSET:def 2 :: thesis: ( {} c= dom (x | 1) & Sum (Seq ((x | 1),{})) = s )
thus ( {} c= dom (x | 1) & Sum (Seq ((x | 1),{})) = s ) by A20, RVSUM_1:72; :: thesis: verum

end;

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

end;

end;