let a1, a2, v, v1, v2 be object ; :: thesis: for V, A being set st {v,v1,v2} c= V & v <> v1 & a2 in A & not v1 .--> a1 in A & not v .--> (v2 .--> a2) in A & a1 is TypeSCNominativeData of V,A holds
local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1)
let V, A be set ; :: thesis: ( {v,v1,v2} c= V & v <> v1 & a2 in A & not v1 .--> a1 in A & not v .--> (v2 .--> a2) in A & a1 is TypeSCNominativeData of V,A implies local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1) )
set d1 = v1 .--> a1;
set d2 = v2 .--> a2;
assume that
A1: {v,v1,v2} c= V and
A2: v <> v1 and
A3: a2 in A and
A4: not v1 .--> a1 in A and
A5: not v .--> (v2 .--> a2) in A and
A6: a1 is TypeSCNominativeData of V,A ; :: thesis: local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1)
A7: v in {v,v1,v2} by ENUMSET1:def 1;
v2 in {v,v1,v2} by ENUMSET1:def 1;
then A8: ND_ex_1 (v2,a2) is TypeSCNominativeData of V,A by A1, A3, Th46;
then A9: naming (V,A,v,(v2 .--> a2)) = v .--> (v2 .--> a2) by A1, A7, Def13;
{v1,v} c= V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v1,v} or x in V )
assume x in {v1,v} ; :: thesis: x in V
then ( x = v1 or x = v ) by TARSKI:def 2;
then x in {v,v1,v2} by ENUMSET1:def 1;
hence x in V by A1; :: thesis: verum

end;

hence local_overlapping (V,A,(v1 .--> a1),(v2 .--> a2),v) = (v,v1) --> ((v2 .--> a2),a1) by A4, A5, A6, A2, A8, A9, Th68; :: thesis: verum