let T be non empty TopSpace; :: thesis: delta the carrier of T is continuous Function of T,[:T,T:]
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then reconsider f = delta the carrier of T as Function of T,[:T,T:] ;
f is continuous

proof

let W be Point of 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
consider A being Subset-Family of [:T,T:] such that
A1: Int G = union A and
A2: for e being set st e in A holds
ex X1, Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
f . W in Int G by CONNSP_2:def 1;
then consider Z being set such that
A3: f . W in Z and
A4: Z in A by A1, TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A5: Z = [:X1,Y1:] and
A6: ( X1 is open & Y1 is open ) by A2, A4;
f . W = [W,W] by FUNCT_3:def 6;
then ( W in X1 & W in Y1 ) by A3, A5, ZFMISC_1:87;
then A7: W in X1 /\ Y1 by XBOOLE_0:def 4;
X1 /\ Y1 is open by A6;
then W in Int (X1 /\ Y1) by A7, TOPS_1:23;
then reconsider H = X1 /\ Y1 as a_neighborhood of W by CONNSP_2:def 1;
A8: f .: H c= Int G

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: H or y in Int G )
assume y in f .: H ; :: thesis: y in Int G
then consider x being object such that
A9: x in dom f and
A10: x in H and
A11: y = f . x by FUNCT_1:def 6;
A12: ( x in X1 & x in Y1 ) by A10, XBOOLE_0:def 4;
y = [x,x] by A9, A11, FUNCT_3:def 6;
then y in Z by A5, A12, ZFMISC_1:87;
hence y in Int G by A1, A4, TARSKI:def 4; :: thesis: verum

end;

take H ; :: thesis: f .: H c= G
Int G c= G by TOPS_1:16;
hence f .: H c= G by A8; :: thesis: verum

end;

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