set f = ArProg (37,30);
for i being Nat holds (ArProg (37,30)) . i is not_representable_by_sum_or_difference_of_two_primes

proof

let i be Nat; :: thesis: (ArProg (37,30)) . i is not_representable_by_sum_or_difference_of_two_primes
(ArProg (37,30)) . i = 37 + (30 * i) by ArDefNth
.= 7 + (30 * (i + 1)) ;
hence (ArProg (37,30)) . i is not_representable_by_sum_or_difference_of_two_primes by Lemma73, NAT_1:12; :: thesis: verum

end;

hence ArProg (37,30) is with_terms_not_representable_by_sum_or_diff_of_two_primes ; :: thesis: verum