deffunc H₁( Element of NAT ) -> set = (n choose $1) * (n ^ (- $1));
thus ( ex seq being Real_Sequence st
for n being Element of NAT holds seq . n = H₁(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H₁(n) ) & ( for n being Element of NAT holds seq2 . n = H₁(n) ) holds
seq1 = seq2 ) ) from IRRAT_1:sch 1(); :: thesis: verum