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 A1: for x being Point of X st x in the carrier of X0 holds
x = f0 . x ; :: thesis: incl X0 = f0

now

let x be Point of X; :: thesis: ( x in the carrier of X0 implies (id X) . x = f0 . x )
assume A2: x in the carrier of X0 ; :: thesis: (id X) . x = f0 . x
(id X) . x = x by FUNCT_1:35;
hence (id X) . x = f0 . x by A1, A2; :: thesis: verum

end;

hence incl X0 = f0 by Th59; :: thesis: verum