let T1, T2, S1, S2 be non empty TopSpace; for f being Function of T1,S1
for g being Function of T2,S2 st f is open & g is open holds
[:f,g:] is open
let f be Function of T1,S1; for g being Function of T2,S2 st f is open & g is open holds
[:f,g:] is open
let g be Function of T2,S2; ( f is open & g is open implies [:f,g:] is open )
assume A1:
( f is open & g is open )
; [:f,g:] is open
ex B being Basis of [:T1,T2:] st
for P being Subset of [:T1,T2:] st P in B holds
[:f,g:] .: P is open
proof
set B1 = the
Basis of
T1;
set B2 = the
Basis of
T2;
set B =
{ [:V,W:] where V is Subset of T1, W is Subset of T2 : ( V in the Basis of T1 & W in the Basis of T2 ) } ;
reconsider B =
{ [:V,W:] where V is Subset of T1, W is Subset of T2 : ( V in the Basis of T1 & W in the Basis of T2 ) } as
Basis of
[:T1,T2:] by YELLOW_9:40;
take
B
;
for P being Subset of [:T1,T2:] st P in B holds
[:f,g:] .: P is open
let P be
Subset of
[:T1,T2:];
( P in B implies [:f,g:] .: P is open )
assume
P in B
;
[:f,g:] .: P is open
then consider V being
Subset of
T1,
W being
Subset of
T2 such that A2:
(
P = [:V,W:] &
V in the
Basis of
T1 &
W in the
Basis of
T2 )
;
A3:
(
f .: V is
open &
g .: W is
open )
by A1, T_0TOPSP:def 2, A2, TOPS_2:def 1;
[:f,g:] .: P = [:(f .: V),(g .: W):]
by A2, FUNCT_3:72;
hence
[:f,g:] .: P is
open
by A3, BORSUK_1:6;
verum
end;
hence
[:f,g:] is open
by Th45; verum