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)

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

hence
Q1 = Q2
; :: thesis: verum
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;

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

end;