let v, v1 be object ; for V, A being set st v in V & v <> v1 holds
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1
let V, A be set ; ( v in V & v <> v1 implies for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1 )
assume that
A1:
v in V
and
A2:
v <> v1
; for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1
let d1 be NonatomicND of V,A; for d2 being TypeSCNominativeData of V,A st v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A holds
(local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1
let d2 be TypeSCNominativeData of V,A; ( v1 in dom d1 & not d1 in A & not naming (V,A,v,d2) in A implies (local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1 )
assume that
A4:
v1 in dom d1
and
A5:
( not d1 in A & not naming (V,A,v,d2) in A )
; (local_overlapping (V,A,d1,d2,v)) . v1 = d1 . v1
A7:
naming (V,A,v,d2) = v .--> d2
by A1, NOMIN_1:def 13;
consider f1, f2 being Function such that
A10:
f1 = d1
and
A11:
f2 = naming (V,A,v,d2)
and
A12:
local_overlapping (V,A,d1,d2,v) = f2 \/ (f1 | ((dom f1) \ (dom f2)))
by A5, NOMIN_1:def 16;
not v1 in {v}
by A2, TARSKI:def 1;
then
v1 in (dom f1) \ (dom f2)
by A4, A7, A10, A11, XBOOLE_0:def 5;
then A13:
v1 in dom (f1 | ((dom f1) \ (dom f2)))
by RELAT_1:57;
hence (local_overlapping (V,A,d1,d2,v)) . v1 =
(f1 | ((dom f1) \ (dom f2))) . v1
by A12, GRFUNC_1:15
.=
d1 . v1
by A10, A13, FUNCT_1:47
;
verum