let F, G be Function; :: thesis: ( dom F = dom X & ( for x being object st x in dom X holds
F . x = [(X . x),((g . x) . d)] ) & dom G = dom X & ( for x being object st x in dom X holds
G . x = [(X . x),((g . x) . d)] ) implies F = G )
assume that
A2: dom F = dom X and
A3: for x being object st x in dom X holds
F . x = [(X . x),((g . x) . d)] and
A4: dom G = dom X and
A5: for x being object st x in dom X holds
G . x = [(X . x),((g . x) . d)] ; :: thesis: F = G
thus dom F = dom G by A2, A4; :: 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 A6: x in dom F ; :: thesis: F . x = G . x
hence F . x = [(X . x),((g . x) . d)] by A2, A3
.= G . x by A2, A5, A6 ;
:: thesis: verum