let f, g be PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)); :: thesis: ( dom f = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

f . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) & dom g = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

g . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) implies f = g )

assume that

A9: dom f = [:((ND (V,A)) \ A),(ND (V,A)):] and

A10: for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

f . [d1,d2] = local_overlapping (V,A,d1,d2,v) and

A11: dom g = [:((ND (V,A)) \ A),(ND (V,A)):] and

A12: for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

g . [d1,d2] = local_overlapping (V,A,d1,d2,v) ; :: thesis: f = g

thus dom f = dom g by A9, A11; :: 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 A13: D in dom f ; :: thesis: f . D = g . D

consider D1, D2 being object such that

A14: ( D1 in (ND (V,A)) \ A & D2 in ND (V,A) ) and

A15: D = [D1,D2] by A9, A13, ZFMISC_1:def 2;

reconsider D1 = D1 as NonatomicND of V,A by A14, Th43;

A16: not D1 in A by A14, XBOOLE_0:def 5;

hence f . D = local_overlapping (V,A,D1,D2,v) by A10, A14, A15

.= g . D by A12, A14, A15, A16 ;

:: thesis: verum

for d2 being object st not d1 in A & d2 in ND (V,A) holds

f . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) & dom g = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

g . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) implies f = g )

assume that

A9: dom f = [:((ND (V,A)) \ A),(ND (V,A)):] and

A10: for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

f . [d1,d2] = local_overlapping (V,A,d1,d2,v) and

A11: dom g = [:((ND (V,A)) \ A),(ND (V,A)):] and

A12: for d1 being NonatomicND of V,A

for d2 being object st not d1 in A & d2 in ND (V,A) holds

g . [d1,d2] = local_overlapping (V,A,d1,d2,v) ; :: thesis: f = g

thus dom f = dom g by A9, A11; :: 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 A13: D in dom f ; :: thesis: f . D = g . D

consider D1, D2 being object such that

A14: ( D1 in (ND (V,A)) \ A & D2 in ND (V,A) ) and

A15: D = [D1,D2] by A9, A13, ZFMISC_1:def 2;

reconsider D1 = D1 as NonatomicND of V,A by A14, Th43;

A16: not D1 in A by A14, XBOOLE_0:def 5;

hence f . D = local_overlapping (V,A,D1,D2,v) by A10, A14, A15

.= g . D by A12, A14, A15, A16 ;

:: thesis: verum