let S, T, Y be non empty TopSpace; for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous
let f be continuous Function of Y,[:S,T:]; pr1 f is continuous
set g = pr1 f;
for p being Point of Y
for V being Subset of S st (pr1 f) . p in V & V is open holds
ex W being Subset of Y st
( p in W & W is open & (pr1 f) .: W c= V )
proof
let p be
Point of
Y;
for V being Subset of S st (pr1 f) . p in V & V is open holds
ex W being Subset of Y st
( p in W & W is open & (pr1 f) .: W c= V )let V be
Subset of
S;
( (pr1 f) . p in V & V is open implies ex W being Subset of Y st
( p in W & W is open & (pr1 f) .: W c= V ) )
assume that A1:
(pr1 f) . p in V
and A2:
V is
open
;
ex W being Subset of Y st
( p in W & W is open & (pr1 f) .: W c= V )
A3:
[:V,([#] T):] 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
s in the
carrier of
S
and A4:
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 (pr1 f) . p =
[s,t] `1
by A5, MCART_1:def 12
.=
s
;
then
f . p in [:V,([#] T):]
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= [:V,([#] T):]
by A3, JGRAPH_2:10;
take
W
;
( p in W & W is open & (pr1 f) .: W c= V )
thus
(
p in W &
W is
open )
by A7;
(pr1 f) .: W c= V
let y be
object ;
TARSKI:def 3 ( not y in (pr1 f) .: W or y in V )
assume
y in (pr1 f) .: W
;
y in V
then consider x being
Point of
Y such that A9:
x in W
and A10:
y = (pr1 f) . x
by FUNCT_2:65;
A11:
(pr1 f) . x = (f . x) `1
by A6, MCART_1:def 12;
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
pr1 f is continuous
by JGRAPH_2:10; verum