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;
A2: X1 is SubSpace of X1 union X2 by TSEP_1:22;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
A4: h | X1 = g | X1 by A2, Def4;
h | X2 = g | X2 by A3, Def4;
hence g = (g | X1) union (g | X2) by A4, Th138; :: thesis: verum