let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
for g being Function of X,Y holds g = (g | X1) union (g | X2)
let X1, X2 be non empty SubSpace of X; :: thesis: ( X = X1 union X2 implies for g being Function of X,Y holds g = (g | X1) union (g | X2) )
assume A1: X = X1 union X2 ; :: thesis: for g being Function of X,Y holds g = (g | X1) union (g | X2)
let g be Function of X,Y; :: thesis: g = (g | X1) union (g | X2)
reconsider h = g as Function of (X1 union X2),Y by A1;
X2 is SubSpace of X1 union X2 by TSEP_1:22;
then A2: h | X2 = g | X2 by Def5;
X1 is SubSpace of X1 union X2 by TSEP_1:22;
then h | X1 = g | X1 by Def5;
hence g = (g | X1) union (g | X2) by A2, Th126; :: thesis: verum