let x be REAL -valued FinSequence; :: thesis: ex Q being Function of [:(Seg (len x)),REAL:],BOOLEAN st

for i being Nat

for s being Real st 1 <= i & 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 ) )

set L = Seg (len x);

defpred S_{1}[ object , object , object ] means ex i being Nat ex s being 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 being object st u in Seg (len x) & t in REAL holds

ex z being object st

( z in BOOLEAN & S_{1}[u,t,z] )

A5: for x, y being object st x in Seg (len x) & y in REAL holds

S_{1}[x,y,Q . (x,y)]
from BINOP_1:sch 1(A1);

take Q ; :: thesis: for i being Nat

for s being Real st 1 <= i & 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 ) )

let i be Nat; :: thesis: for s being Real st 1 <= i & 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 ) )

let s be Real; :: thesis: ( 1 <= i & i <= len x implies ( ( 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 ) ) )

assume A6: ( 1 <= i & i <= len x ) ; :: thesis: ( ( 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 ) )

i in Seg (len x) by A6;

then ex i0 being Nat ex s0 being 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 ( ( 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 ) ) ; :: thesis: verum

for i being Nat

for s being Real st 1 <= i & 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 ) )

set L = Seg (len x);

defpred S

( $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 being object st u in Seg (len x) & t in REAL holds

ex z being object st

( z in BOOLEAN & S

proof

consider Q being Function of [:(Seg (len x)),REAL:],BOOLEAN such that
let u, t be object ; :: thesis: ( u in Seg (len x) & t in REAL implies ex z being object st

( z in BOOLEAN & S_{1}[u,t,z] ) )

assume A2: ( u in Seg (len x) & t in REAL ) ; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[u,t,z] )

then reconsider i = u as Nat ;

reconsider s = t as Real by A2;

end;( z in BOOLEAN & S

assume A2: ( u in Seg (len x) & t in REAL ) ; :: thesis: ex z being object st

( z in BOOLEAN & S

then reconsider i = u as Nat ;

reconsider s = t as Real by A2;

per cases
( x | i exist_subset_sum_eq s or not x | i exist_subset_sum_eq s )
;

end;

suppose A3:
x | i exist_subset_sum_eq s
; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[u,t,z] )

( z in BOOLEAN & S

take z = TRUE ; :: thesis: ( z in BOOLEAN & S_{1}[u,t,z] )

thus z in BOOLEAN ; :: thesis: S_{1}[u,t,z]

thus S_{1}[u,t,z]
by A3; :: thesis: verum

end;thus z in BOOLEAN ; :: thesis: S

thus S

suppose A4:
not x | i exist_subset_sum_eq s
; :: thesis: ex z being object st

( z in BOOLEAN & S_{1}[u,t,z] )

( z in BOOLEAN & S

take z = FALSE ; :: thesis: ( z in BOOLEAN & S_{1}[u,t,z] )

thus z in BOOLEAN ; :: thesis: S_{1}[u,t,z]

thus S_{1}[u,t,z]
by A4; :: thesis: verum

end;thus z in BOOLEAN ; :: thesis: S

thus S

A5: for x, y being object st x in Seg (len x) & y in REAL holds

S

take Q ; :: thesis: for i being Nat

for s being Real st 1 <= i & 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 ) )

let i be Nat; :: thesis: for s being Real st 1 <= i & 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 ) )

let s be Real; :: thesis: ( 1 <= i & i <= len x implies ( ( 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 ) ) )

assume A6: ( 1 <= i & i <= len x ) ; :: thesis: ( ( 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 ) )

i in Seg (len x) by A6;

then ex i0 being Nat ex s0 being 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 ( ( 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 ) ) ; :: thesis: verum