let X be set ; :: thesis: 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; :: thesis: 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); :: thesis: 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 47;
for x being object st x in X holds
(f <##> g) . x in the carrier of (TOP-REAL n)

proof

let x be object ; :: thesis: ( x in X implies (f <##> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; :: thesis: (f <##> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f, g = g as Function of X,(TOP-REAL n) ;
(f <##> g) . x = (f . x) (#) (g . x) by A2, VALUED_2:def 47;
hence (f <##> g) . x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

hence f <##> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; :: thesis: verum