let S1, S2, T1, T2 be non empty TopSpace; :: thesis: for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open
let f be continuous Function of S1,T1; :: thesis: for g being continuous Function of S2,T2
for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open
let g be continuous Function of S2,T2; :: thesis: for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open
let P1, P2 be Subset of [:T1,T2:]; :: thesis: ( P2 in Base-Appr P1 implies [:f,g:] " P2 is open )
assume P2 in Base-Appr P1 ; :: thesis: [:f,g:] " P2 is open
then consider X11 being Subset of T1, Y11 being Subset of T2 such that
A1: P2 = [:X11,Y11:] and
[:X11,Y11:] c= P1 and
A2: X11 is open and
A3: Y11 is open ;
[#] T1 <> {} ;
then A4: f " X11 is open by A2, TOPS_2:43;
[#] T2 <> {} ;
then A5: g " Y11 is open by A3, TOPS_2:43;
[:f,g:] " P2 = [:(f " X11),(g " Y11):] by A1, FUNCT_3:73;
hence [:f,g:] " P2 is open by A4, A5, BORSUK_1:6; :: thesis: verum