set Y = the carrier of R^1;
set TR = the carrier of (TOP-REAL n);

A1: now :: thesis: for x being object st x in dom F holds
(doms F) . x = X

let x be object ; :: thesis: ( x in dom F implies (doms F) . x = X )
assume A2: x in dom F ; :: thesis: (doms F) . x = X
then F . x in rng F by FUNCT_1:def 3;
then ex Fx being Function st
( Fx = F . x & dom Fx = X & rng Fx c= the carrier of R^1 ) by FUNCT_2:def 2;
hence (doms F) . x = X by A2, FUNCT_6:22; :: thesis: verum

end;

A3: rng <:F:> c= product (rngs F) by FUNCT_6:29;
len F = n by CARD_1:def 7;
then A4: dom F = Seg n by FINSEQ_1:def 3;
A5: dom (rngs F) = dom F by FUNCT_6:60;
A6: product (rngs F) c= the carrier of (TOP-REAL n)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in product (rngs F) or y in the carrier of (TOP-REAL n) )
assume y in product (rngs F) ; :: thesis: y in the carrier of (TOP-REAL n)
then consider g being Function such that
A7: y = g and
A8: dom g = dom F and
A9: for z being object st z in dom F holds
g . z in (rngs F) . z by CARD_3:def 5, A5;
reconsider g = g as FinSequence by A4, A8, FINSEQ_1:def 2;
rng g c= REAL

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in REAL )
assume z in rng g ; :: thesis: z in REAL
then consider x being object such that
A10: x in dom g and
A11: z = g . x by FUNCT_1:def 3;
A12: (rngs F) . x = rng (F . x) by A8, A10, FUNCT_6:def 3;
g . x in (rngs F) . x by A8, A9, A10;
hence z in REAL by A12, A11; :: thesis: verum

end;

then reconsider g = g as FinSequence of REAL by FINSEQ_1:def 4;
n in NAT by ORDINAL1:def 12;
then len g = n by A8, A4, FINSEQ_1:def 3;
hence y in the carrier of (TOP-REAL n) by A7, TOPREAL7:17; :: thesis: verum

end;

dom (doms F) = dom F by FUNCT_6:59;
then doms F = (dom F) --> X by A1, FUNCOP_1:11;
then dom <:F:> = meet ((dom F) --> X) by FUNCT_6:29;
then dom <:F:> = X by FUNCT_6:27;
hence <:F:> is Function of X,(TOP-REAL n) by A6, A3, XBOOLE_1:1, FUNCT_2:2; :: thesis: verum