let v be object ; :: thesis: for V, A being set st A is_without_nonatomicND_wrt V & v in V holds
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
let V, A be set ; :: thesis: ( A is_without_nonatomicND_wrt V & v in V implies for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1) )
assume that
A1: A is_without_nonatomicND_wrt V and
A2: v in V ; :: thesis: for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
let d1 be NonatomicND of V,A; :: thesis: for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
let d2 be TypeSCNominativeData of V,A; :: thesis: dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
( not d1 in A & not naming (V,A,v,d2) in A ) by A1, Th3;
hence dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1) by A2, NOMIN_2:15; :: thesis: verum