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

f . x0 = x0 ^2 ) implies f | (dom f) is continuous )

reconsider f1 = id (dom f) as PartFunc of REAL,REAL ;

assume A1: for x0 being Real st x0 in dom f holds

f . x0 = x0 ^2 ; :: thesis: f | (dom f) is continuous

then f = f1 (#) f1 by A2, VALUED_1:def 4;

hence f | (dom f) is continuous ; :: thesis: verum

f . x0 = x0 ^2 ) implies f | (dom f) is continuous )

reconsider f1 = id (dom f) as PartFunc of REAL,REAL ;

assume A1: for x0 being Real st x0 in dom f holds

f . x0 = x0 ^2 ; :: thesis: f | (dom f) is continuous

A2: now :: thesis: for x0 being object st x0 in dom f holds

f . x0 = (f1 . x0) * (f1 . x0)

(dom f1) /\ (dom f1) = dom f
;f . x0 = (f1 . x0) * (f1 . x0)

let x0 be object ; :: thesis: ( x0 in dom f implies f . x0 = (f1 . x0) * (f1 . x0) )

assume A3: x0 in dom f ; :: thesis: f . x0 = (f1 . x0) * (f1 . x0)

then reconsider x1 = x0 as Real ;

thus f . x0 = x1 ^2 by A1, A3

.= (f1 . x1) * x1 by A3, FUNCT_1:18

.= (f1 . x0) * (f1 . x0) by A3, FUNCT_1:18 ; :: thesis: verum

end;assume A3: x0 in dom f ; :: thesis: f . x0 = (f1 . x0) * (f1 . x0)

then reconsider x1 = x0 as Real ;

thus f . x0 = x1 ^2 by A1, A3

.= (f1 . x1) * x1 by A3, FUNCT_1:18

.= (f1 . x0) * (f1 . x0) by A3, FUNCT_1:18 ; :: thesis: verum

then f = f1 (#) f1 by A2, VALUED_1:def 4;

hence f | (dom f) is continuous ; :: thesis: verum