let F, G be Function; ( 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)]
; F = G
thus
dom F = dom G
by A2, A4; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom F or F . b1 = G . b1 )
let x be object ; ( not x in dom F or F . x = G . x )
assume A6:
x in dom F
; F . x = G . x
hence F . x =
[(X . x),((g . x) . d)]
by A2, A3
.=
G . x
by A2, A5, A6
;
verum