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