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 S1[ 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 & S1[u,t,z] )
proof
let u, t be object ; :: thesis: ( u in Seg (len x) & t in REAL implies ex z being object st
( z in BOOLEAN & S1[u,t,z] ) )
assume A2: ( u in Seg (len x) & t in REAL ) ; :: thesis: ex z being object st
( z in BOOLEAN & S1[u,t,z] )
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 ) ;
suppose A3: x | i exist_subset_sum_eq s ; :: thesis: ex z being object st
( z in BOOLEAN & S1[u,t,z] )
take z = TRUE ; :: thesis: ( z in BOOLEAN & S1[u,t,z] )
thus z in BOOLEAN ; :: thesis: S1[u,t,z]
thus S1[u,t,z] by A3; :: thesis: verum
end;
suppose A4: not x | i exist_subset_sum_eq s ; :: thesis: ex z being object st
( z in BOOLEAN & S1[u,t,z] )
take z = FALSE ; :: thesis: ( z in BOOLEAN & S1[u,t,z] )
thus z in BOOLEAN ; :: thesis: S1[u,t,z]
thus S1[u,t,z] by A4; :: thesis: verum
end;
end;
end;
consider Q being Function of [:(Seg (len x)),REAL:],BOOLEAN such that
A5: for x, y being object st x in Seg (len x) & y in REAL holds
S1[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