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