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 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 2 ;
then [:(rng f),(rng g):] c= dom (TIMES n) by ZFMISC_1:96;
then A2: dom ((TIMES n) .: (f,g)) = (dom f) /\ (dom g) by FUNCOP_1:69;
now :: thesis: for x being object st x in dom (f <##> g) holds
(f <##> g) . x = ((TIMES n) .: (f,g)) . x
let x be object ; :: 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:5;
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:22 ; :: thesis: verum
end;
hence f <##> g = (TIMES n) .: (f,g) by A1, A2; :: thesis: verum