let n be Nat; :: thesis: for T being non empty TopSpace
for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: f,g
let T be non empty TopSpace; :: thesis: for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: f,g
set c = the carrier of T;
set R = TOP-REAL n;
set F = TIMES n;
let f, g be Function of T,(TOP-REAL n); :: thesis: f <##> g = (TIMES n) .: f,g
A1: dom (f <##> g) = (dom f) /\ (dom g) by VALUED_2:def 47;
dom (TIMES n) = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by FUNCT_2:def 1
.= [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] by BORSUK_1:def 5 ;
then [:(rng f),(rng g):] c= dom (TIMES n) by ZFMISC_1:119;
then A2: dom ((TIMES n) .: f,g) = (dom f) /\ (dom g) by FUNCOP_1:84;

now

let x be set ; :: thesis: ( x in dom (f <##> g) implies (f <##> g) . x = ((TIMES n) .: f,g) . x )
assume A3: x in dom (f <##> g) ; :: thesis: (f <##> g) . x = ((TIMES n) .: f,g) . x
then A4: ( f . x is Point of (TOP-REAL n) & g . x is Point of (TOP-REAL n) ) by FUNCT_2:7;
thus (f <##> g) . x = (f . x) (#) (g . x) by A3, VALUED_2:def 47
.= (TIMES n) . (f . x),(g . x) by A4, Def5
.= ((TIMES n) .: f,g) . x by A1, A2, A3, FUNCOP_1:28 ; :: thesis: verum

end;

hence f <##> g = (TIMES n) .: f,g by A1, A2, FUNCT_1:9; :: thesis: verum