let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for d1 being NonatomicND of V,A
for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds
(local_overlapping (V,A,d1,d,z)) . z = d1 . v
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for d1 being NonatomicND of V,A
for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds
(local_overlapping (V,A,d1,d,z)) . z = d1 . v
let d be TypeSCNominativeData of V,A; :: thesis: for d1 being NonatomicND of V,A
for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds
(local_overlapping (V,A,d1,d,z)) . z = d1 . v
let d1 be NonatomicND of V,A; :: thesis: for z being Element of V st not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 holds
(local_overlapping (V,A,d1,d,z)) . z = d1 . v
let z be Element of V; :: thesis: ( not V is empty & v in dom d1 & d = (denaming (V,A,v)) . d1 implies (local_overlapping (V,A,d1,d,z)) . z = d1 . v )
assume A1: not V is empty ; :: thesis: ( not v in dom d1 or not d = (denaming (V,A,v)) . d1 or (local_overlapping (V,A,d1,d,z)) . z = d1 . v )
set Dj = denaming (V,A,v);
assume that
A2: v in dom d1 and
A3: d = (denaming (V,A,v)) . d1 ; :: thesis: (local_overlapping (V,A,d1,d,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 A4: d1 in dom (denaming (V,A,v)) by A2;
thus (local_overlapping (V,A,d1,d,z)) . z = (denaming (V,A,v)) . d1 by A1, A3, Th10
.= denaming (v,d1) by A4, NOMIN_1:def 18
.= d1 . v by A2, NOMIN_1:def 12 ; :: thesis: verum