let X, Y be non empty TopSpace; for X0, X1 being non empty SubSpace of X
for f being Function of X,Y
for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let X0, X1 be non empty SubSpace of X; for f being Function of X,Y
for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let f be Function of X,Y; for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
let g be Function of X0,Y; ( g = f | X0 & X1 is SubSpace of X0 implies g | X1 = f | X1 )
assume A1:
g = f | X0
; ( not X1 is SubSpace of X0 or g | X1 = f | X1 )
assume A2:
X1 is SubSpace of X0
; g | X1 = f | X1
then A3:
the carrier of X1 c= the carrier of X0
by TSEP_1:4;
thus g | X1 =
g | the carrier of X1
by A2, Def5
.=
f | X1
by A1, A3, FUNCT_1:51
; verum