let n be Nat; :: thesis: for T being non empty TopSpace
for f, g being Function of T,() holds f <##> g = () .: (f,g)

let T be non empty TopSpace; :: thesis: for f, g being Function of T,() holds f <##> g = () .: (f,g)
set R = TOP-REAL n;
set F = TIMES n;
let f, g be Function of T,(); :: thesis: f <##> g = () .: (f,g)
A1: dom (f <##> g) = (dom f) /\ (dom g) by VALUED_2:def 47;
dom () = the carrier of [:(),():] by FUNCT_2:def 1
.= [: the carrier of (), the carrier of ():] by BORSUK_1:def 2 ;
then [:(rng f),(rng g):] c= dom () by ZFMISC_1:96;
then A2: dom (() .: (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 = (() .: (f,g)) . x
let x be object ; :: thesis: ( x in dom (f <##> g) implies (f <##> g) . x = (() .: (f,g)) . x )
assume A3: x in dom (f <##> g) ; :: thesis: (f <##> g) . x = (() .: (f,g)) . x
then A4: ( f . x is Point of () & g . x is Point of () ) by FUNCT_2:5;
thus (f <##> g) . x = (f . x) (#) (g . x) by
.= () . ((f . x),(g . x)) by
.= (() .: (f,g)) . x by ; :: thesis: verum
end;
hence f <##> g = () .: (f,g) by A1, A2; :: thesis: verum