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 x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )