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 & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = {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 & not d1 in A & not naming (V,A,v,d2) in 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 st v in V & not d1 in A & not naming (V,A,v,d2) in A holds
dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
let d2 be TypeSCNominativeData of V,A; :: thesis: ( v in V & not d1 in A & not naming (V,A,v,d2) in A implies dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1) )
assume A1: ( v in V & not d1 in A & not naming (V,A,v,d2) in A ) ; :: thesis: dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
per cases ( v in dom d1 or not v in dom d1 ) ;
suppose A2: v in dom d1 ; :: thesis: dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
then dom (local_overlapping (V,A,d1,d2,v)) = dom d1 by A1, Th13;
hence dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1) by A2, ZFMISC_1:40; :: thesis: verum
end;
suppose not v in dom d1 ; :: thesis: dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)
hence dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1) by A1, Th12; :: thesis: verum
end;
end;