let f, g be PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)); ( 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)
; f = g
thus
dom f = dom g
by A9, A11; 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 A13:
D in dom f
; 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
;
verum