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))

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

hence
f ^^ g is Function of X,(TOP-REAL (n + m))
by A3, FUNCT_2:2; :: thesis: verum
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;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