let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) holds
f | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) implies f | X is continuous )
assume A1: ( X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = abs x0 ) ) ; :: thesis: f | X is continuous
then X = (dom f) /\ X by XBOOLE_1:28;
then A2: X = dom (f | X) by RELAT_1:90;

now

let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies (f | X) . x0 = abs x0 )
assume A3: x0 in dom (f | X) ; :: thesis: (f | X) . x0 = abs x0
then f . x0 = abs x0 by A1, A2;
hence (f | X) . x0 = abs x0 by A3, FUNCT_1:70; :: thesis: verum

end;

then f | X is continuous by Th51;
hence f | X is continuous ; :: thesis: verum