deffunc H₁( Nat) -> set = 1 / (primenumber $1);
thus ( ex seq being Real_Sequence st
for n being Nat holds seq . n = H₁(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = H₁(n) ) & ( for n being Nat holds seq2 . n = H₁(n) ) holds
seq1 = seq2 ) ) from NUMPOLY1:sch 1(); :: thesis: verum