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) by FUNCT_3:99;
A2: [:f,g:] is continuous Function of [:T,T:],[:S,R:] by BORSUK_2:12;
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