let X be set ; for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <//> g is Function of X,(TOP-REAL n)
let n be Nat; for f, g being Function of X,(TOP-REAL n) holds f <//> g is Function of X,(TOP-REAL n)
let f, g be Function of X,(TOP-REAL n); f <//> g is Function of X,(TOP-REAL n)
set h = f <//> g;
A1:
dom f = X
by FUNCT_2:def 1;
dom g = X
by FUNCT_2:def 1;
then A2:
dom (f <//> g) = X
by A1, VALUED_2:def 48;
for x being object st x in X holds
(f <//> g) . x in the carrier of (TOP-REAL n)
hence
f <//> g is Function of X,(TOP-REAL n)
by A2, FUNCT_2:3; verum