deffunc H₁( Element of D) -> object = lim (H # $1);
thus for f1, f2 being PartFunc of D,REAL st dom f1 = X & ( for x being Element of D st x in dom f1 holds
f1 . x = H₁(x) ) & dom f2 = X & ( for x being Element of D st x in dom f2 holds
f2 . x = H₁(x) ) holds
f1 = f2 from SEQ_1:sch 4(); :: thesis: verum