let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds
local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds
local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))
let d be TypeSCNominativeData of V,A; :: thesis: for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds
local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))
let d1 be NonatomicND of V,A; :: thesis: ( v in V & A is_without_nonatomicND_wrt V implies local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v)) )
set L = local_overlapping (V,A,d1,d,v);
set D = denaming (V,A,v);
A1: dom (denaming (V,A,v)) = { d where d is NonatomicND of V,A : v in dom d } by NOMIN_1:def 18;
A2: local_overlapping (V,A,d1,d,v) is NonatomicND of V,A by NOMIN_2:9;
assume ( v in V & A is_without_nonatomicND_wrt V ) ; :: thesis: local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))
then A3: dom (local_overlapping (V,A,d1,d,v)) = {v} \/ (dom d1) by Th4;
v in {v} by TARSKI:def 1;
then v in dom (local_overlapping (V,A,d1,d,v)) by A3, XBOOLE_0:def 3;
hence local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v)) by A1, A2; :: thesis: verum