let Y, S, T be non empty TopSpace; :: thesis: for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous
let f be continuous Function of Y,[:S,T:]; :: thesis: 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;
:: thesis: 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;
:: thesis: ( (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
;
:: thesis: ex W being Subset of Y st
( p in W & W is open & (pr1 f) .: W c= V )
the
carrier of
[:S,T:] = [:the carrier of S,the carrier of T:]
by BORSUK_1:def 5;
then consider s,
t being
set such that
s in the
carrier of
S
and A3:
t in the
carrier of
T
and A4:
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 =
(f . p) `1
by MCART_1:def 12
.=
s
by A4, MCART_1:def 1
;
then A7:
f . p in [:V,([#] T):]
by A1, A3, A4, ZFMISC_1:106;
[:V,([#] T):] is
open
by A2, BORSUK_1:46;
then consider W being
Subset of
Y such that A8:
p in W
and A9:
W is
open
and A10:
f .: W c= [:V,([#] T):]
by A7, JGRAPH_2:20;
take
W
;
:: thesis: ( p in W & W is open & (pr1 f) .: W c= V )
thus
(
p in W &
W is
open )
by A8, A9;
:: thesis: (pr1 f) .: W c= V
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in (pr1 f) .: W or y in V )
assume
y in (pr1 f) .: W
;
:: thesis: y in V
then consider x being
Point of
Y such that A11:
x in W
and A12:
y = (pr1 f) . x
by FUNCT_2:116;
A13:
(pr1 f) . x = (f . x) `1
by A6, MCART_1:def 12;
f . x in f .: W
by A6, A11, FUNCT_1:def 12;
hence
y in V
by A10, A12, A13, MCART_1:10;
:: thesis: verum
end;
hence
pr1 f is continuous
by JGRAPH_2:20; :: thesis: verum