deffunc H₁( Element of D) -> Element of the carrier of Y = lim (H # $1);
thus for f1, f2 being PartFunc of D, the carrier of Y 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