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)

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) )

hence
g = (g | X1) union (g | X2)
by Def12; :: thesis: verumassume 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;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