let g, h be Function; :: thesis: ( dom g = dom f & ( for x being object st x in dom g holds
g . x = Im (f . x) ) & dom h = dom f & ( for x being object st x in dom h holds
h . x = Im (f . x) ) implies g = h )
assume that
A6: dom g = dom f and
A7: for x being object st x in dom g holds
g . x = H₂(x) and
A8: dom h = dom f and
A9: for x being object st x in dom h holds
h . x = H₂(x) ; :: thesis: g = h

now :: thesis: for x being object st x in dom g holds
g . x = h . x

let x be object ; :: thesis: ( x in dom g implies g . x = h . x )
assume A10: x in dom g ; :: thesis: g . x = h . x
hence g . x = H₂(x) by A7
.= h . x by A6, A8, A9, A10 ;
:: thesis: verum

end;

hence g = h by A6, A8, FUNCT_1:2; :: thesis: verum