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 P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let f be continuous Function of S1,T1; :: thesis: for g being continuous Function of S2,T2

for P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let g be continuous Function of S2,T2; :: thesis: for P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let P2 be Subset of [:T1,T2:]; :: thesis: ( P2 is open implies [:f,g:] " P2 is open )

reconsider Kill = [:f,g:] " (Base-Appr P2) as Subset-Family of [:S1,S2:] ;

for P being Subset of [:S1,S2:] st P in Kill holds

P is open

assume P2 is open ; :: thesis: [:f,g:] " P2 is open

then P2 = union (Base-Appr P2) by BORSUK_1:13;

then [:f,g:] " P2 = union ([:f,g:] " (Base-Appr P2)) by Th7;

hence [:f,g:] " P2 is open by A1, TOPS_2:19; :: thesis: verum

for g being continuous Function of S2,T2

for P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let f be continuous Function of S1,T1; :: thesis: for g being continuous Function of S2,T2

for P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let g be continuous Function of S2,T2; :: thesis: for P2 being Subset of [:T1,T2:] st P2 is open holds

[:f,g:] " P2 is open

let P2 be Subset of [:T1,T2:]; :: thesis: ( P2 is open implies [:f,g:] " P2 is open )

reconsider Kill = [:f,g:] " (Base-Appr P2) as Subset-Family of [:S1,S2:] ;

for P being Subset of [:S1,S2:] st P in Kill holds

P is open

proof

then A1:
Kill is open
by TOPS_2:def 1;
let P be Subset of [:S1,S2:]; :: thesis: ( P in Kill implies P is open )

assume P in Kill ; :: thesis: P is open

then ex B being Subset of [:T1,T2:] st

( B in Base-Appr P2 & P = [:f,g:] " B ) by FUNCT_2:def 9;

hence P is open by Th8; :: thesis: verum

end;assume P in Kill ; :: thesis: P is open

then ex B being Subset of [:T1,T2:] st

( B in Base-Appr P2 & P = [:f,g:] " B ) by FUNCT_2:def 9;

hence P is open by Th8; :: thesis: verum

assume P2 is open ; :: thesis: [:f,g:] " P2 is open

then P2 = union (Base-Appr P2) by BORSUK_1:13;

then [:f,g:] " P2 = union ([:f,g:] " (Base-Appr P2)) by Th7;

hence [:f,g:] " P2 is open by A1, TOPS_2:19; :: thesis: verum