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

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