:: deftheorem Def1 defines union TMAP_1:def 1 :
for A, B being non empty set
for A1, A2 being non empty Subset of A
for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
for b₇ being Function of (A1 \/ A2),B holds
( b₇ = f1 union f2 iff ( b₇ | A1 = f1 & b₇ | A2 = f2 ) );