for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous
; :: thesis: verum

f | X is_continuous_in x0

proof

hence
for b
let x0 be Real; :: 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:57;

then A2: f is_continuous_in x0 by Def2;

x0 in X by A1;

hence f | X is_continuous_in x0 by A2, Th1; :: thesis: verum

end;assume A1: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

then x0 in dom f by RELAT_1:57;

then A2: f is_continuous_in x0 by Def2;

x0 in X by A1;

hence f | X is_continuous_in x0 by A2, Th1; :: thesis: verum

b