let S, T be non empty TopSpace; :: thesis: pr1 the carrier of S,the carrier of T is continuous Function of [:S,T:],S
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 5;
then reconsider f = pr1 the carrier of S,the carrier of T as Function of [:S,T:],S ;
f is continuous

proof

let w be Point of [:S,T:]; :: according to BORSUK_1:def 3 :: 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
consider x, y being set such that
A2: ( x in the carrier of S & y in the carrier of T & w = [x,y] ) by A1, ZFMISC_1:def 2;
set H = [:(Int G),([#] T):];
A3: Int [:(Int G),([#] T):] = [:(Int (Int G)),(Int ([#] T)):] by BORSUK_1:47
.= [:(Int G),([#] T):] by TOPS_1:43 ;
A4: f . w in Int G by CONNSP_2:def 1;
[:(Int G),([#] T):] is a_neighborhood of w

proof

f . x,y = x by A2, FUNCT_3:def 5;
hence w in Int [:(Int G),([#] T):] by A2, A3, A4, ZFMISC_1:def 2; :: according to CONNSP_2:def 1 :: thesis: verum

end;

then reconsider H = [:(Int G),([#] T):] as a_neighborhood of w ;
take H ; :: thesis: f .: H c= G
reconsider X = Int G as non empty Subset of S by CONNSP_2:def 1;
[:X,([#] T):] <> {} ;
then f .: H = Int G by BORSUK_1:12;
hence f .: H c= G by TOPS_1:44; :: thesis: verum

end;

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