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