:: deftheorem Def12 defines union TMAP_1:def 12 :
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for b₇ being Function of (X1 union X2),Y holds
( b₇ = f1 union f2 iff ( b₇ | X1 = f1 & b₇ | X2 = f2 ) );