let f, g be PartFunc of (ND (V,A)),(ND (V,A)); :: thesis: ( 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) ; :: thesis: f = g
thus dom f = dom g by A6, A8; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f or f . b₁ = g . b₁ )
let D be object ; :: thesis: ( not D in dom f or f . D = g . D )
assume A10: D in dom f ; :: thesis: 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 ; :: thesis: verum