let S, T be non empty TopSpace; 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:];
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
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
;
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;
verum
end;
hence
pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T
; verum