let S, T be non empty TopSpace; :: thesis: pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T
set I = the carrier of S;
set J = the carrier of T;
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2;
then reconsider f = pr2 ( the carrier of S, the carrier of T) as Function of [:S,T:],T ;
f is continuous

proof

let w be Point of [:S,T:]; :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of f . w ex b₂ being a_neighborhood of w st f .: b₂ c= b₁
let G be a_neighborhood of f . w; :: thesis: ex b₁ being a_neighborhood of w st f .: b₁ c= G
set H = [:([#] S),(Int G):];
A2: Int [:([#] S),(Int G):] = [:(Int ([#] S)),(Int (Int G)):] by BORSUK_1:7
.= [:([#] S),(Int G):] by TOPS_1:15 ;
consider x, y being object such that
A3: x in the carrier of S and
A4: y in the carrier of T and
A5: w = [x,y] by A1, ZFMISC_1:def 2;
( f . w in Int G & f . (x,y) = y ) by A3, A4, CONNSP_2:def 1, FUNCT_3:def 5;
then w in Int [:([#] S),(Int G):] by A3, A5, A2, ZFMISC_1:def 2;
then reconsider H = [:([#] S),(Int G):] as a_neighborhood of w by CONNSP_2:def 1;
take H ; :: thesis: f .: H c= G
reconsider X = Int G as non empty Subset of T by CONNSP_2:def 1;
[:([#] S),X:] <> {} ;
then f .: H = Int G by EQREL_1:49;
hence f .: H c= G by TOPS_1:16; :: thesis: verum

end;

hence pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T ; :: thesis: verum