let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X
for g being Function of (X1 union X2),Y holds g = (g | X1) union (g | X2)
let X1, X2 be non empty SubSpace of X; :: thesis: for g being Function of (X1 union X2),Y holds g = (g | X1) union (g | X2)
let g be Function of (X1 union X2),Y; :: thesis: g = (g | X1) union (g | X2)

now :: thesis: ( X1 meets X2 implies (g | X1) | (X1 meet X2) = (g | X2) | (X1 meet X2) )

assume A1: X1 meets X2 ; :: thesis: (g | X1) | (X1 meet X2) = (g | X2) | (X1 meet X2)
then A2: X1 meet X2 is SubSpace of X2 by TSEP_1:27;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;
X1 meet X2 is SubSpace of X1 by A1, TSEP_1:27;
hence (g | X1) | (X1 meet X2) = g | (X1 meet X2) by A4, Th72
.= (g | X2) | (X1 meet X2) by A2, A3, Th72 ;
:: thesis: verum

end;

hence g = (g | X1) union (g | X2) by Def12; :: thesis: verum