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 ;
TARSKI:def 3 ( not y in rng (f ^^ g) or y in the carrier of (TOP-REAL (n + m)) )
assume
y in rng (f ^^ g)
;
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;
verum
end;
hence
f ^^ g is Function of X,(TOP-REAL (n + m))
by A3, FUNCT_2:2; verum