let F, G be Function; :: thesis: ( dom F = dom f & ( for x being object st x in dom F holds
F . x = c (#) (f . x) ) & dom G = dom f & ( for x being object st x in dom G holds
G . x = c (#) (f . x) ) implies F = G )
assume that
A1: dom F = dom f and
A2: for x being object st x in dom F holds
F . x = H₁(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds
G . x = H₁(x) ; :: thesis: F = G
thus dom F = dom G by A1, A3; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom F or F . b₁ = G . b₁ )
let x be object ; :: thesis: ( not x in dom F or 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