let v be object ; :: thesis: for V, A being set
for z being Element of V
for d1 being NonatomicND of V,A st not V is empty & v in dom d1 holds
(local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v
let V, A be set ; :: thesis: for z being Element of V
for d1 being NonatomicND of V,A st not V is empty & v in dom d1 holds
(local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v
let z be Element of V; :: thesis: for d1 being NonatomicND of V,A st not V is empty & v in dom d1 holds
(local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v
let d1 be NonatomicND of V,A; :: thesis: ( not V is empty & v in dom d1 implies (local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v )
assume A1: not V is empty ; :: thesis: ( not v in dom d1 or (local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v )
set Dj = denaming (V,A,v);
assume A2: v in dom d1 ; :: thesis: (local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v
dom (denaming (V,A,v)) = { d where d is NonatomicND of V,A : v in dom d } by NOMIN_1:def 18;
then A3: d1 in dom (denaming (V,A,v)) by A2;
then (denaming (V,A,v)) . d1 is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
hence (local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = (denaming (V,A,v)) . d1 by A1, NOMIN_2:10
.= denaming (v,d1) by A3, NOMIN_1:def 18
.= d1 . v by A2, NOMIN_1:def 12 ;
:: thesis: verum