defpred S1[ Element of (), object ] means f = T /. 1;
A1: for x being Element of () ex y being Element of R^1 st S1[x,y] by TOPMETR:17;
consider P being Function of (),R^1 such that
A2: for x being Element of () holds S1[x,P . x] from A3: P is being_homeomorphism by ;
then reconsider PP = P " as continuous Function of R^1,() by TOPS_2:def 5;
A4: dom PP = the carrier of R^1 by FUNCT_2:def 1;
A5: dom |[f]| = dom f by Def1;
reconsider PPf = PP * f as Function of T,() ;
A6: dom f = the carrier of T by FUNCT_2:def 1;
A7: now :: thesis: for x being object st x in dom PPf holds
PPf . x = |[f]| . x
A8: PP = P " by ;
let x be object ; :: thesis: ( x in dom PPf implies PPf . x = |[f]| . x )
A9: rng P = [#] R^1 by ;
assume A10: x in dom PPf ; :: thesis: PPf . x = |[f]| . x
then A11: PPf . x = PP . (f . x) by FUNCT_1:12;
PPf . x in rng PPf by ;
then reconsider PPfx = PPf . x as Point of () ;
f . x in dom PP by ;
then P . (PPf . x) = f . x by ;
then A12: PPfx /. 1 = f . x by A2;
consider R being Real such that
B: <*R*> = PPfx by JORDAN2B:20;
R is Element of REAL by XREAL_0:def 1;
then R = f . x by ;
hence PPf . x = |[f]| . x by B, A10, A6, A5, Def1; :: thesis: verum
end;
rng f c= the carrier of R^1 by RELAT_1:def 19;
hence for b1 being Function of T,() st b1 = |[f]| holds
b1 is continuous by ; :: thesis: verum