let g, h be Function; :: thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g . x = Re (f . x) ) & dom h = dom f & ( for x being set st x in dom h holds
h . x = Re (f . x) ) implies g = h )
assume that
a1: dom g = dom f and
a2: for x being set st x in dom g holds
g . x = H₁(x) and
a3: dom h = dom f and
a4: for x being set st x in dom h holds
h . x = H₁(x) ; :: thesis: g = h

now

let x be set ; :: thesis: ( x in dom g implies g . x = h . x )
assume a5: x in dom g ; :: thesis: g . x = h . x
hence g . x = H₁(x) by a2
.= h . x by a1, a3, a4, a5 ;
:: thesis: verum

end;

hence g = h by a1, a3, FUNCT_1:9; :: thesis: verum