defpred S_{1}[ 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_{1}[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_{1}[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;

hence for b_{1} being Function of T,(TOP-REAL 1) st b_{1} = |[f]| holds

b_{1} is continuous
by A4, A7, RELAT_1:27, A5, FUNCT_1:2; :: thesis: verum

A1: for x being Element of (TOP-REAL 1) ex y being Element of R^1 st S

consider P being Function of (TOP-REAL 1),R^1 such that

A2: for x being Element of (TOP-REAL 1) holds S

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

rng f c= the carrier of R^1
by RELAT_1:def 19;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;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

hence for b

b