let T1, T2, S1, S2 be non empty TopSpace; 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; 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; ( 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
; [: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 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:];
( ( 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;
( [:f,g:] " P is open implies P is open )thus
(
[:f,g:] " P is
open implies
P is
open )
verumproof
assume A14:
[:f,g:] " P is
open
;
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;
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; verum