set X = dom f;
deffunc H₂( Element of C) -> object = r * (f . $1);
thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = H₂(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds
G . c = H₂(c) ) holds
F = G from SEQ_1:sch 4(); :: thesis: verum