thus for h, g being PartFunc of C,COMPLEX st dom h = dom f & ( for c being Element of C st c in dom h holds
h . c = H₁(c) ) & dom g = dom f & ( for c being Element of C st c in dom g holds
g . c = H₁(c) ) holds
h = g from SEQ_1:sch 4(); :: thesis: verum