let R, S, T 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:]
A1: <:f,g:> = [:f,g:] * (delta the carrier of T) by FUNCT_3:78;
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