let T1, T2, S1, S2 be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( f is open & g is open implies [:f,g:] is open )

assume A1: ( f is open & g is open ) ; :: thesis: [: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

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; :: thesis: 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; :: thesis: ( f is open & g is open implies [:f,g:] is open )

assume A1: ( f is open & g is open ) ; :: thesis: [: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

hence
[:f,g:] is open
by Th45; :: thesis: verum
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 ; :: thesis: for P being Subset of [:T1,T2:] st P in B holds

[:f,g:] .: P is open

let P be Subset of [:T1,T2:]; :: thesis: ( P in B implies [:f,g:] .: P is open )

assume P in B ; :: thesis: [: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; :: thesis: verum

end;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 ; :: thesis: for P being Subset of [:T1,T2:] st P in B holds

[:f,g:] .: P is open

let P be Subset of [:T1,T2:]; :: thesis: ( P in B implies [:f,g:] .: P is open )

assume P in B ; :: thesis: [: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; :: thesis: verum