for x0 being Point of X0 holds f | X0 is_continuous_at x0

proof

hence
f | X0 is continuous
by Th44; :: thesis: verum
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;( 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