let X, Y be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X

for f being Function of X,Y

for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let X0 be non empty SubSpace of X; :: thesis: for f being Function of X,Y

for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let f be Function of X,Y; :: thesis: for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let f0 be Function of X0,Y; :: thesis: ( ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) implies f | X0 = f0 )

the carrier of X0 is Subset of X by TSEP_1:1;

hence ( ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) implies f | X0 = f0 ) by FUNCT_2:96; :: thesis: verum

for f being Function of X,Y

for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let X0 be non empty SubSpace of X; :: thesis: for f being Function of X,Y

for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let f be Function of X,Y; :: thesis: for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) holds

f | X0 = f0

let f0 be Function of X0,Y; :: thesis: ( ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) implies f | X0 = f0 )

the carrier of X0 is Subset of X by TSEP_1:1;

hence ( ( for x being Point of X st x in the carrier of X0 holds

f . x = f0 . x ) implies f | X0 = f0 ) by FUNCT_2:96; :: thesis: verum