let X, Y be non empty TopSpace; :: thesis: for f being continuous Function of X,Y
for X0 being non empty SubSpace of X holds f | X0 is continuous Function of X0,Y
let f be continuous Function of X,Y; :: thesis: for X0 being non empty SubSpace of X holds f | X0 is continuous Function of X0,Y
let X0 be non empty SubSpace of X; :: thesis: f | X0 is continuous Function of X0,Y
for x0 being Point of X0 holds f | X0 is_continuous_at x0

proof

let x0 be Point of X0; :: thesis: f | X0 is_continuous_at x0
( the carrier of X0 c= the carrier of X & x0 in the carrier of X0 ) by BORSUK_1:35;
then reconsider x = x0 as Point of X ;
f is_continuous_at x by Th49;
hence f | X0 is_continuous_at x0 by Th64; :: thesis: verum

end;

hence f | X0 is continuous Function of X0,Y by Th49; :: thesis: verum