let a1, a2, v be object ; :: thesis: for V, A being set st v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds

global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

let V, A be set ; :: thesis: ( v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A implies global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2 )

assume that

A1: v in V and

A2: ( not v .--> a1 in A & not v .--> a2 in A ) and

A3: ( a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A ) ; :: thesis: global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

( naming (V,A,v,a1) = v .--> a1 & naming (V,A,v,a2) = v .--> a2 ) by A1, A3, Def13;

hence global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2 by A2, Th65; :: thesis: verum

global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

let V, A be set ; :: thesis: ( v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A implies global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2 )

assume that

A1: v in V and

A2: ( not v .--> a1 in A & not v .--> a2 in A ) and

A3: ( a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A ) ; :: thesis: global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2

( naming (V,A,v,a1) = v .--> a1 & naming (V,A,v,a2) = v .--> a2 ) by A1, A3, Def13;

hence global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2 by A2, Th65; :: thesis: verum