let v be object ; :: thesis: for V, A being set
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = dom d1
let V, A be set ; :: thesis: for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = dom d1
let d1 be NonatomicND of V,A; :: thesis: for d2 being TypeSCNominativeData of V,A st v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = dom d1
let d2 be TypeSCNominativeData of V,A; :: thesis: ( v in V & v in dom d1 & not d1 in A & not naming (V,A,v,d2) in A implies dom (local_overlapping (V,A,d1,d2,v)) = dom d1 )
assume that
A1: v in V and
A2: v in dom d1 and
A3: ( not d1 in A & not naming (V,A,v,d2) in A ) ; :: thesis: dom (local_overlapping (V,A,d1,d2,v)) = dom d1
set n = naming (V,A,v,d2);
A4: naming (V,A,v,d2) = v .--> d2 by A1, NOMIN_1:def 13;
A5: (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2)))))) = dom d1

proof

A6: dom (naming (V,A,v,d2)) c= dom d1 by A2, A4, ZFMISC_1:31;
dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))) c= dom d1 by RELAT_1:60;
hence (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2)))))) c= dom d1 by A6, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: dom d1 c= (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom d1 or x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2)))))) )
assume A7: x in dom d1 ; :: thesis: x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))))

per cases ( x = v or x <> v ) ;

suppose x = v ; :: thesis: x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))))

then x in dom (naming (V,A,v,d2)) by A4, TARSKI:def 1;
hence x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2)))))) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x <> v ; :: thesis: x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))))

then not x in dom (naming (V,A,v,d2)) by A4, TARSKI:def 1;
then x in (dom d1) \ (dom (naming (V,A,v,d2))) by A7, XBOOLE_0:def 5;
then x in dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))) by RELAT_1:57;
hence x in (dom (naming (V,A,v,d2))) \/ (dom (d1 | ((dom d1) \ (dom (naming (V,A,v,d2)))))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

local_overlapping (V,A,d1,d2,v) = (naming (V,A,v,d2)) \/ (d1 | ((dom d1) \ (dom (naming (V,A,v,d2))))) by A3, NOMIN_1:64;
hence dom (local_overlapping (V,A,d1,d2,v)) = dom d1 by A5, XTUPLE_0:23; :: thesis: verum