let T1, T2, S1, S2 be non empty TopSpace; :: thesis: for f being Function of T1,T2
for g being Function of S1,S2 st f is being_homeomorphism & g is being_homeomorphism holds
[:f,g:] is being_homeomorphism
let f be Function of T1,T2; :: thesis: for g being Function of S1,S2 st f is being_homeomorphism & g is being_homeomorphism holds
[:f,g:] is being_homeomorphism
let g be Function of S1,S2; :: thesis: ( f is being_homeomorphism & g is being_homeomorphism implies [:f,g:] is being_homeomorphism )
assume that
A1: f is being_homeomorphism and
A2: g is being_homeomorphism ; :: thesis: [:f,g:] is being_homeomorphism
A3: rng g = [#] S2 by A2, TOPS_2:def 5;
A4: g " is continuous by A2, TOPS_2:def 5;
A5: f " is continuous by A1, TOPS_2:def 5;
A6: the carrier of [:T2,S2:] = [: the carrier of T2, the carrier of S2:] by BORSUK_1:def 2;
set fg = [:f,g:];
A7: rng f = [#] T2 by A1, TOPS_2:def 5;
then A8: rng [:f,g:] = [#] [:T2,S2:] by A3, FUNCT_3:67, A6;
reconsider F = f, G = g, FG = [:f,g:] as Function ;
A9: FG " = [:(F "),(G "):] by A1, A2, FUNCTOR0:6;
A10: F " = f " by A1, TOPS_2:def 4;
A11: rng [:f,g:] = [:(rng f),(rng g):] by FUNCT_3:67;
then [:f,g:] is onto by A6, A7, A3, FUNCT_2:def 3;
then A12: FG " = [:f,g:] " by A1, A2, TOPS_2:def 4;

A13: now :: thesis: for P being Subset of [:T2,S2:] holds
( ( P is open implies [:f,g:] " P is open ) & ( [:f,g:] " P is open implies P is open ) )

let P be Subset of [:T2,S2:]; :: thesis: ( ( P is open implies [:f,g:] " P is open ) & ( [:f,g:] " P is open implies P is open ) )
thus ( P is open implies [:f,g:] " P is open ) by BORSUK_2:10, A1, A2; :: thesis: ( [:f,g:] " P is open implies P is open )
thus ( [:f,g:] " P is open implies P is open ) :: thesis: verum

proof

assume A14: [:f,g:] " P is open ; :: thesis: P is open
[:(f "),(g "):] " ([:f,g:] " P) = ([:f,g:] ") " ([:f,g:] " P) by A10, A2, TOPS_2:def 4, A9, A12
.= [:f,g:] .: ([:f,g:] " P) by TOPS_2:54, A1, A2, A8
.= P by FUNCT_1:77, A7, A3, A11, A6 ;
hence P is open by BORSUK_2:10, A5, A4, A14; :: thesis: verum

end;

end;

A15: dom g = [#] S1 by A2, TOPS_2:def 5;
A16: the carrier of [:T1,S1:] = [: the carrier of T1, the carrier of S1:] by BORSUK_1:def 2;
dom f = [#] T1 by A1, TOPS_2:def 5;
then dom [:f,g:] = [#] [:T1,S1:] by A15, FUNCT_3:def 8, A16;
hence [:f,g:] is being_homeomorphism by A13, TOPGRP_1:26, A1, A2, A8; :: thesis: verum