per cases ( ( not d1 in A & not d2 in A ) or d1 in A or d2 in A ) ;

suppose that A3: not d1 in A and
A4: not d2 in A ; :: thesis: ( ( not d1 in A & not d2 in A implies ex b₁ being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b₁ being TypeSCNominativeData of V,A st b₁ = d2 ) )

reconsider f1 = d1 as Function by A1, A3, Def6;
reconsider f2 = d2 as Function by A2, A4, Def6;
set X = (dom f1) \ (dom f2);
set D = f2 \/ (f1 | ((dom f1) \ (dom f2)));
f2 \/ (f1 | ((dom f1) \ (dom f2))) is NonatomicND of V,A

proof

d1 is NonatomicND of V,A by A1, A3, Def6;
then A5: f1 | ((dom f1) \ (dom f2)) is NonatomicND of V,A by Th32, RELAT_1:59;
A6: d2 is NonatomicND of V,A by A2, A4, Def6;
A7: dom (f1 | ((dom f1) \ (dom f2))) = (dom f1) \ (dom f2) by RELAT_1:62;
(dom f1) \ (dom f2) misses dom f2 by XBOOLE_1:79;
hence f2 \/ (f1 | ((dom f1) \ (dom f2))) is NonatomicND of V,A by A5, A6, A7, Th36, PARTFUN1:56; :: thesis: verum

end;

hence ( ( not d1 in A & not d2 in A implies ex b₁ being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b₁ being TypeSCNominativeData of V,A st b₁ = d2 ) ) by A2; :: thesis: verum

end;

suppose ( d1 in A or d2 in A ) ; :: thesis: ( ( not d1 in A & not d2 in A implies ex b₁ being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b₁ being TypeSCNominativeData of V,A st b₁ = d2 ) )

hence ( ( not d1 in A & not d2 in A implies ex b₁ being TypeSCNominativeData of V,A ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₁ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) & ( ( d1 in A or d2 in A ) implies ex b₁ being TypeSCNominativeData of V,A st b₁ = d2 ) ) by A2; :: thesis: verum

end;

end;