let f, g be PartFunc of (ND (V,A)),(ND (V,A)); ( dom f = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom f holds
f . D = denaming (v,D) ) & dom g = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom g holds
g . D = denaming (v,D) ) implies f = g )
assume that
A6:
dom f = { d where d is NonatomicND of V,A : v in dom d }
and
A7:
for D being NonatomicND of V,A st D in dom f holds
f . D = denaming (v,D)
and
A8:
dom g = { d where d is NonatomicND of V,A : v in dom d }
and
A9:
for D being NonatomicND of V,A st D in dom g holds
g . D = denaming (v,D)
; f = g
thus
dom f = dom g
by A6, A8; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom f or f . b1 = g . b1 )
let D be object ; ( not D in dom f or f . D = g . D )
assume A10:
D in dom f
; f . D = g . D
then consider D1 being NonatomicND of V,A such that
A11:
( D = D1 & v in dom D1 )
by A6;
thus f . D =
denaming (v,D1)
by A7, A10, A11
.=
g . D
by A6, A8, A9, A10, A11
; verum