reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
g | X is continuous PartFunc of REAL,(REAL-NS n) ;
hence for b₁ being PartFunc of REAL,(REAL n) st b₁ = f | X holds
b₁ is continuous by Th23; :: thesis: verum