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
A2: now :: thesis: for x0 being object st x0 in dom f holds
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;
(dom f1) /\ (dom f1) = dom f ;
then f = f1 (#) f1 by A2, VALUED_1:def 4;
hence f | (dom f) is continuous ; :: thesis: verum