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₁ 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 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