let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for f0 being Function of X0,X st ( for x being Point of X st x in the carrier of X0 holds
x = f0 . x ) holds
incl X0 = f0
let X0 be non empty SubSpace of X; :: thesis: for f0 being Function of X0,X st ( for x being Point of X st x in the carrier of X0 holds
x = f0 . x ) holds
incl X0 = f0
let f0 be Function of X0,X; :: thesis: ( ( for x being Point of X st x in the carrier of X0 holds
x = f0 . x ) implies incl X0 = f0 )
assume for x being Point of X st x in the carrier of X0 holds
x = f0 . x ; :: thesis: incl X0 = f0
then for x being Point of X st x in the carrier of X0 holds
(id X) . x = f0 . x ;
hence incl X0 = f0 by Th53; :: thesis: verum