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_{1} being object holds

( not b_{1} in dom f or f . b_{1} = g . b_{1} )

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

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

( not 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