let v be object ; 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 ; ( 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
; 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; for L being Function st L = local_overlapping (V,A,d1,d2,v) holds
L . v = d2
let L be Function; ( L = local_overlapping (V,A,d1,d2,v) implies L . v = d2 )
assume A2:
L = local_overlapping (V,A,d1,d2,v)
; 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 )
;
L . v = d2then 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
;
verum end;