let X be set ; :: thesis: for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in X holds

f . x0 = |.x0.| ) holds

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( ( for x0 being Real st x0 in X holds

f . x0 = |.x0.| ) implies f | X is continuous )

assume A1: for x0 being Real st x0 in X holds

f . x0 = |.x0.| ; :: thesis: f | X is continuous

f . x0 = |.x0.| ) holds

f | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( ( for x0 being Real st x0 in X holds

f . x0 = |.x0.| ) implies f | X is continuous )

assume A1: for x0 being Real st x0 in X holds

f . x0 = |.x0.| ; :: thesis: f | X is continuous

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

(f | X) . x0 = |.x0.|

hence
f | X is continuous
by Th44; :: thesis: verum(f | X) . x0 = |.x0.|

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies (f | X) . x0 = |.x0.| )

assume A2: x0 in dom (f | X) ; :: thesis: (f | X) . x0 = |.x0.|

then f . x0 = |.x0.| by A1;

hence (f | X) . x0 = |.x0.| by A2, FUNCT_1:47; :: thesis: verum

end;assume A2: x0 in dom (f | X) ; :: thesis: (f | X) . x0 = |.x0.|

then f . x0 = |.x0.| by A1;

hence (f | X) . x0 = |.x0.| by A2, FUNCT_1:47; :: thesis: verum