let v, v1 be object ; :: thesis: for V, A being set
for d1 being NonatomicND of V,A
for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1
let V, A be set ; :: thesis: for d1 being NonatomicND of V,A
for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1
let d1 be NonatomicND of V,A; :: thesis: for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1
let T be TypeSCNominativeData of V,A; :: thesis: ( A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 implies (local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1 )
assume that
A1: A is_without_nonatomicND_wrt V and
A2: ( v in V & v <> v1 ) ; :: thesis: ( not v1 in dom d1 or (local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1 )
( not d1 in A & not naming (V,A,v,T) in A ) by A1, NOMIN_4:3;
hence ( not v1 in dom d1 or (local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1 ) by A2, NOMIN_2:12; :: thesis: verum