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

let x be REAL -valued FinSequence; :: thesis: ( 1 <= len x implies (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' () )
assume A1: 1 <= len x ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' ()
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 ;
1 in Seg 1 ;
then A4: (x | 1) . 1 = x . 1 by FUNCT_1:49;
A5: {1} = dom (x | 1) by ;
A8: Seq ((x | 1),{1}) = (x | 1) | {1} by
.= <*(x . 1)*> by ;
per cases ( s <> 0 or s = 0 ) ;
suppose A9: s <> 0 ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' ()
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' ()
then A12: (x . 1) _eq_ s = TRUE by FUNCOP_1:def 8;
Sum (Seq ((x | 1),{1})) = s by ;
hence (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' () by Q1, A12, A5; :: thesis: verum
end;
suppose A13: x . 1 <> s ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' ()
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 ;
end;
hence (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' () by ; :: thesis: verum
end;
end;
end;
suppose A20: s = 0 ; :: thesis: (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' ()
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 ; :: thesis: verum
end;
hence (Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' () by ; :: thesis: verum
end;
end;