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

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