let F, G be Function; :: thesis: ( dom F = (dom f) /\ (dom g) & ( for x being object st x in dom F holds
F . x = (f . x) to_power (g . x) ) & dom G = (dom f) /\ (dom g) & ( for x being object st x in dom G holds
G . x = (f . x) to_power (g . x) ) implies F = G )
assume that
A1: dom F = (dom f) /\ (dom g) and
A2: for c being object st c in dom F holds
F . c = H₁(c) and
A3: dom G = (dom f) /\ (dom g) and
A4: for c being object st c in dom G holds
G . c = H₁(c) ; :: thesis: F = G

now :: thesis: for x being object st x in dom F holds
F . x = G . x

let x be object ; :: thesis: ( x in dom F implies F . x = G . x )
assume A5: x in dom F ; :: thesis: F . x = G . x
hence F . x = H₁(x) by A2
.= G . x by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence F = G by A1, A3, FUNCT_1:def 11; :: thesis: verum