defpred S₁[ set , set ] means $2 = n |-> (f . $1);
A1: for x being Element of T ex y being Element of (TOP-REAL n) st S₁[x,y]

proof

let x be Element of T; :: thesis: ex y being Element of (TOP-REAL n) st S₁[x,y]
f . x in REAL by XREAL_0:def 1;
then n |-> (f . x) is Element of REAL n by FINSEQ_2:112;
then reconsider y = n |-> (f . x) as Point of (TOP-REAL n) by EUCLID:22;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

ex F being Function of T,(TOP-REAL n) st
for x being Element of T holds S₁[x,F . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of T,(TOP-REAL n) st
for t being Element of T holds b₁ . t = n |-> (f . t) ; :: thesis: verum