let a1, a2, v1, v2 be object ; :: thesis: for V, A being set st {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds
global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)
let V, A be set ; :: thesis: ( {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A implies global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1) )
set D1 = v1 .--> a1;
set D2 = v2 .--> a2;
assume that
A1: {v1,v2} c= V and
A2: v1 <> v2 and
A3: ( not v1 .--> a1 in A & not v2 .--> a2 in A ) and
A4: ( a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A ) ; :: thesis: global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)
( v1 in V & v2 in V ) by A1, ZFMISC_1:32;
then A5: ( naming (V,A,v1,a1) = v1 .--> a1 & naming (V,A,v2,a2) = v2 .--> a2 ) by A4, Def13;
A6: {v1} \ {v2} = {v1} by A2, ZFMISC_1:14;
{v1} misses {v2} by A2, ZFMISC_1:11;
hence (v2,v1) --> (a2,a1) = (v2 .--> a2) \/ ((v1 .--> a1) | ((dom (v1 .--> a1)) \ (dom (v2 .--> a2)))) by A6, FUNCT_4:30, PARTFUN1:56
.= global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) by A3, A5, Th64 ;
:: thesis: verum