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

f . x0 = x0 ^2 ) holds

f | X is continuous

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

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

assume that

A1: X c= dom f and

A2: for x0 being Real st x0 in X holds

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

X = (dom f) /\ X by A1, XBOOLE_1:28;

then A3: X = dom (f | X) by RELAT_1:61;

hence f | X is continuous ; :: thesis: verum

f . x0 = x0 ^2 ) holds

f | X is continuous

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

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

assume that

A1: X c= dom f and

A2: for x0 being Real st x0 in X holds

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

X = (dom f) /\ X by A1, XBOOLE_1:28;

then A3: X = dom (f | X) by RELAT_1:61;

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

(f | X) . x0 = x0 ^2

then
(f | X) | X is continuous
by A3, Th42;(f | X) . x0 = x0 ^2

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

assume A4: x0 in dom (f | X) ; :: thesis: (f | X) . x0 = x0 ^2

then f . x0 = x0 ^2 by A2;

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

end;assume A4: x0 in dom (f | X) ; :: thesis: (f | X) . x0 = x0 ^2

then f . x0 = x0 ^2 by A2;

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

hence f | X is continuous ; :: thesis: verum