defpred S_{1}[ set , set ] means $2 = n |-> (f . $1);

A1: for x being Element of T ex y being Element of (TOP-REAL n) st S_{1}[x,y]

for x being Element of T holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A1);

hence ex b_{1} being Function of T,(TOP-REAL n) st

for t being Element of T holds b_{1} . t = n |-> (f . t)
; :: thesis: verum

A1: for x being Element of T ex y being Element of (TOP-REAL n) st S

proof

ex F being Function of T,(TOP-REAL n) st
let x be Element of T; :: thesis: ex y being Element of (TOP-REAL n) st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;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

thus S

for x being Element of T holds S

hence ex b

for t being Element of T holds b