let T, S, R be non empty TopSpace; :: thesis: for f being continuous Function of T,S
for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:]
let f be continuous Function of T,S; :: thesis: for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:]
let g be continuous Function of T,R; :: thesis: <:f,g:> is continuous Function of T,[:S,R:]
the carrier of [:S,R:] = [: the carrier of S, the carrier of R:] by BORSUK_1:def 5;
then A2: <:f,g:> is Function of T,[:S,R:] ;
A1: <:f,g:> = [:f,g:] * (delta the carrier of T) by FUNCT_3:99;
delta the carrier of T is continuous Function of T,[:T,T:] by Th38;
hence <:f,g:> is continuous Function of T,[:S,R:] by A1, A2; :: thesis: verum