set fg = f ^^ g;
A1: dom g = X by FUNCT_2:def 1;
A2: dom f = X by FUNCT_2:def 1;
then A3: dom (f ^^ g) = X /\ X by A1, PRE_POLY:def 4;
rng (f ^^ g) c= the carrier of (TOP-REAL (n + m))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f ^^ g) or y in the carrier of (TOP-REAL (n + m)) )
assume y in rng (f ^^ g) ; :: thesis: y in the carrier of (TOP-REAL (n + m))
then consider x being object such that
A4: x in dom (f ^^ g) and
A5: (f ^^ g) . x = y by FUNCT_1:def 3;
g . x in rng g by A1, A4, A3, FUNCT_1:def 3;
then reconsider gx = g . x as Point of (TOP-REAL m) ;
f . x in rng f by A2, A4, A3, FUNCT_1:def 3;
then reconsider fx = f . x as Point of (TOP-REAL n) ;
rng (fx ^ gx) c= REAL ;
then A7: fx ^ gx is FinSequence of REAL by FINSEQ_1:def 4;
Z: len (fx ^ gx) = n + m by CARD_1:def 7;
(f ^^ g) . x = fx ^ gx by PRE_POLY:def 4, A4;
hence y in the carrier of (TOP-REAL (n + m)) by A5, Z, A7, TOPREAL7:17; :: thesis: verum

end;

hence f ^^ g is Function of X,(TOP-REAL (n + m)) by A3, FUNCT_2:2; :: thesis: verum