let V, A be set ; :: thesis: for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A holds
global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))
let D1, D2 be NonatomicND of V,A; :: thesis: ( not D1 in A & not D2 in A implies global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2))) )
A1: D1 is TypeSCNominativeData of V,A by Def6;
A2: D2 is TypeSCNominativeData of V,A by Def6;
assume ( not D1 in A & not D2 in A ) ; :: thesis: global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))
then ex f1, f2 being Function st
( f1 = D1 & f2 = D2 & global_overlapping (V,A,D1,D2) = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) by A1, A2, Def16;
hence global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2))) ; :: thesis: verum