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

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 ; :: 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;

hence [:f,g:] is open by Th45; :: thesis: verum