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 reconsider h = <:f,g:> as Function of T,[:S,R:] ;
A1: ( h = [:f,g:] * (delta the carrier of T) & [:f,g:] is continuous Function of [:T,T:],[:S,R:] ) by BORSUK_2:12, 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; :: thesis: verum