defpred S₁[ Element of (TOP-REAL 1), object ] means f = T /. 1;
A1: for x being Element of (TOP-REAL 1) ex y being Element of R^1 st S₁[x,y] by TOPMETR:17;
consider P being Function of (TOP-REAL 1),R^1 such that
A2: for x being Element of (TOP-REAL 1) holds S₁[x,P . x] from FUNCT_2:sch 3(A1);
A3: P is being_homeomorphism by A2, JORDAN2B:28;
then reconsider PP = P " as continuous Function of R^1,(TOP-REAL 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,(TOP-REAL 1) ;
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 A3, TOPS_2:def 4;
let x be object ; :: thesis: ( x in dom PPf implies PPf . x = |[f]| . x )
A9: rng P = [#] R^1 by A3, TOPS_2:def 5;
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 A10, FUNCT_1:def 3;
then reconsider PPfx = PPf . x as Point of (TOP-REAL 1) ;
f . x in dom PP by A10, FUNCT_1:11;
then P . (PPf . x) = f . x by A11, A8, A3, A9, FUNCT_1:35;
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 A12, B, FINSEQ_4:16;
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 b₁ being Function of T,(TOP-REAL 1) st b₁ = |[f]| holds
b₁ is continuous by A4, A7, RELAT_1:27, A5, FUNCT_1:2; :: thesis: verum