for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0

proof

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A1: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
then x0 in dom f by RELAT_1:86;
then A2: f is_continuous_in x0 by Def2;
x0 in X by A1, RELAT_1:86;
hence f | X is_continuous_in x0 by A2, Th1; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL,REAL st b₁ = f | X holds
b₁ is continuous by Def2; :: thesis: verum