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:1;
then reconsider x = x0 as Point of X ;
f is_continuous_at x by Th44;
hence f | X0 is_continuous_at x0 by Th58; :: thesis: verum
end;
hence f | X0 is continuous by Th44; :: thesis: verum