let T be non empty TopSpace; 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;
BORSUK_1:def 1 for b1 being a_neighborhood of f . W ex b2 being a_neighborhood of W st f .: b2 c= b1let G be
a_neighborhood of
f . W;
ex b1 being a_neighborhood of W st f .: b1 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
take
H
;
f .: H c= G
Int G c= G
by TOPS_1:16;
hence
f .: H c= G
by A8;
verum
end;
hence
delta the carrier of T is continuous Function of T,[:T,T:]
; verum