let v be object ; :: thesis: for V, A being set st v in V holds
for d1, d2 being TypeSCNominativeData of V,A
for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2
let V, A be set ; :: thesis: ( v in V implies for d1, d2 being TypeSCNominativeData of V,A
for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2 )
assume A1: v in V ; :: thesis: for d1, d2 being TypeSCNominativeData of V,A
for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2
let d1, d2 be TypeSCNominativeData of V,A; :: thesis: for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2
let L be Function; :: thesis: ( L = local_overlapping (V,A,d1,d2,v) implies L . v = d2 )
assume A2: L = local_overlapping (V,A,d1,d2,v) ; :: thesis: L . v = d2
A4: naming (V,A,v,d2) = v .--> d2 by A1, NOMIN_1:def 13;
A6: v in {v} by TARSKI:def 1;
A7: (v .--> d2) . v = d2 by FUNCOP_1:72;

per cases ( ( not d1 in A & not naming (V,A,v,d2) in A ) or d1 in A or naming (V,A,v,d2) in A ) ;

suppose ( not d1 in A & not naming (V,A,v,d2) in A ) ; :: thesis: L . v = d2

then consider f1, f2 being Function such that
f1 = d1 and
A8: f2 = naming (V,A,v,d2) and
A9: L = f2 \/ (f1 | ((dom f1) \ (dom f2))) by A2, NOMIN_1:def 16;
thus L . v = f2 . v by A4, A6, A8, A9, GRFUNC_1:15
.= d2 by A8, A4, A6, FUNCOP_1:7 ; :: thesis: verum

end;

suppose ( d1 in A or naming (V,A,v,d2) in A ) ; :: thesis: L . v = d2

hence L . v = d2 by A4, A7, A2, NOMIN_1:def 16; :: thesis: verum

end;

end;