let x be REAL -valued FinSequence; :: thesis: for Q1, Q2 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 Q1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q1 . (i,s) = FALSE ) ) ) & ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q2 . (i,s) = FALSE ) ) ) holds
Q1 = Q2
set L = Seg (len x);
let Q1, Q2 be Function of [:(Seg (len x)),REAL:],BOOLEAN; :: thesis: ( ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q1 . (i,s) = FALSE ) ) ) & ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q2 . (i,s) = FALSE ) ) ) implies Q1 = Q2 )
assume that
A1: for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q1 . (i,s) = FALSE ) ) and
A2: for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q2 . (i,s) = FALSE ) ) ; :: thesis: Q1 = Q2
for i, s being set st i in Seg (len x) & s in REAL holds
Q1 . (i,s) = Q2 . (i,s)
proof
let i, s be set ; :: thesis: ( i in Seg (len x) & s in REAL implies Q1 . (i,s) = Q2 . (i,s) )
assume A3: ( i in Seg (len x) & s in REAL ) ; :: thesis: Q1 . (i,s) = Q2 . (i,s)
then reconsider i0 = i as Nat ;
reconsider s0 = s as Real by A3;
A4: ( 1 <= i0 & i0 <= len x ) by A3, FINSEQ_1:1;
per cases ( x | i0 exist_subset_sum_eq s0 or not x | i0 exist_subset_sum_eq s0 ) ;
suppose A5: x | i0 exist_subset_sum_eq s0 ; :: thesis: Q1 . (i,s) = Q2 . (i,s)
hence Q1 . (i,s) = TRUE by A1, A4
.= Q2 . (i,s) by A2, A4, A5 ;
:: thesis: verum
end;
suppose A6: not x | i0 exist_subset_sum_eq s0 ; :: thesis: Q1 . (i,s) = Q2 . (i,s)
hence Q1 . (i,s) = FALSE by A1, A4
.= Q2 . (i,s) by A2, A4, A6 ;
:: thesis: verum
end;
end;
end;
hence Q1 = Q2 ; :: thesis: verum