:: deftheorem 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 holds f1 union f2 = f1 +* f2;