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

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