let S, T, Y be non empty TopSpace; for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous
let f be continuous Function of Y,[:S,T:]; pr2 f is continuous
set g = pr2 f;
for p being Point of Y
for V being Subset of T st (pr2 f) . p in V & V is open holds
ex W being Subset of Y st
( p in W & W is open & (pr2 f) .: W c= V )
proof
let p be
Point of
Y;
for V being Subset of T st (pr2 f) . p in V & V is open holds
ex W being Subset of Y st
( p in W & W is open & (pr2 f) .: W c= V )let V be
Subset of
T;
( (pr2 f) . p in V & V is open implies ex W being Subset of Y st
( p in W & W is open & (pr2 f) .: W c= V ) )
assume that A1:
(pr2 f) . p in V
and A2:
V is
open
;
ex W being Subset of Y st
( p in W & W is open & (pr2 f) .: W c= V )
A3:
[:([#] S),V:] is
open
by A2, BORSUK_1:6;
the
carrier of
[:S,T:] = [: the carrier of S, the carrier of T:]
by BORSUK_1:def 2;
then consider s,
t being
object such that A4:
s in the
carrier of
S
and
t in the
carrier of
T
and A5:
f . p = [s,t]
by ZFMISC_1:def 2;
A6:
dom f = the
carrier of
Y
by FUNCT_2:def 1;
then (pr2 f) . p =
[s,t] `2
by A5, MCART_1:def 13
.=
t
;
then
f . p in [:([#] S),V:]
by A1, A4, A5, ZFMISC_1:87;
then consider W being
Subset of
Y such that A7:
(
p in W &
W is
open )
and A8:
f .: W c= [:([#] S),V:]
by A3, JGRAPH_2:10;
take
W
;
( p in W & W is open & (pr2 f) .: W c= V )
thus
(
p in W &
W is
open )
by A7;
(pr2 f) .: W c= V
let y be
object ;
TARSKI:def 3 ( not y in (pr2 f) .: W or y in V )
assume
y in (pr2 f) .: W
;
y in V
then consider x being
Point of
Y such that A9:
x in W
and A10:
y = (pr2 f) . x
by FUNCT_2:65;
A11:
(pr2 f) . x = (f . x) `2
by A6, MCART_1:def 13;
f . x in f .: W
by A6, A9, FUNCT_1:def 6;
hence
y in V
by A8, A10, A11, MCART_1:10;
verum
end;
hence
pr2 f is continuous
by JGRAPH_2:10; verum