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 ;

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

end;

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;

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

end;

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

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

end;proof

hence
(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)
by A13, A10, Q1, FUNCOP_1:def 8; :: thesis: verum
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;

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

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

end;x | 1 exist_subset_sum_eq s

proof

hence
(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)
by A21, A1, defQ; :: thesis: verum
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;thus ( {} c= dom (x | 1) & Sum (Seq ((x | 1),{})) = s ) by A20, RVSUM_1:72; :: thesis: verum