let T1, T2 be TopSpace; ( not T1 is empty & not T2 is empty implies ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] ) )
defpred S1[ object ] means verum;
set PR2 = pr2 ( the carrier of T1, the carrier of T2);
set PR1 = pr1 ( the carrier of T1, the carrier of T2);
assume
( not T1 is empty & not T2 is empty )
; ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )
then reconsider t1 = T1, t2 = T2 as non empty TopSpace ;
reconsider T12 = [:t1,t2:] as non empty TopSpace ;
consider B12 being Basis of T12 such that
A1:
card B12 = weight T12
by WAYBEL23:74;
deffunc H1( Subset of T12) -> Element of bool the carrier of T1 = (pr1 ( the carrier of T1, the carrier of T2)) .: $1;
defpred S2[ object ] means ( $1 in B12 & S1[$1] );
consider B1 being Subset-Family of T1 such that
A2:
B1 = { H1(w) where w is Subset of T12 : S2[w] }
from LMOD_7:sch 5();
A3:
B12 c= the topology of T12
by TOPS_2:64;
A4:
B1 c= the topology of T1
for A being Subset of T1 st A is open holds
for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A )
proof
let A be
Subset of
T1;
( A is open implies for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A ) )
assume
A is
open
;
for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A )
then A7:
[:A,([#] T2):] is
open
by BORSUK_1:6;
set p2 = the
Point of
T2;
A8:
the
Point of
T2 in [#] t2
;
let p1 be
Point of
T1;
( p1 in A implies ex a being Subset of T1 st
( a in B1 & p1 in a & a c= A ) )
assume
p1 in A
;
ex a being Subset of T1 st
( a in B1 & p1 in a & a c= A )
then A9:
[p1, the Point of T2] in [:A,([#] T2):]
by A8, ZFMISC_1:87;
then reconsider p =
[p1, the Point of T2] as
Point of
T12 ;
consider a12 being
Subset of
T12 such that A10:
a12 in B12
and A11:
p in a12
and A12:
a12 c= [:A,([#] T2):]
by A7, A9, YELLOW_9:31;
(
p1 in [#] t1 & the
Point of
T2 in [#] t2 )
;
then A13:
(pr1 ( the carrier of T1, the carrier of T2)) . (
p1, the
Point of
T2)
= p1
by FUNCT_3:def 4;
a12 is
open
by A3, A10;
then reconsider a =
H1(
a12) as
open Subset of
T1 by BORSUK_1:18;
take
a
;
( a in B1 & p1 in a & a c= A )
dom (pr1 ( the carrier of T1, the carrier of T2)) =
[:([#] T1),([#] T2):]
by FUNCT_3:def 4
.=
[#] T12
by BORSUK_1:def 2
;
hence
(
a in B1 &
p1 in a )
by A2, A10, A11, A13, FUNCT_1:def 6;
a c= A
let y be
object ;
TARSKI:def 3 ( not y in a or y in A )
assume
y in a
;
y in A
then consider x being
object such that A14:
x in dom (pr1 ( the carrier of T1, the carrier of T2))
and A15:
(
x in a12 &
y = (pr1 ( the carrier of T1, the carrier of T2)) . x )
by FUNCT_1:def 6;
consider x1,
x2 being
object such that A16:
(
x1 in [#] T1 &
x2 in [#] T2 )
and A17:
x = [x1,x2]
by A14, ZFMISC_1:def 2;
(pr1 ( the carrier of T1, the carrier of T2)) . (
x1,
x2)
= x1
by A16, FUNCT_3:def 4;
hence
y in A
by A12, A15, A17, ZFMISC_1:87;
verum
end;
then reconsider B1 = B1 as Basis of T1 by A4, YELLOW_9:32;
A18:
card { H1(w) where w is Subset of T12 : S2[w] } c= card B12
from BORSUK_2:sch 1();
weight t1 c= card B1
by WAYBEL23:73;
hence
weight T1 c= weight [:T1,T2:]
by A1, A2, A18; weight T2 c= weight [:T1,T2:]
deffunc H2( Subset of T12) -> Element of bool the carrier of T2 = (pr2 ( the carrier of T1, the carrier of T2)) .: $1;
consider B2 being Subset-Family of T2 such that
A19:
B2 = { H2(w) where w is Subset of T12 : S2[w] }
from LMOD_7:sch 5();
A20:
for A being Subset of T2 st A is open holds
for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
proof
let A be
Subset of
T2;
( A is open implies for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A ) )
assume
A is
open
;
for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
then A21:
[:([#] T1),A:] is
open
by BORSUK_1:6;
set p1 = the
Point of
T1;
A22:
the
Point of
T1 in [#] t1
;
let p2 be
Point of
T2;
( p2 in A implies ex a being Subset of T2 st
( a in B2 & p2 in a & a c= A ) )
assume
p2 in A
;
ex a being Subset of T2 st
( a in B2 & p2 in a & a c= A )
then A23:
[ the Point of T1,p2] in [:([#] T1),A:]
by A22, ZFMISC_1:87;
then reconsider p =
[ the Point of T1,p2] as
Point of
T12 ;
consider a12 being
Subset of
T12 such that A24:
a12 in B12
and A25:
p in a12
and A26:
a12 c= [:([#] T1),A:]
by A21, A23, YELLOW_9:31;
( the
Point of
T1 in [#] t1 &
p2 in [#] t2 )
;
then A27:
(pr2 ( the carrier of T1, the carrier of T2)) . ( the
Point of
T1,
p2)
= p2
by FUNCT_3:def 5;
a12 is
open
by A3, A24;
then reconsider a =
H2(
a12) as
open Subset of
T2 by BORSUK_1:18;
take
a
;
( a in B2 & p2 in a & a c= A )
dom (pr2 ( the carrier of T1, the carrier of T2)) =
[:([#] T1),([#] T2):]
by FUNCT_3:def 5
.=
[#] T12
by BORSUK_1:def 2
;
hence
(
a in B2 &
p2 in a )
by A19, A24, A25, A27, FUNCT_1:def 6;
a c= A
let y be
object ;
TARSKI:def 3 ( not y in a or y in A )
assume
y in a
;
y in A
then consider x being
object such that A28:
x in dom (pr2 ( the carrier of T1, the carrier of T2))
and A29:
(
x in a12 &
y = (pr2 ( the carrier of T1, the carrier of T2)) . x )
by FUNCT_1:def 6;
consider x1,
x2 being
object such that A30:
(
x1 in [#] T1 &
x2 in [#] T2 )
and A31:
x = [x1,x2]
by A28, ZFMISC_1:def 2;
(pr2 ( the carrier of T1, the carrier of T2)) . (
x1,
x2)
= x2
by A30, FUNCT_3:def 5;
hence
y in A
by A26, A29, A31, ZFMISC_1:87;
verum
end;
B2 c= the topology of T2
then reconsider B2 = B2 as Basis of T2 by A20, YELLOW_9:32;
A34:
card { H2(w) where w is Subset of T12 : S2[w] } c= card B12
from BORSUK_2:sch 1();
weight T2 c= card B2
by WAYBEL23:73;
hence
weight T2 c= weight [:T1,T2:]
by A1, A19, A34; verum