let S1, S2, T1, T2 be non empty TopSpace; 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; 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; 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:]; ( P2 in Base-Appr P1 implies [:f,g:] " P2 is open )
assume
P2 in Base-Appr P1
; [: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; verum