:: WAYBEL18 semantic presentation

begin

theorem Th1: :: WAYBEL18:1
for X being set
for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds
UniCl A = UniCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds
UniCl A = UniCl B
let A, B be Subset-Family of X; ::_thesis: ( ( B = A \ {{}} or A = B \/ {{}} ) implies UniCl A = UniCl B )
assume A1: ( B = A \ {{}} or A = B \/ {{}} ) ; ::_thesis: UniCl A = UniCl B
A2: UniCl A c= UniCl B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl A or x in UniCl B )
assume  x in UniCl A ; ::_thesis: x in UniCl B
then consider Y being Subset-Family of X such that
A3: Y c= A and
A4: x = union Y by CANTOR_1:def_1;
A5: Y \ {{}} c= B
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Y \ {{}} or w in B )
assume A6: w in Y \ {{}} ; ::_thesis: w in B
percases ( B = A \ {{}} or A = B \/ {{}} ) by A1;
supposeA7: B = A \ {{}} ; ::_thesis: w in B
 ( w in Y & not w in {{}} ) by A6, XBOOLE_0:def_5;
hence  w in B by A3, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA8: A = B \/ {{}} ; ::_thesis: w in B
 ( w in Y & not w in {{}} ) by A6, XBOOLE_0:def_5;
hence  w in B by A3, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
reconsider Z = Y \ {{}} as Subset-Family of X ;
 Z \/ {{}} = Y \/ {{}} by XBOOLE_1:39;
then  union (Z \/ {{}}) = (union Y) \/ (union {{}}) by ZFMISC_1:78
.= (union Y) \/ {} by ZFMISC_1:25
.= union Y ;
then x = (union Z) \/ (union {{}}) by A4, ZFMISC_1:78
.= (union Z) \/ {} by ZFMISC_1:25
.= union Z ;
hence  x in UniCl B by A5, CANTOR_1:def_1; ::_thesis: verum
end;
 UniCl B c= UniCl A by A1, CANTOR_1:9, XBOOLE_1:7, XBOOLE_1:36;
hence  UniCl A = UniCl B by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th2: :: WAYBEL18:2
for T being TopSpace
for K being Subset-Family of T holds
( K is Basis of T iff K \ {{}} is Basis of T )
proof
let T be TopSpace; ::_thesis: for K being Subset-Family of T holds
( K is Basis of T iff K \ {{}} is Basis of T )
let K be Subset-Family of T; ::_thesis: ( K is Basis of T iff K \ {{}} is Basis of T )
reconsider K9 = K \ {{}} as Subset-Family of T ;
A1: UniCl K9 c= UniCl K by CANTOR_1:9, XBOOLE_1:36;
A2: K \ {{}} c= K by XBOOLE_1:36;
hereby  ::_thesis: ( K \ {{}} is Basis of T implies K is Basis of T )
assume A3: K is Basis of T ; ::_thesis: K \ {{}} is Basis of T
then  the topology of T c= UniCl K by CANTOR_1:def_2;
then A4: the topology of T c= UniCl K9 by Th1;
 K c= the topology of T by A3, TOPS_2:64;
then  K \ {{}} c= the topology of T by A2, XBOOLE_1:1;
hence  K \ {{}} is Basis of T by A4, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;
assume A5: K \ {{}} is Basis of T ; ::_thesis: K is Basis of T
then A6: K9 c= the topology of T by TOPS_2:64;
A7: K c= the topology of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in K or x in the topology of T )
assume A8: x in K ; ::_thesis: x in the topology of T
percases ( x = {} or x <> {} ) ;
suppose x = {} ; ::_thesis: x in the topology of T
hence  x in the topology of T by PRE_TOPC:1; ::_thesis: verum
end;
suppose x <> {} ; ::_thesis: x in the topology of T
then  not x in {{}} by TARSKI:def_1;
then  x in K9 by A8, XBOOLE_0:def_5;
hence  x in the topology of T by A6; ::_thesis: verum
end;
end;
end;
 the topology of T c= UniCl K9 by A5, CANTOR_1:def_2;
then  the topology of T c= UniCl K by A1, XBOOLE_1:1;
hence  K is Basis of T by A7, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;

definition
let F be Relation;
attrF is TopStruct-yielding  means :Def1: :: WAYBEL18:def 1
 for x being set st x in rng F holds
x is TopStruct ;
end;

:: deftheorem Def1 defines TopStruct-yielding WAYBEL18:def_1_:_
 for F being Relation holds
( F is TopStruct-yielding iff for x being set st x in rng F holds
x is TopStruct );

registration
cluster Relation-like Function-like TopStruct-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is TopStruct-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is TopStruct-yielding implies F is 1-sorted-yielding )
assume A1: F is TopStruct-yielding ; ::_thesis: F is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom F or F . x is 1-sorted )
assume  x in dom F ; ::_thesis: F . x is 1-sorted
then  F . x in rng F by FUNCT_1:def_3;
hence  F . x is 1-sorted by A1, Def1; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total TopStruct-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is TopStruct-yielding
proof
set T = the TopSpace;
take  I --> the TopSpace ; ::_thesis: I --> the TopSpace is TopStruct-yielding
let v be set ; :: according to WAYBEL18:def_1 ::_thesis: ( v in rng (I --> the TopSpace) implies v is TopStruct )
assume  v in rng (I --> the TopSpace) ; ::_thesis: v is TopStruct
hence  v is TopStruct by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total non-Empty TopStruct-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is TopStruct-yielding & b1 is non-Empty )
proof
set R = the non empty TopSpace;
take J = I --> the non empty TopSpace; ::_thesis: ( J is TopStruct-yielding & J is non-Empty )
thus  J is TopStruct-yielding ::_thesis: J is non-Empty
proof
let x be set ; :: according to WAYBEL18:def_1 ::_thesis: ( x in rng J implies x is TopStruct )
assume  x in rng J ; ::_thesis: x is TopStruct
hence  x is TopStruct by TARSKI:def_1; ::_thesis: verum
end;
thus  J is non-Empty ::_thesis: verum
proof
let S be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not S in rng J or not S is empty )
assume  S in rng J ; ::_thesis: not S is empty
hence  not S is empty by TARSKI:def_1; ::_thesis: verum
end;
end;
end;

definition
let J be non empty set ;
let A be TopStruct-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine funcA . j ->  TopStruct ;
coherence
 A . j is TopStruct
proof
 dom A = J by PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
hence  A . j is TopStruct by Def1; ::_thesis: verum
end;
end;

definition
let I be set ;
let J be TopStruct-yielding ManySortedSet of I;
func product_prebasis J ->  Subset-Family of (product (Carrier J)) means :Def2: :: WAYBEL18:def 2
 for x being Subset of (product (Carrier J)) holds
( x in it iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) );
existence
 ex b1 being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) )
proof
defpred S1[ Subset of (product (Carrier J))] means  ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & $1 = product ((Carrier J) +* (i,V)) );
thus  ex F being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in F iff S1[x] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of (product (Carrier J)) st ( for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) & ( for x being Subset of (product (Carrier J)) holds
( x in b2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) holds
b1 = b2
proof
let P1, P2 be Subset-Family of (product (Carrier J)); ::_thesis: ( ( for x being Subset of (product (Carrier J)) holds
( x in P1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) & ( for x being Subset of (product (Carrier J)) holds
( x in P2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) implies P1 = P2 )
assume that
A1: for x being Subset of (product (Carrier J)) holds
( x in P1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) and
A2: for x being Subset of (product (Carrier J)) holds
( x in P2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ; ::_thesis: P1 = P2
A3: P2 c= P1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 or x in P1 )
assume A4: x in P2 ; ::_thesis: x in P1
then reconsider x9 = x as Subset of (product (Carrier J)) ;
 ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x9 = product ((Carrier J) +* (i,V)) ) by A2, A4;
hence  x in P1 by A1; ::_thesis: verum
end;
 P1 c= P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 )
assume A5: x in P1 ; ::_thesis: x in P2
then reconsider x9 = x as Subset of (product (Carrier J)) ;
 ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x9 = product ((Carrier J) +* (i,V)) ) by A1, A5;
hence  x in P2 by A2; ::_thesis: verum
end;
hence  P1 = P2 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def_2_:_
 for I being set
for J being TopStruct-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier J)) holds
( b3 = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b3 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );

theorem Th3: :: WAYBEL18:3
for X being set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
 ( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A & FinMeetCl A c= UniCl (FinMeetCl A) ) by CANTOR_1:1, CANTOR_1:8;
hence  the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #))) holds
( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) )
hence  for a being Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) st a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A1; ::_thesis: for b1, b2 being Element of K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
thus  for b1, b2 being Element of K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by A1; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
hence  TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like by CANTOR_1:15; ::_thesis: verum
end;
end;
end;

definition
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
func product J ->  strict TopSpace means :Def3: :: WAYBEL18:def 3
( the carrier of it = product (Carrier J) & product_prebasis J is prebasis of it );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 )
proof
set X = product (Carrier J);
reconsider A = product_prebasis J as Subset-Family of (product (Carrier J)) ;
consider T being strict TopStruct  such that
A1: T = TopStruct(# (product (Carrier J)),(UniCl (FinMeetCl A)) #) ;
reconsider T = T as strict TopSpace by A1, Th3;
take  T ; ::_thesis: ( the carrier of T = product (Carrier J) & product_prebasis J is prebasis of T )
thus  the carrier of T = product (Carrier J) by A1; ::_thesis: product_prebasis J is prebasis of T
now__::_thesis:_not_{}_in_rng_(Carrier_J)
assume  {} in rng (Carrier J) ; ::_thesis: contradiction
then consider i being set  such that
A2: i in dom (Carrier J) and
A3: {} = (Carrier J) . i by FUNCT_1:def_3;
consider R being 1-sorted  such that
A4: R = J . i and
A5: {} = the carrier of R by A2, A3, PRALG_1:def_13;
 dom J = I by PARTFUN1:def_2;
then  R in rng J by A2, A4, FUNCT_1:def_3;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def_7;
 the carrier of R = {} by A5;
hence  contradiction ; ::_thesis: verum
end;
then  not product (Carrier J) is empty by CARD_3:26;
hence  product_prebasis J is prebasis of T by A1, CANTOR_1:18; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 & the carrier of b2 = product (Carrier J) & product_prebasis J is prebasis of b2 holds
b1 = b2
proof
let T1, T2 be strict TopSpace; ::_thesis: ( the carrier of T1 = product (Carrier J) & product_prebasis J is prebasis of T1 & the carrier of T2 = product (Carrier J) & product_prebasis J is prebasis of T2 implies T1 = T2 )
assume that
A6: the carrier of T1 = product (Carrier J) and
A7: product_prebasis J is prebasis of T1 and
A8: the carrier of T2 = product (Carrier J) and
A9: product_prebasis J is prebasis of T2 ; ::_thesis: T1 = T2
now__::_thesis:_not_{}_in_rng_(Carrier_J)
assume  {} in rng (Carrier J) ; ::_thesis: contradiction
then consider i being set  such that
A10: i in dom (Carrier J) and
A11: {} = (Carrier J) . i by FUNCT_1:def_3;
consider R being 1-sorted  such that
A12: R = J . i and
A13: {} = the carrier of R by A10, A11, PRALG_1:def_13;
 dom J = I by PARTFUN1:def_2;
then  R in rng J by A10, A12, FUNCT_1:def_3;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def_7;
 the carrier of R = {} by A13;
hence  contradiction ; ::_thesis: verum
end;
then  product (Carrier J) <> {} by CARD_3:26;
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A6, A8;
 t1 = t2 by A6, A7, A8, A9, CANTOR_1:17;
hence  T1 = T2 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines product WAYBEL18:def_3_:_
 for I being set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for b3 being strict TopSpace holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & product_prebasis J is prebasis of b3 ) );

registration
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
cluster product J ->  non empty strict ;
coherence
 not product J is empty
proof
A1: now__::_thesis:_not_{}_in_rng_(Carrier_J)
assume  {} in rng (Carrier J) ; ::_thesis: contradiction
then consider i being set  such that
A2: i in dom (Carrier J) and
A3: {} = (Carrier J) . i by FUNCT_1:def_3;
consider R being 1-sorted  such that
A4: R = J . i and
A5: {} = the carrier of R by A2, A3, PRALG_1:def_13;
 dom J = I by PARTFUN1:def_2;
then  R in rng J by A2, A4, FUNCT_1:def_3;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def_7;
 the carrier of R = {} by A5;
hence  contradiction ; ::_thesis: verum
end;
 the carrier of (product J) = product (Carrier J) by Def3;
then  the carrier of (product J) <> {} by A1, CARD_3:26;
hence  not product J is empty ; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine funcJ . i ->  non empty TopStruct ;
coherence
 J . i is non empty TopStruct
proof
 dom J = I by PARTFUN1:def_2;
then  J . i in rng J by FUNCT_1:def_3;
hence  J . i is non empty TopStruct by WAYBEL_3:def_7; ::_thesis: verum
end;
end;

registration
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
cluster product J ->  strict constituted-Functions ;
coherence
 product J is constituted-Functions
proof
 the carrier of (product J) = product (Carrier J) by Def3;
hence  product J is constituted-Functions by MONOID_0:80; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine funcx . i ->  Element of (J . i);
coherence
 x . i is Element of (J . i)
proof
A1: dom (Carrier J) = I by PARTFUN1:def_2;
 ( ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) & the carrier of (product J) = product (Carrier J) ) by Def3, PRALG_1:def_13;
hence  x . i is Element of (J . i) by A1, CARD_3:9; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let i be Element of I;
func proj (J,i) ->  Function of (product J),(J . i) equals :: WAYBEL18:def 4
 proj ((Carrier J),i);
coherence
 proj ((Carrier J),i) is Function of (product J),(J . i)
proof
consider f being Function such that
A1: f = proj ((Carrier J),i) ;
A2: dom f = product (Carrier J) by A1, CARD_3:def_16
.= the carrier of (product J) by Def3 ;
 rng f c= the carrier of (J . i)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of (J . i) )
assume  y in rng f ; ::_thesis: y in the carrier of (J . i)
then consider x being set  such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of (product J) by A2, A3;
 f . x = x . i by A1, A3, CARD_3:def_16;
hence  y in the carrier of (J . i) by A4; ::_thesis: verum
end;
hence  proj ((Carrier J),i) is Function of (product J),(J . i) by A1, A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

:: deftheorem  defines proj WAYBEL18:def_4_:_
 for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) = proj ((Carrier J),i);

theorem Th4: :: WAYBEL18:4
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))
let i be Element of I; ::_thesis: for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))
let P be Subset of (J . i); ::_thesis: (proj (J,i)) " P = product ((Carrier J) +* (i,P))
set f = (Carrier J) +* (i,P);
A1: dom (Carrier J) = I by PARTFUN1:def_2;
A2: dom ((Carrier J) +* (i,P)) = dom (Carrier J) by FUNCT_7:30
.= I by PARTFUN1:def_2 ;
A3: product ((Carrier J) +* (i,P)) c= (proj (J,i)) " P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ((Carrier J) +* (i,P)) or x in (proj (J,i)) " P )
assume  x in product ((Carrier J) +* (i,P)) ; ::_thesis: x in (proj (J,i)) " P
then consider g being Function such that
A4: x = g and
A5: dom g = dom ((Carrier J) +* (i,P)) and
A6: for y being set st y in dom ((Carrier J) +* (i,P)) holds
g . y in ((Carrier J) +* (i,P)) . y by CARD_3:def_5;
A7: for j being set st j in dom (Carrier J) holds
g . j in (Carrier J) . j
proof
let j be set ; ::_thesis: ( j in dom (Carrier J) implies g . j in (Carrier J) . j )
assume  j in dom (Carrier J) ; ::_thesis: g . j in (Carrier J) . j
then A8: j in I ;
then A9: ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def_13;
percases ( j = i or j <> i ) ;
supposeA10: j = i ; ::_thesis: g . j in (Carrier J) . j
 ((Carrier J) +* (i,P)) . i = P by A1, FUNCT_7:31;
then  g . j in P by A2, A6, A10;
hence  g . j in (Carrier J) . j by A9, A10; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: g . j in (Carrier J) . j
then  ((Carrier J) +* (i,P)) . j = (Carrier J) . j by FUNCT_7:32;
hence  g . j in (Carrier J) . j by A2, A6, A8; ::_thesis: verum
end;
end;
end;
 dom g = dom (Carrier J) by A5, FUNCT_7:30;
then A11: g in product (Carrier J) by A7, CARD_3:9;
then A12: g in dom (proj ((Carrier J),i)) by CARD_3:def_16;
 ((Carrier J) +* (i,P)) . i = P by A1, FUNCT_7:31;
then  g . i in P by A2, A6;
then A13: (proj ((Carrier J),i)) . g in P by A12, CARD_3:def_16;
 g in dom (proj (J,i)) by A11, CARD_3:def_16;
hence  x in (proj (J,i)) " P by A4, A13, FUNCT_1:def_7; ::_thesis: verum
end;
 (proj (J,i)) " P c= product ((Carrier J) +* (i,P))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj (J,i)) " P or x in product ((Carrier J) +* (i,P)) )
assume A14: x in (proj (J,i)) " P ; ::_thesis: x in product ((Carrier J) +* (i,P))
then A15: x in dom (proj ((Carrier J),i)) by FUNCT_1:def_7;
then  x in product (Carrier J) ;
then consider g being Function such that
A16: x = g and
A17: dom g = dom (Carrier J) and
A18: for y being set st y in dom (Carrier J) holds
g . y in (Carrier J) . y by CARD_3:def_5;
A19: dom g = dom ((Carrier J) +* (i,P)) by A17, FUNCT_7:30;
 for j being set st j in dom ((Carrier J) +* (i,P)) holds
g . j in ((Carrier J) +* (i,P)) . j
proof
let j be set ; ::_thesis: ( j in dom ((Carrier J) +* (i,P)) implies g . j in ((Carrier J) +* (i,P)) . j )
assume  j in dom ((Carrier J) +* (i,P)) ; ::_thesis: g . j in ((Carrier J) +* (i,P)) . j
then A20: g . j in (Carrier J) . j by A17, A18, A19;
percases ( i = j or i <> j ) ;
supposeA21: i = j ; ::_thesis: g . j in ((Carrier J) +* (i,P)) . j
 (proj ((Carrier J),i)) . x = g . i by A15, A16, CARD_3:def_16;
then  g . i in P by A14, FUNCT_1:def_7;
hence  g . j in ((Carrier J) +* (i,P)) . j by A1, A21, FUNCT_7:31; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: g . j in ((Carrier J) +* (i,P)) . j
hence  g . j in ((Carrier J) +* (i,P)) . j by A20, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence  x in product ((Carrier J) +* (i,P)) by A16, A19, CARD_3:def_5; ::_thesis: verum
end;
hence  (proj (J,i)) " P = product ((Carrier J) +* (i,P)) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th5: :: WAYBEL18:5
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is continuous
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is continuous
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for i being Element of I holds proj (J,i) is continuous
let i be Element of I; ::_thesis: proj (J,i) is continuous
A1: for P being Subset of (J . i) st P is open holds
(proj (J,i)) " P is open
proof
let P be Subset of (J . i); ::_thesis: ( P is open implies (proj (J,i)) " P is open )
assume A2: P is open ; ::_thesis: (proj (J,i)) " P is open
 (proj (J,i)) " P c= product (Carrier J)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj (J,i)) " P or x in product (Carrier J) )
assume  x in (proj (J,i)) " P ; ::_thesis: x in product (Carrier J)
then  x in dom (proj ((Carrier J),i)) by FUNCT_1:def_7;
hence  x in product (Carrier J) ; ::_thesis: verum
end;
then reconsider x = (proj (J,i)) " P as Subset of (product (Carrier J)) ;
 product_prebasis J is prebasis of (product J) by Def3;
then A3: product_prebasis J c= the topology of (product J) by TOPS_2:64;
 x = product ((Carrier J) +* (i,P)) by Th4;
then  (proj (J,i)) " P in product_prebasis J by A2, Def2;
hence  (proj (J,i)) " P is open by A3, PRE_TOPC:def_2; ::_thesis: verum
end;
 [#] (J . i) <> {} ;
hence  proj (J,i) is continuous by A1, TOPS_2:43; ::_thesis: verum
end;

theorem Th6: :: WAYBEL18:6
for X being non empty TopSpace
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )
proof
let X be non empty TopSpace; ::_thesis: for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )
let f be Function of X,(product J); ::_thesis: ( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )
set B = product_prebasis J;
hereby  ::_thesis: ( ( for i being Element of I holds (proj (J,i)) * f is continuous ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for i being Element of I holds (proj (J,i)) * f is continuous
let i be Element of I; ::_thesis: (proj (J,i)) * f is continuous
 proj (J,i) is continuous by Th5;
hence  (proj (J,i)) * f is continuous by A1, TOPS_2:46; ::_thesis: verum
end;
assume A2: for i being Element of I holds (proj (J,i)) * f is continuous ; ::_thesis: f is continuous
A3: for P being Subset of (product J) st P in product_prebasis J holds
f " P is open
proof
let P be Subset of (product J); ::_thesis: ( P in product_prebasis J implies f " P is open )
reconsider p = P as Subset of (product (Carrier J)) by Def3;
assume  P in product_prebasis J ; ::_thesis: f " P is open
then consider i being set , T being TopStruct , V being Subset of T such that
A4: i in I and
A5: V is open and
A6: T = J . i and
A7: p = product ((Carrier J) +* (i,V)) by Def2;
reconsider j = i as Element of I by A4;
reconsider V = V as Subset of (J . j) by A6;
 ( (proj (J,j)) * f is continuous & [#] (J . j) <> {} ) by A2;
then A8: ((proj (J,j)) * f) " V is open by A5, A6, TOPS_2:43;
 (proj (J,j)) " V = p by A7, Th4;
hence  f " P is open by A8, RELAT_1:146; ::_thesis: verum
end;
 product_prebasis J is prebasis of (product J) by Def3;
hence  f is continuous by A3, YELLOW_9:36; ::_thesis: verum
end;

begin

definition
let Z be TopStruct ;
attrZ is injective  means :Def5: :: WAYBEL18:def 5
 for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f );
end;

:: deftheorem Def5 defines injective WAYBEL18:def_5_:_
 for Z being TopStruct holds
( Z is injective iff for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f ) );

theorem Th7: :: WAYBEL18:7
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective
proof
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is injective ) implies product J is injective )
assume A1: for i being Element of I holds J . i is injective ; ::_thesis: product J is injective
set B = product_prebasis J;
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for f being Function of X,(product J) st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
let f be Function of X,(product J); ::_thesis: ( f is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f ) )
assume A2: f is continuous ; ::_thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
let Y be non empty TopSpace; ::_thesis: ( X is SubSpace of Y implies ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f ) )
defpred S1[ set , set ] means  ex i1 being Element of I st
( i1 = $1 & ex g being Function of Y,(J . i1) st
( g is continuous & g | the carrier of X = (proj (J,i1)) * f & $2 = g ) );
assume A3: X is SubSpace of Y ; ::_thesis: ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
A4: for i being set st i in I holds
ex u being set st S1[i,u]
proof
let i be set ; ::_thesis: ( i in I implies ex u being set st S1[i,u] )
assume  i in I ; ::_thesis: ex u being set st S1[i,u]
then reconsider i1 = i as Element of I ;
 ( J . i1 is injective & (proj (J,i1)) * f is continuous ) by A1, A2, Th6;
then consider g being Function of Y,(J . i1) such that
A5: ( g is continuous & g | the carrier of X = (proj (J,i1)) * f ) by A3, Def5;
take  g ; ::_thesis: S1[i,g]
take  i1 ; ::_thesis: ( i1 = i & ex g being Function of Y,(J . i1) st
( g is continuous & g | the carrier of X = (proj (J,i1)) * f & g = g ) )
thus  ( i1 = i & ex g being Function of Y,(J . i1) st
( g is continuous & g | the carrier of X = (proj (J,i1)) * f & g = g ) ) by A5; ::_thesis: verum
end;
consider G being Function such that
A6: dom G = I and
A7: for i being set st i in I holds
S1[i,G . i] from CLASSES1:sch_1(A4);
A8: the carrier of Y c= dom <:G:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of Y or x in dom <:G:> )
consider i being set  such that
A9: i in I by XBOOLE_0:def_1;
assume A10: x in the carrier of Y ; ::_thesis: x in dom <:G:>
A11: for f9 being Function st f9 in rng G holds
x in dom f9
proof
let f9 be Function; ::_thesis: ( f9 in rng G implies x in dom f9 )
assume  f9 in rng G ; ::_thesis: x in dom f9
then consider k being set  such that
A12: k in dom G and
A13: f9 = G . k by FUNCT_1:def_3;
 ex i1 being Element of I st
( i1 = k & ex ff being Function of Y,(J . i1) st
( ff is continuous & ff | the carrier of X = (proj (J,i1)) * f & G . k = ff ) ) by A6, A7, A12;
hence  x in dom f9 by A10, A13, FUNCT_2:def_1; ::_thesis: verum
end;
consider j being Element of I such that
 j = i and
A14: ex g being Function of Y,(J . j) st
( g is continuous & g | the carrier of X = (proj (J,j)) * f & G . i = g ) by A7, A9;
consider g being Function of Y,(J . j) such that
 g is continuous and
 g | the carrier of X = (proj (J,j)) * f and
A15: G . i = g by A14;
 g in rng G by A6, A9, A15, FUNCT_1:def_3;
hence  x in dom <:G:> by A11, FUNCT_6:33; ::_thesis: verum
end;
A16: G is Function-yielding
proof
let j be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not j in dom G or G . j is set )
assume  j in dom G ; ::_thesis: G . j is set
then  ex i being Element of I st
( i = j & ex g being Function of Y,(J . i) st
( g is continuous & g | the carrier of X = (proj (J,i)) * f & G . j = g ) ) by A6, A7;
hence  G . j is set ; ::_thesis: verum
end;
A17: product (rngs G) c= product (Carrier J)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product (rngs G) or y in product (Carrier J) )
assume  y in product (rngs G) ; ::_thesis: y in product (Carrier J)
then consider h being Function such that
A18: y = h and
A19: dom h = dom (rngs G) and
A20: for x being set st x in dom (rngs G) holds
h . x in (rngs G) . x by CARD_3:def_5;
A21: dom h = I by A6, A16, A19, FUNCT_6:60
.= dom (Carrier J) by PARTFUN1:def_2 ;
 for x being set st x in dom (Carrier J) holds
h . x in (Carrier J) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier J) implies h . x in (Carrier J) . x )
assume A22: x in dom (Carrier J) ; ::_thesis: h . x in (Carrier J) . x
then A23: x in I ;
then consider i being Element of I such that
A24: i = x and
A25: ex g being Function of Y,(J . i) st
( g is continuous & g | the carrier of X = (proj (J,i)) * f & G . x = g ) by A7;
A26: ex R being 1-sorted st
( R = J . x & (Carrier J) . x = the carrier of R ) by A23, PRALG_1:def_13;
consider g being Function of Y,(J . i) such that
 g is continuous and
 g | the carrier of X = (proj (J,i)) * f and
A27: G . x = g by A25;
 x in dom G by A6, A22;
then A28: (rngs G) . x = rng g by A27, FUNCT_6:22;
 h . x in (rngs G) . x by A19, A20, A21, A22;
hence  h . x in (Carrier J) . x by A24, A28, A26; ::_thesis: verum
end;
hence  y in product (Carrier J) by A18, A21, CARD_3:def_5; ::_thesis: verum
end;
 dom <:G:> c= the carrier of Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:G:> or x in the carrier of Y )
assume A29: x in dom <:G:> ; ::_thesis: x in the carrier of Y
consider j being set  such that
A30: j in I by XBOOLE_0:def_1;
consider i being Element of I such that
 i = j and
A31: ex g being Function of Y,(J . i) st
( g is continuous & g | the carrier of X = (proj (J,i)) * f & G . j = g ) by A7, A30;
consider g being Function of Y,(J . i) such that
 g is continuous and
 g | the carrier of X = (proj (J,i)) * f and
A32: G . j = g by A31;
 g in rng G by A6, A30, A32, FUNCT_1:def_3;
then  x in dom g by A29, FUNCT_6:32;
hence  x in the carrier of Y ; ::_thesis: verum
end;
then A33: dom <:G:> = the carrier of Y by A8, XBOOLE_0:def_10;
 rng <:G:> c= product (rngs G) by FUNCT_6:29;
then A34: rng <:G:> c= product (Carrier J) by A17, XBOOLE_1:1;
then  rng <:G:> c= the carrier of (product J) by Def3;
then reconsider h = <:G:> as Function of the carrier of Y, the carrier of (product J) by A33, FUNCT_2:def_1, RELSET_1:4;
A35: dom (h | the carrier of X) = (dom h) /\ the carrier of X by RELAT_1:61
.= the carrier of Y /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X by A3, BORSUK_1:1, XBOOLE_1:28
.= dom f by FUNCT_2:def_1 ;
A36: for x being set st x in dom (h | the carrier of X) holds
(h | the carrier of X) . x = f . x
proof
let x be set ; ::_thesis: ( x in dom (h | the carrier of X) implies (h | the carrier of X) . x = f . x )
assume A37: x in dom (h | the carrier of X) ; ::_thesis: (h | the carrier of X) . x = f . x
then A38: x in dom h by RELAT_1:57;
 (h | the carrier of X) . x in rng (h | the carrier of X) by FUNCT_1:def_3, A37;
then  (h | the carrier of X) . x in the carrier of (product J) ;
then  (h | the carrier of X) . x in product (Carrier J) by Def3;
then consider z being Function such that
A39: (h | the carrier of X) . x = z and
A40: dom z = dom (Carrier J) and
 for i being set st i in dom (Carrier J) holds
z . i in (Carrier J) . i by CARD_3:def_5;
 f . x in rng f by A35, A37, FUNCT_1:def_3;
then  f . x in the carrier of (product J) ;
then A41: f . x in product (Carrier J) by Def3;
then consider y being Function such that
A42: f . x = y and
A43: dom y = dom (Carrier J) and
 for i being set st i in dom (Carrier J) holds
y . i in (Carrier J) . i by CARD_3:def_5;
A44: x in the carrier of Y by A38;
 for j being set st j in dom y holds
y . j = z . j
proof
let j be set ; ::_thesis: ( j in dom y implies y . j = z . j )
assume  j in dom y ; ::_thesis: y . j = z . j
then A45: j in I by A43;
then consider i being Element of I such that
A46: i = j and
A47: ex g being Function of Y,(J . i) st
( g is continuous & g | the carrier of X = (proj (J,i)) * f & G . j = g ) by A7;
A48: y in dom (proj ((Carrier J),i)) by A41, A42, CARD_3:def_16;
consider g being Function of Y,(J . i) such that
 g is continuous and
A49: g | the carrier of X = (proj (J,i)) * f and
A50: G . j = g by A47;
 ( x in dom h & z = <:G:> . x ) by A37, A44, A39, FUNCT_1:49, FUNCT_2:def_1;
hence z . j = g . x by A6, A45, A50, FUNCT_6:34
.= ((proj (J,i)) * f) . x by A37, A49, FUNCT_1:49
.= (proj ((Carrier J),i)) . y by A37, A42, FUNCT_2:15
.= y . j by A46, A48, CARD_3:def_16 ;
::_thesis: verum
end;
hence  (h | the carrier of X) . x = f . x by A42, A43, A39, A40, FUNCT_1:2; ::_thesis: verum
end;
reconsider h = h as Function of Y,(product J) ;
A51: for P being Subset of (product J) st P in product_prebasis J holds
h " P is open
proof
let P be Subset of (product J); ::_thesis: ( P in product_prebasis J implies h " P is open )
reconsider p = P as Subset of (product (Carrier J)) by Def3;
assume  P in product_prebasis J ; ::_thesis: h " P is open
then consider i being set , T being TopStruct , V being Subset of T such that
A52: i in I and
A53: V is open and
A54: T = J . i and
A55: p = product ((Carrier J) +* (i,V)) by Def2;
consider j being Element of I such that
A56: j = i and
A57: ex g being Function of Y,(J . j) st
( g is continuous & g | the carrier of X = (proj (J,j)) * f & G . i = g ) by A7, A52;
reconsider V = V as Subset of (J . j) by A54, A56;
A58: dom (proj (J,j)) = product (Carrier J) by CARD_3:def_16;
consider g being Function of Y,(J . j) such that
A59: g is continuous and
 g | the carrier of X = (proj (J,j)) * f and
A60: G . i = g by A57;
A61: dom g = the carrier of Y by FUNCT_2:def_1
.= dom h by FUNCT_2:def_1 ;
A62: (proj (J,j)) " V = p by A55, A56, Th4;
A63: h " P c= g " V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h " P or x in g " V )
assume A64: x in h " P ; ::_thesis: x in g " V
then A65: h . x in (proj (J,j)) " V by A62, FUNCT_1:def_7;
then  h . x in product (Carrier J) by A58, FUNCT_1:def_7;
then consider y being Function such that
A66: h . x = y and
 dom y = dom (Carrier J) and
 for i being set st i in dom (Carrier J) holds
y . i in (Carrier J) . i by CARD_3:def_5;
 h . x in dom (proj (J,j)) by A65, FUNCT_1:def_7;
then  (proj (J,j)) . (h . x) = y . j by A66, CARD_3:def_16;
then A67: y . j in V by A65, FUNCT_1:def_7;
 x in dom h by A64, FUNCT_1:def_7;
then A68: g . x = y . j by A6, A56, A60, A66, FUNCT_6:34;
 x in dom g by A61, A64, FUNCT_1:def_7;
hence  x in g " V by A67, A68, FUNCT_1:def_7; ::_thesis: verum
end;
A69: g " V c= h " P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g " V or x in h " P )
assume A70: x in g " V ; ::_thesis: x in h " P
then A71: x in dom h by A61, FUNCT_1:def_7;
then A72: h . x in rng h by FUNCT_1:def_3;
then consider y being Function such that
A73: h . x = y and
 dom y = dom (Carrier J) and
 for i being set st i in dom (Carrier J) holds
y . i in (Carrier J) . i by A34, CARD_3:def_5;
 h . x in product (Carrier J) by A34, A72;
then  y in dom (proj ((Carrier J),j)) by A73, CARD_3:def_16;
then A74: (proj (J,j)) . (h . x) = y . j by A73, CARD_3:def_16;
 g . x = y . j by A6, A56, A60, A71, A73, FUNCT_6:34;
then  (proj (J,j)) . (h . x) in V by A70, A74, FUNCT_1:def_7;
then  h . x in (proj (J,j)) " V by A34, A58, A72, FUNCT_1:def_7;
hence  x in h " P by A62, A71, FUNCT_1:def_7; ::_thesis: verum
end;
 [#] (J . j) <> {} ;
then  g " V is open by A53, A54, A56, A59, TOPS_2:43;
hence  h " P is open by A63, A69, XBOOLE_0:def_10; ::_thesis: verum
end;
take  h ; ::_thesis: ( h is continuous & h | the carrier of X = f )
 product_prebasis J is prebasis of (product J) by Def3;
hence  h is continuous by A51, YELLOW_9:36; ::_thesis: h | the carrier of X = f
thus  h | the carrier of X = f by A35, A36, FUNCT_1:2; ::_thesis: verum
end;

theorem :: WAYBEL18:8
for T being non empty TopSpace st T is injective holds
for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
proof
let T be non empty TopSpace; ::_thesis: ( T is injective implies for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective )
assume A1: T is injective ; ::_thesis: for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
let S be non empty SubSpace of T; ::_thesis: ( S is_a_retract_of T implies S is injective )
set p = incl S;
assume  S is_a_retract_of T ; ::_thesis: S is injective
then consider r being continuous Function of T,S such that
A2: r is being_a_retraction by BORSUK_1:def_17;
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for f being Function of X,S st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
let F be Function of X,S; ::_thesis: ( F is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A3: F is continuous ; ::_thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
reconsider f = (incl S) * F as Function of X,T ;
let Y be non empty TopSpace; ::_thesis: ( X is SubSpace of Y implies ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A4: X is SubSpace of Y ; ::_thesis: ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
 incl S is continuous by TMAP_1:87;
then consider g being Function of Y,T such that
A5: g is continuous and
A6: g | the carrier of X = f by A1, A3, A4, Def5;
take G = r * g; ::_thesis: ( G is continuous & G | the carrier of X = F )
A7: the carrier of S c= the carrier of T by BORSUK_1:1;
A8: the carrier of X c= the carrier of Y by A4, BORSUK_1:1;
A9: for x being set st x in dom F holds
F . x = G . x
proof
let x be set ; ::_thesis: ( x in dom F implies F . x = G . x )
assume A10: x in dom F ; ::_thesis: F . x = G . x
then A11: ( x in the carrier of X & g . x = f . x ) by A6, FUNCT_1:49;
A12: F . x in rng F by A10, FUNCT_1:def_3;
then  F . x in the carrier of S ;
then reconsider y = F . x as Point of T by A7;
A13: f . x = (incl S) . y by A10, FUNCT_2:15
.= F . x by A12, TMAP_1:84 ;
 F . x = r . y by A2, A12, BORSUK_1:def_16;
hence  F . x = G . x by A8, A13, A11, FUNCT_2:15; ::_thesis: verum
end;
thus  G is continuous by A5; ::_thesis: G | the carrier of X = F
A14: dom F = the carrier of X by FUNCT_2:def_1;
(dom G) /\ the carrier of X = the carrier of Y /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X by A4, BORSUK_1:1, XBOOLE_1:28 ;
hence  G | the carrier of X = F by A14, A9, FUNCT_1:46; ::_thesis: verum
end;

definition
let X be 1-sorted ;
let Y be TopStruct ;
let f be Function of X,Y;
func Image f ->  SubSpace of Y equals :: WAYBEL18:def 6
Y | (rng f);
coherence
 Y | (rng f) is SubSpace of Y ;
end;

:: deftheorem  defines Image WAYBEL18:def_6_:_
 for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds Image f = Y | (rng f);

registration
let X be non empty 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster Image f ->  non empty ;
coherence
 not Image f is empty ;
end;

theorem Th9: :: WAYBEL18:9
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f
proof
let X be 1-sorted ; ::_thesis: for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f
let Y be TopStruct ; ::_thesis: for f being Function of X,Y holds the carrier of (Image f) = rng f
let f be Function of X,Y; ::_thesis: the carrier of (Image f) = rng f
thus  the carrier of (Image f) = [#] (Y | (rng f))
.= rng f by PRE_TOPC:def_5 ; ::_thesis: verum
end;

definition
let X be 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
func corestr f ->  Function of X,(Image f) equals :: WAYBEL18:def 7
f;
coherence
 f is Function of X,(Image f)
proof
 ( the carrier of (Image f) = rng f & the carrier of X = dom f ) by Th9, FUNCT_2:def_1;
hence  f is Function of X,(Image f) by FUNCT_2:1; ::_thesis: verum
end;
end;

:: deftheorem  defines corestr WAYBEL18:def_7_:_
 for X being 1-sorted
for Y being non empty TopStruct
for f being Function of X,Y holds corestr f = f;

theorem Th10: :: WAYBEL18:10
for X, Y being non empty TopSpace
for f being Function of X,Y st f is continuous holds
corestr f is continuous
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y st f is continuous holds
corestr f is continuous
let f be Function of X,Y; ::_thesis: ( f is continuous implies corestr f is continuous )
A1: f is Function of (dom f),(rng f) by FUNCT_2:1;
A2: [#] Y <> {} ;
assume A3: f is continuous ; ::_thesis: corestr f is continuous
A4: for R being Subset of (Image f) st R is open holds
(corestr f) " R is open
proof
 [#] (Image f) = rng f by Th9;
then A5: f " ([#] (Image f)) = dom f by A1, FUNCT_2:40
.= the carrier of X by FUNCT_2:def_1 ;
 the carrier of X in the topology of X by PRE_TOPC:def_1;
then A6: f " ([#] (Image f)) is open by A5, PRE_TOPC:def_2;
let R be Subset of (Image f); ::_thesis: ( R is open implies (corestr f) " R is open )
assume  R is open ; ::_thesis: (corestr f) " R is open
then  R in the topology of (Image f) by PRE_TOPC:def_2;
then consider Q being Subset of Y such that
A7: Q in the topology of Y and
A8: R = Q /\ ([#] (Image f)) by PRE_TOPC:def_4;
reconsider Q = Q as Subset of Y ;
 Q is open by A7, PRE_TOPC:def_2;
then A9: f " Q is open by A3, A2, TOPS_2:43;
 (f " Q) /\ (f " ([#] (Image f))) = f " (Q /\ ([#] (Image f))) by FUNCT_1:68;
hence  (corestr f) " R is open by A8, A9, A6, TOPS_1:11; ::_thesis: verum
end;
 [#] (Image f) <> {} ;
hence  corestr f is continuous by A4, TOPS_2:43; ::_thesis: verum
end;

registration
let X be 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster corestr f ->  onto ;
coherence
 corestr f is onto
proof
 the carrier of (Image f) = rng (corestr f) by Th9;
hence  corestr f is onto by FUNCT_2:def_3; ::_thesis: verum
end;
end;

definition
let X, Y be TopStruct ;
predX is_Retract_of Y means :: WAYBEL18:def 8
 ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic );
end;

:: deftheorem  defines is_Retract_of WAYBEL18:def_8_:_
 for X, Y being TopStruct holds
( X is_Retract_of Y iff ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic ) );

theorem Th11: :: WAYBEL18:11
for T, S being non empty TopSpace st T is injective holds
for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S
proof
let T, S be non empty TopSpace; ::_thesis: ( T is injective implies for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S )
assume A1: T is injective ; ::_thesis: for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S
let f be Function of T,S; ::_thesis: ( corestr f is being_homeomorphism implies T is_Retract_of S )
consider g being Function of (Image f),T such that
A2: g = (corestr f) " ;
assume A3: corestr f is being_homeomorphism ; ::_thesis: T is_Retract_of S
then  g is continuous by A2, TOPS_2:def_5;
then consider h being Function of S,T such that
A4: h is continuous and
A5: h | the carrier of (Image f) = g by A1, Def5;
 g is being_homeomorphism by A3, A2, TOPS_2:56;
then A6: g is one-to-one by TOPS_2:def_5;
A7: the carrier of (Image f) = rng f by Th9;
A8: for x being set st x in the carrier of T holds
(h * f) . x = x
proof
let x be set ; ::_thesis: ( x in the carrier of T implies (h * f) . x = x )
assume A9: x in the carrier of T ; ::_thesis: (h * f) . x = x
then A10: x in dom (corestr f) by FUNCT_2:def_1;
A11: x in dom f by A9, FUNCT_2:def_1;
then A12: f . x in rng f by FUNCT_1:def_3;
A13: corestr f is one-to-one by A3, TOPS_2:def_5;
thus (h * f) . x = h . (f . x) by A11, FUNCT_1:13
.= ((corestr f) ") . ((corestr f) . x) by A2, A5, A7, A12, FUNCT_1:49
.= ((corestr f) ") . ((corestr f) . x) by A13, TOPS_2:def_4
.= x by A10, A13, FUNCT_1:34 ; ::_thesis: verum
end;
 dom (h * f) = the carrier of T by FUNCT_2:def_1;
then A14: h * f = id the carrier of T by A8, FUNCT_1:17;
take F = f * h; :: according to WAYBEL18:def_8 ::_thesis: ( F is continuous & F * F = F & Image F,T are_homeomorphic )
set H = h * (incl (Image F));
A15: dom (h * (incl (Image F))) = [#] (Image F) by FUNCT_2:def_1;
 rng h c= the carrier of T ;
then A16: rng h c= dom f by FUNCT_2:def_1;
A17: rng F c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in rng f )
assume  y in rng F ; ::_thesis: y in rng f
then consider x being set  such that
A18: x in dom F and
A19: y = F . x by FUNCT_1:def_3;
 x in the carrier of S by A18;
then A20: x in dom h by FUNCT_2:def_1;
then A21: h . x in rng h by FUNCT_1:def_3;
 f . (h . x) = y by A19, A20, FUNCT_1:13;
hence  y in rng f by A16, A21, FUNCT_1:def_3; ::_thesis: verum
end;
A22: h * (incl (Image F)) is one-to-one
proof
let x, y be Element of (Image F); :: according to WAYBEL_1:def_1 ::_thesis: ( not (h * (incl (Image F))) . x = (h * (incl (Image F))) . y or x = y )
assume A23: (h * (incl (Image F))) . x = (h * (incl (Image F))) . y ; ::_thesis: x = y
A24: x in the carrier of (Image F) ;
then A25: x in dom (incl (Image F)) by FUNCT_2:def_1;
A26: y in the carrier of (Image F) ;
then A27: y in dom (incl (Image F)) by FUNCT_2:def_1;
A28: y in rng F by A26, Th9;
A29: x in rng F by A24, Th9;
then reconsider a = x, b = y as Point of S by A28;
reconsider x9 = x, y9 = y as Element of (Image f) by A17, A29, A28, Th9;
g . x9 = h . x by A5, FUNCT_1:49
.= h . ((incl (Image F)) . a) by TMAP_1:84
.= (h * (incl (Image F))) . b by A23, A25, FUNCT_1:13
.= h . ((incl (Image F)) . b) by A27, FUNCT_1:13
.= h . y by TMAP_1:84
.= g . y9 by A5, FUNCT_1:49 ;
hence  x = y by A6, WAYBEL_1:def_1; ::_thesis: verum
end;
A30: dom (incl (Image F)) = the carrier of (Image F) by FUNCT_2:def_1;
A31: rng (h * (incl (Image F))) = [#] T
proof
thus  rng (h * (incl (Image F))) c= [#] T ; :: according to XBOOLE_0:def_10 ::_thesis: [#] T c= rng (h * (incl (Image F)))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] T or y in rng (h * (incl (Image F))) )
assume A32: y in [#] T ; ::_thesis: y in rng (h * (incl (Image F)))
then A33: y in dom f by FUNCT_2:def_1;
then A34: F . (f . y) = ((f * h) * f) . y by FUNCT_1:13
.= (f * (id T)) . y by A14, RELAT_1:36
.= f . y by FUNCT_2:17 ;
A35: f . y in rng f by A33, FUNCT_1:def_3;
then reconsider pp = f . y as Point of S ;
 f . y in the carrier of S by A35;
then A36: f . y in dom F by FUNCT_2:def_1;
then  F . (f . y) in rng F by FUNCT_1:def_3;
then A37: f . y in the carrier of (Image F) by A34, Th9;
then A38: y in dom ((incl (Image F)) * f) by A30, A33, FUNCT_1:11;
 dom (h * (incl (Image F))) = rng F by A15, Th9;
then A39: f . y in dom (h * (incl (Image F))) by A36, A34, FUNCT_1:def_3;
(h * (incl (Image F))) . (f . y) = ((h * (incl (Image F))) * f) . y by A33, FUNCT_1:13
.= (h * ((incl (Image F)) * f)) . y by RELAT_1:36
.= h . (((incl (Image F)) * f) . y) by A38, FUNCT_1:13
.= h . ((incl (Image F)) . pp) by A33, FUNCT_1:13
.= h . (f . y) by A37, TMAP_1:84
.= (id T) . y by A14, A33, FUNCT_1:13
.= y by A32, FUNCT_1:18 ;
hence  y in rng (h * (incl (Image F))) by A39, FUNCT_1:def_3; ::_thesis: verum
end;
reconsider p = incl (Image f) as Function of (Image f),S ;
A40: [#] S <> {} ;
A41: dom (p * (corestr f)) = the carrier of T by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
A42: for P being Subset of S holds f " P = (p * (corestr f)) " P
proof
let P be Subset of S; ::_thesis: f " P = (p * (corestr f)) " P
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (p * (corestr f)) " P c= f " P
let x be set ; ::_thesis: ( x in f " P implies x in (p * (corestr f)) " P )
assume A43: x in f " P ; ::_thesis: x in (p * (corestr f)) " P
then A44: x in dom f by FUNCT_1:def_7;
then  f . x in rng f by FUNCT_1:def_3;
then A45: f . x in the carrier of (Image f) by Th9;
A46: f . x in P by A43, FUNCT_1:def_7;
then reconsider y = f . x as Point of S ;
(p * (corestr f)) . x = p . (f . x) by A44, FUNCT_1:13
.= y by A45, TMAP_1:84 ;
hence  x in (p * (corestr f)) " P by A41, A44, A46, FUNCT_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (p * (corestr f)) " P or x in f " P )
assume A47: x in (p * (corestr f)) " P ; ::_thesis: x in f " P
then A48: x in dom (p * (corestr f)) by FUNCT_1:def_7;
then A49: f . x in rng f by A41, FUNCT_1:def_3;
then reconsider y = f . x as Point of S ;
A50: (p * (corestr f)) . x in P by A47, FUNCT_1:def_7;
A51: f . x in the carrier of (Image f) by A49, Th9;
(p * (corestr f)) . x = p . (f . x) by A41, A48, FUNCT_1:13
.= y by A51, TMAP_1:84 ;
hence  x in f " P by A41, A48, A50, FUNCT_1:def_7; ::_thesis: verum
end;
A52: corestr f is continuous by A3, TOPS_2:def_5;
A53: for P being Subset of (Image F) st P is open holds
((h * (incl (Image F))) ") " P is open
proof
let P be Subset of (Image F); ::_thesis: ( P is open implies ((h * (incl (Image F))) ") " P is open )
A54: p is continuous by TMAP_1:87;
 (incl (Image F)) .: P = P
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P c= (incl (Image F)) .: P
let y be set ; ::_thesis: ( y in (incl (Image F)) .: P implies y in P )
assume  y in (incl (Image F)) .: P ; ::_thesis: y in P
then consider x being set  such that
A55: x in dom (incl (Image F)) and
A56: ( x in P & y = (incl (Image F)) . x ) by FUNCT_1:def_6;
 x in the carrier of (Image F) by A55;
then  x in rng F by Th9;
then reconsider xx = x as Point of S ;
 (incl (Image F)) . xx = x by A55, TMAP_1:84;
hence  y in P by A56; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P or y in (incl (Image F)) .: P )
assume A57: y in P ; ::_thesis: y in (incl (Image F)) .: P
then A58: y in the carrier of (Image F) ;
then  y in rng F by Th9;
then reconsider yy = y as Point of S ;
A59: yy = (incl (Image F)) . y by A57, TMAP_1:84;
 y in dom (incl (Image F)) by A58, FUNCT_2:def_1;
hence  y in (incl (Image F)) .: P by A57, A59, FUNCT_1:def_6; ::_thesis: verum
end;
then A60: (h * (incl (Image F))) .: P = h .: P by RELAT_1:126;
assume  P is open ; ::_thesis: ((h * (incl (Image F))) ") " P is open
then  P in the topology of (Image F) by PRE_TOPC:def_2;
then consider Q being Subset of S such that
A61: Q in the topology of S and
A62: P = Q /\ ([#] (Image F)) by PRE_TOPC:def_4;
reconsider Q = Q as Subset of S ;
A63: f " Q = h .: P
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: h .: P c= f " Q
let x be set ; ::_thesis: ( x in f " Q implies x in h .: P )
assume A64: x in f " Q ; ::_thesis: x in h .: P
then A65: x in dom f by FUNCT_1:def_7;
then A66: h . (f . x) = (id T) . x by A14, FUNCT_1:13
.= x by A64, FUNCT_1:18 ;
 f . x in rng f by A65, FUNCT_1:def_3;
then A67: f . x in the carrier of S ;
then A68: f . x in dom h by FUNCT_2:def_1;
A69: f . x in dom F by A67, FUNCT_2:def_1;
F . (f . x) = f . (h . (f . x)) by A68, FUNCT_1:13
.= f . ((id T) . x) by A14, A65, FUNCT_1:13
.= f . x by A64, FUNCT_1:18 ;
then  f . x in rng F by A69, FUNCT_1:def_3;
then A70: f . x in the carrier of (Image F) by Th9;
 f . x in Q by A64, FUNCT_1:def_7;
then  f . x in P by A62, A70, XBOOLE_0:def_4;
hence  x in h .: P by A68, A66, FUNCT_1:def_6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h .: P or x in f " Q )
assume  x in h .: P ; ::_thesis: x in f " Q
then consider y being set  such that
A71: y in dom h and
A72: y in P and
A73: x = h . y by FUNCT_1:def_6;
A74: y in Q by A62, A72, XBOOLE_0:def_4;
 y in the carrier of (Image F) by A72;
then A75: y in rng F by Th9;
A76: x in rng h by A71, A73, FUNCT_1:def_3;
then  f . x in rng f by A16, FUNCT_1:def_3;
then reconsider a = f . x, b = y as Element of (Image f) by A17, A75, Th9;
g . a = h . (f . x) by A5, FUNCT_1:49
.= (id T) . x by A16, A14, A76, FUNCT_1:13
.= h . y by A73, A76, FUNCT_1:18
.= g . b by A5, FUNCT_1:49 ;
then  f . x in Q by A6, A74, WAYBEL_1:def_1;
hence  x in f " Q by A16, A76, FUNCT_1:def_7; ::_thesis: verum
end;
 Q is open by A61, PRE_TOPC:def_2;
then  (p * (corestr f)) " Q is open by A40, A52, A54, TOPS_2:43;
then  f " Q is open by A42;
hence  ((h * (incl (Image F))) ") " P is open by A31, A22, A63, A60, TOPS_2:54; ::_thesis: verum
end;
A77: p is continuous by TMAP_1:87;
A78: [#] T <> {} ;
 for P being Subset of S st P is open holds
F " P is open
proof
let P be Subset of S; ::_thesis: ( P is open implies F " P is open )
assume  P is open ; ::_thesis: F " P is open
then  (p * (corestr f)) " P is open by A40, A52, A77, TOPS_2:43;
then  f " P is open by A42;
then  h " (f " P) is open by A78, A4, TOPS_2:43;
hence  F " P is open by RELAT_1:146; ::_thesis: verum
end;
hence  F is continuous by A40, TOPS_2:43; ::_thesis: ( F * F = F & Image F,T are_homeomorphic )
thus F * F = ((f * h) * f) * h by RELAT_1:36
.= (f * (id T)) * h by A14, RELAT_1:36
.= F by FUNCT_2:17 ; ::_thesis: Image F,T are_homeomorphic
 [#] (Image F) <> {} ;
then  ( incl (Image F) is continuous & (h * (incl (Image F))) " is continuous ) by A53, TMAP_1:87, TOPS_2:43;
then  h * (incl (Image F)) is being_homeomorphism by A4, A15, A31, A22, TOPS_2:def_5;
hence  Image F,T are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;

definition
func Sierpinski_Space  ->  strict TopStruct  means :Def9: :: WAYBEL18:def 9
( the carrier of it = {0,1} & the topology of it = {{},{1},{0,1}} );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} )
proof
set c = {0,1};
set t = {{},{1},{0,1}};
 {{},{1},{0,1}} c= bool {0,1}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{},{1},{0,1}} or x in bool {0,1} )
assume A1: x in {{},{1},{0,1}} ; ::_thesis: x in bool {0,1}
percases ( x = {} or x = {1} or x = {0,1} ) by A1, ENUMSET1:def_1;
supposeA2: x = {} ; ::_thesis: x in bool {0,1}
 {} c= {0,1} by XBOOLE_1:2;
hence  x in bool {0,1} by A2; ::_thesis: verum
end;
suppose x = {1} ; ::_thesis: x in bool {0,1}
then  x c= {0,1} by ZFMISC_1:7;
hence  x in bool {0,1} ; ::_thesis: verum
end;
suppose x = {0,1} ; ::_thesis: x in bool {0,1}
then  x c= {0,1} ;
hence  x in bool {0,1} ; ::_thesis: verum
end;
end;
end;
then reconsider t = {{},{1},{0,1}} as Subset-Family of {0,1} ;
take s = TopStruct(# {0,1},t #); ::_thesis: ( the carrier of s = {0,1} & the topology of s = {{},{1},{0,1}} )
thus  the carrier of s = {0,1} ; ::_thesis: the topology of s = {{},{1},{0,1}}
thus  the topology of s = {{},{1},{0,1}} ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopStruct st the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} & the carrier of b2 = {0,1} & the topology of b2 = {{},{1},{0,1}} holds
b1 = b2 ;
end;

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def_9_:_
 for b1 being strict TopStruct holds
( b1 = Sierpinski_Space iff ( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} ) );

registration
cluster Sierpinski_Space  ->  non empty strict TopSpace-like ;
coherence
 ( not Sierpinski_Space is empty & Sierpinski_Space is TopSpace-like )
proof
set IT = Sierpinski_Space ;
thus  not Sierpinski_Space is empty by Def9; ::_thesis: Sierpinski_Space is TopSpace-like
 {0,1} in {{},{1},{0,1}} by ENUMSET1:def_1;
then  the carrier of Sierpinski_Space in {{},{1},{0,1}} by Def9;
hence  the carrier of Sierpinski_Space in the topology of Sierpinski_Space by Def9; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of Sierpinski_Space)) holds
( not b1 c= the topology of Sierpinski_Space or union b1 in the topology of Sierpinski_Space ) ) & ( for b1, b2 being Element of K19( the carrier of Sierpinski_Space) holds
( not b1 in the topology of Sierpinski_Space or not b2 in the topology of Sierpinski_Space or b1 /\ b2 in the topology of Sierpinski_Space ) ) )
thus  for a being Subset-Family of Sierpinski_Space st a c= the topology of Sierpinski_Space holds
union a in the topology of Sierpinski_Space ::_thesis: for b1, b2 being Element of K19( the carrier of Sierpinski_Space) holds
( not b1 in the topology of Sierpinski_Space or not b2 in the topology of Sierpinski_Space or b1 /\ b2 in the topology of Sierpinski_Space )
proof
let a be Subset-Family of Sierpinski_Space; ::_thesis: ( a c= the topology of Sierpinski_Space implies union a in the topology of Sierpinski_Space )
assume  a c= the topology of Sierpinski_Space ; ::_thesis: union a in the topology of Sierpinski_Space
then A1: a c= {{},{1},{0,1}} by Def9;
percases ( a = {} or a = {{}} or a = {{1}} or a = {{0,1}} or a = {{},{1}} or a = {{1},{0,1}} or a = {{},{0,1}} or a = {{},{1},{0,1}} ) by A1, ZFMISC_1:118;
suppose a = {} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1, ZFMISC_1:2;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {} by ZFMISC_1:25;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {1} by ZFMISC_1:25;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{0,1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {0,1} by ZFMISC_1:25;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{},{1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {} \/ {1} by ZFMISC_1:75;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{1},{0,1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9 ;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{},{0,1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  union a = {} \/ {0,1} by ZFMISC_1:75;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose a = {{},{1},{0,1}} ; ::_thesis: union a in the topology of Sierpinski_Space
then  a = {{}} \/ {{1},{0,1}} by ENUMSET1:2;
then  union a = (union {{}}) \/ (union {{1},{0,1}}) by ZFMISC_1:78
.= {} \/ (union {{1},{0,1}}) by ZFMISC_1:25
.= {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9 ;
then  union a in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  union a in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
end;
end;
let a, b be Subset of Sierpinski_Space; ::_thesis: ( not a in the topology of Sierpinski_Space or not b in the topology of Sierpinski_Space or a /\ b in the topology of Sierpinski_Space )
assume  ( a in the topology of Sierpinski_Space & b in the topology of Sierpinski_Space ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then A2: ( a in {{},{1},{0,1}} & b in {{},{1},{0,1}} ) by Def9;
percases ( ( a = {} & b = {} ) or ( a = {} & b = {1} ) or ( a = {} & b = {0,1} ) or ( a = {1} & b = {} ) or ( a = {1} & b = {1} ) or ( a = {1} & b = {0,1} ) or ( a = {0,1} & b = {} ) or ( a = {0,1} & b = {1} ) or ( a = {0,1} & b = {0,1} ) ) by A2, ENUMSET1:def_1;
suppose ( a = {} & b = {} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {} & b = {1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {} & b = {0,1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {1} & b = {} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {1} & b = {1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {1} & b = {0,1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b = {1} by ZFMISC_1:13;
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {0,1} & b = {} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {0,1} & b = {1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b = {1} by ZFMISC_1:13;
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
suppose ( a = {0,1} & b = {0,1} ) ; ::_thesis: a /\ b in the topology of Sierpinski_Space
then  a /\ b in {{},{1},{0,1}} by ENUMSET1:def_1;
hence  a /\ b in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
end;
end;
end;

Lm1:  Sierpinski_Space is T_0
proof
set S = Sierpinski_Space ;
 for x, y being Point of Sierpinski_Space st x <> y holds
ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
proof
set V = {1};
let x, y be Point of Sierpinski_Space; ::_thesis: ( x <> y implies ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) )
 y in the carrier of Sierpinski_Space ;
then A1: y in {0,1} by Def9;
 {1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
 x in the carrier of Sierpinski_Space ;
then  x in {0,1} by Def9;
then A2: ( x = 0 or x = 1 ) by TARSKI:def_2;
 {1} in {{},{1},{0,1}} by ENUMSET1:def_1;
then  {1} in the topology of Sierpinski_Space by Def9;
then A3: V is open by PRE_TOPC:def_2;
assume A4: x <> y ; ::_thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
percases ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) ) by A4, A1, A2, TARSKI:def_2;
suppose ( x = 0 & y = 1 ) ; ::_thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
then  ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by TARSKI:def_1;
hence  ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A3; ::_thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; ::_thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
then  ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by TARSKI:def_1;
hence  ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A3; ::_thesis: verum
end;
end;
end;
hence  Sierpinski_Space is T_0 by T_0TOPSP:def_7; ::_thesis: verum
end;

registration
cluster Sierpinski_Space  ->  strict T_0 ;
coherence
 Sierpinski_Space is T_0 by Lm1;
end;

registration
cluster Sierpinski_Space  ->  strict injective ;
coherence
 Sierpinski_Space is injective
proof
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for f being Function of X,Sierpinski_Space st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Sierpinski_Space st
( g is continuous & g | the carrier of X = f )
set S = Sierpinski_Space ;
let f be Function of X,Sierpinski_Space; ::_thesis: ( f is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Sierpinski_Space st
( g is continuous & g | the carrier of X = f ) )
A1: [#] Sierpinski_Space <> {} ;
 {1} c= {0,1} by ZFMISC_1:7;
then reconsider u = {1} as Subset of Sierpinski_Space by Def9;
 u in {{},{1},{0,1}} by ENUMSET1:def_1;
then  u in the topology of Sierpinski_Space by Def9;
then A2: u is open by PRE_TOPC:def_2;
assume  f is continuous ; ::_thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Sierpinski_Space st
( g is continuous & g | the carrier of X = f )
then  f " u is open by A1, A2, TOPS_2:43;
then A3: f " u in the topology of X by PRE_TOPC:def_2;
let Y be non empty TopSpace; ::_thesis: ( X is SubSpace of Y implies ex g being Function of Y,Sierpinski_Space st
( g is continuous & g | the carrier of X = f ) )
assume A4: X is SubSpace of Y ; ::_thesis: ex g being Function of Y,Sierpinski_Space st
( g is continuous & g | the carrier of X = f )
then consider V being Subset of Y such that
A5: V in the topology of Y and
A6: f " u = V /\ ([#] X) by A3, PRE_TOPC:def_4;
reconsider V = V as Subset of Y ;
set g = chi (V, the carrier of Y);
A7: dom (chi (V, the carrier of Y)) = the carrier of Y by FUNCT_3:def_3;
reconsider g = chi (V, the carrier of Y) as Function of Y,Sierpinski_Space by Def9;
A8: the carrier of X c= the carrier of Y by A4, BORSUK_1:1;
A9: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A10: x in dom f ; ::_thesis: f . x = g . x
then A11: x in the carrier of X ;
percases ( x in V or not x in V ) ;
supposeA12: x in V ; ::_thesis: f . x = g . x
then  x in f " u by A6, A10, XBOOLE_0:def_4;
then A13: f . x in {1} by FUNCT_1:def_7;
 g . x = 1 by A12, FUNCT_3:def_3;
hence  f . x = g . x by A13, TARSKI:def_1; ::_thesis: verum
end;
supposeA14: not x in V ; ::_thesis: f . x = g . x
 f . x in rng f by A10, FUNCT_1:def_3;
then  f . x in the carrier of Sierpinski_Space ;
then  f . x in {0,1} by Def9;
then A15: ( f . x = 0 or f . x = 1 ) by TARSKI:def_2;
 not x in f " {1} by A6, A14, XBOOLE_0:def_4;
then  ( not x in dom f or not f . x in {1} ) by FUNCT_1:def_7;
hence  f . x = g . x by A8, A10, A11, A14, A15, FUNCT_3:def_3, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
take  g ; ::_thesis: ( g is continuous & g | the carrier of X = f )
A16: V is open by A5, PRE_TOPC:def_2;
 for P being Subset of Sierpinski_Space st P is open holds
g " P is open
proof
let P be Subset of Sierpinski_Space; ::_thesis: ( P is open implies g " P is open )
assume  P is open ; ::_thesis: g " P is open
then  P in the topology of Sierpinski_Space by PRE_TOPC:def_2;
then A17: P in {{},{1},{0,1}} by Def9;
percases ( P = {} or P = {1} or P = {0,1} ) by A17, ENUMSET1:def_1;
suppose P = {} ; ::_thesis: g " P is open
then  g " P = {} ;
then  g " P in the topology of Y by PRE_TOPC:1;
hence  g " P is open by PRE_TOPC:def_2; ::_thesis: verum
end;
supposeA18: P = {1} ; ::_thesis: g " P is open
A19: g " P c= V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g " P or x in V )
assume A20: x in g " P ; ::_thesis: x in V
then  g . x in {1} by A18, FUNCT_1:def_7;
then  g . x = 1 by TARSKI:def_1;
hence  x in V by A20, FUNCT_3:def_3; ::_thesis: verum
end;
 V c= g " P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in g " P )
assume A21: x in V ; ::_thesis: x in g " P
then  g . x = 1 by FUNCT_3:def_3;
then  g . x in {1} by TARSKI:def_1;
hence  x in g " P by A7, A18, A21, FUNCT_1:def_7; ::_thesis: verum
end;
hence  g " P is open by A16, A19, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose P = {0,1} ; ::_thesis: g " P is open
then  g " P = the carrier of Y by FUNCT_2:40;
then  g " P in the topology of Y by PRE_TOPC:def_1;
hence  g " P is open by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
hence  g is continuous by A1, TOPS_2:43; ::_thesis: g | the carrier of X = f
(dom g) /\ the carrier of X = the carrier of Y /\ the carrier of X by FUNCT_3:def_3
.= the carrier of X by A4, BORSUK_1:1, XBOOLE_1:28
.= dom f by FUNCT_2:def_1 ;
hence  g | the carrier of X = f by A9, FUNCT_1:46; ::_thesis: verum
end;
end;

registration
let I be set ;
let S be non empty 1-sorted ;
clusterI --> S ->  non-Empty ;
coherence
 I --> S is non-Empty
proof
let s be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not s in rng (I --> S) or not s is empty )
assume  s in rng (I --> S) ; ::_thesis: not s is empty
hence  not s is empty by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be set ;
let T be TopStruct ;
clusterI --> T ->  TopStruct-yielding ;
coherence
 I --> T is TopStruct-yielding
proof
let x be set ; :: according to WAYBEL18:def_1 ::_thesis: ( x in rng (I --> T) implies x is TopStruct )
assume  x in rng (I --> T) ; ::_thesis: x is TopStruct
hence  x is TopStruct by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let L be non empty antisymmetric RelStr ;
cluster product (I --> L) ->  antisymmetric ;
coherence
 product (I --> L) is antisymmetric
proof
 for i being Element of I holds (I --> L) . i is antisymmetric by FUNCOP_1:7;
hence  product (I --> L) is antisymmetric by WAYBEL_3:30; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let L be non empty transitive RelStr ;
cluster product (I --> L) ->  transitive ;
coherence
 product (I --> L) is transitive
proof
 for i being Element of I holds (I --> L) . i is transitive by FUNCOP_1:7;
hence  product (I --> L) is transitive by WAYBEL_3:29; ::_thesis: verum
end;
end;

theorem :: WAYBEL18:12
for T being Scott TopAugmentation of BoolePoset 1 holds the topology of T = the topology of Sierpinski_Space
proof
let T be Scott TopAugmentation of BoolePoset 1; ::_thesis: the topology of T = the topology of Sierpinski_Space
A1: LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def_2;
A2: RelStr(# the carrier of T, the InternalRel of T #) = BoolePoset 1 by YELLOW_9:def_4;
then A3: the carrier of T = the carrier of (LattPOSet (BooleLatt 1)) by YELLOW_1:def_2
.= bool 1 by A1, LATTICE3:def_1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
then reconsider j = 1, z = 0 as Element of (BoolePoset 1) by A2, TARSKI:def_2;
A4: now__::_thesis:_for_x_being_set_st_x_in_the_topology_of_Sierpinski_Space_holds_
x_in_the_topology_of_T
let x be set ; ::_thesis: ( x in the topology of Sierpinski_Space implies b1 in the topology of T )
assume  x in the topology of Sierpinski_Space ; ::_thesis: b1 in the topology of T
then A5: x in {{},{1},{0,1}} by Def9;
percases ( x = {} or x = {1} or x = {0,1} ) by A5, ENUMSET1:def_1;
suppose x = {} ; ::_thesis: b1 in the topology of T
hence  x in the topology of T by PRE_TOPC:1; ::_thesis: verum
end;
supposeA6: x = {1} ; ::_thesis: b1 in the topology of T
then reconsider x9 = x as Subset of T by A3, ZFMISC_1:7;
 for a, b being Element of T st a in x9 & a <= b holds
b in x9
proof
let a, b be Element of T; ::_thesis: ( a in x9 & a <= b implies b in x9 )
assume that
A7: a in x9 and
A8: a <= b ; ::_thesis: b in x9
A9: a = 1 by A6, A7, TARSKI:def_1;
A10: b <> 0
proof
assume A11: b = 0 ; ::_thesis: contradiction
 [a,b] in the InternalRel of T by A8, ORDERS_2:def_5;
then  j <= z by A2, A9, A11, ORDERS_2:def_5;
then  1 c= 0 by YELLOW_1:2;
hence  contradiction ; ::_thesis: verum
end;
 ( b = 0 or b = 1 ) by A3, TARSKI:def_2;
hence  b in x9 by A6, A10, TARSKI:def_1; ::_thesis: verum
end;
then A12: x9 is upper by WAYBEL_0:def_20;
 for D being non empty directed Subset of T st sup D in x9 holds
D meets x9
proof
let D be non empty directed Subset of T; ::_thesis: ( sup D in x9 implies D meets x9 )
assume A13: sup D in x9 ; ::_thesis: D meets x9
 D <> {0}
proof
assume  D = {0} ; ::_thesis: contradiction
then  sup D = sup {z} by A2, YELLOW_0:17, YELLOW_0:26
.= 0 by YELLOW_0:39 ;
hence  contradiction by A6, A13, TARSKI:def_1; ::_thesis: verum
end;
then  ( D = {1} or D = {0,1} ) by A3, ZFMISC_1:36;
then A14: 1 in D by TARSKI:def_1, TARSKI:def_2;
 1 in x9 by A6, TARSKI:def_1;
hence  D meets x9 by A14, XBOOLE_0:3; ::_thesis: verum
end;
then  x9 is inaccessible by WAYBEL11:def_1;
then  x9 is open by A12, WAYBEL11:def_4;
hence  x in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
suppose x = {0,1} ; ::_thesis: b1 in the topology of T
hence  x in the topology of T by A3, PRE_TOPC:def_1; ::_thesis: verum
end;
end;
end;
reconsider c = {z} as Subset of T by A2;
now__::_thesis:_for_y_being_set_st_y_in_the_topology_of_T_holds_
y_in_the_topology_of_Sierpinski_Space
set a = 0 ;
set b = 1;
let y be set ; ::_thesis: ( y in the topology of T implies y in the topology of Sierpinski_Space )
A15: not 1 in {z} by TARSKI:def_1;
 ( 0 c= 1 & 0 in {z} ) by TARSKI:def_1, XBOOLE_1:2;
then  not {z} is upper by A15, WAYBEL_7:7;
then  not c is upper by A2, WAYBEL_0:25;
then A16: not c is open by WAYBEL11:def_4;
assume A17: y in the topology of T ; ::_thesis: y in the topology of Sierpinski_Space
then reconsider x = y as Subset of T ;
 ( x = {} or x = {0} or x = {1} or x = {0,1} ) by A3, ZFMISC_1:36;
then  y in {{},{1},{0,1}} by A17, A16, ENUMSET1:def_1, PRE_TOPC:def_2;
hence  y in the topology of Sierpinski_Space by Def9; ::_thesis: verum
end;
hence  the topology of T = the topology of Sierpinski_Space by A4, TARSKI:1; ::_thesis: verum
end;

theorem Th13: :: WAYBEL18:13
for I being non empty set holds  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  is prebasis of (product (I --> Sierpinski_Space))
proof
let I be non empty set ; ::_thesis:  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  is prebasis of (product (I --> Sierpinski_Space))
set IS = I --> Sierpinski_Space;
set pB =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  ;
set P = product_prebasis (I --> Sierpinski_Space);
A1: product_prebasis (I --> Sierpinski_Space) is prebasis of (product (I --> Sierpinski_Space)) by Def3;
then A2: product_prebasis (I --> Sierpinski_Space) c= the topology of (product (I --> Sierpinski_Space)) by TOPS_2:64;
  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  c= bool the carrier of (product (I --> Sierpinski_Space))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  or x in bool the carrier of (product (I --> Sierpinski_Space)) )
assume  x in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  ; ::_thesis: x in bool the carrier of (product (I --> Sierpinski_Space))
then consider i being Element of I such that
A3: x = product ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) ;
 product ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) c= product (Carrier (I --> Sierpinski_Space))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) or y in product (Carrier (I --> Sierpinski_Space)) )
assume  y in product ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) ; ::_thesis: y in product (Carrier (I --> Sierpinski_Space))
then consider g being Function such that
A4: y = g and
A5: dom g = dom ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) and
A6: for z being set st z in dom ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) holds
g . z in ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) . z by CARD_3:def_5;
A7: for z being set st z in dom (Carrier (I --> Sierpinski_Space)) holds
g . z in (Carrier (I --> Sierpinski_Space)) . z
proof
let z be set ; ::_thesis: ( z in dom (Carrier (I --> Sierpinski_Space)) implies g . z in (Carrier (I --> Sierpinski_Space)) . z )
assume A8: z in dom (Carrier (I --> Sierpinski_Space)) ; ::_thesis: g . z in (Carrier (I --> Sierpinski_Space)) . z
then A9: z in I ;
then consider R being 1-sorted  such that
A10: R = (I --> Sierpinski_Space) . z and
A11: (Carrier (I --> Sierpinski_Space)) . z = the carrier of R by PRALG_1:def_13;
A12: the carrier of R = the carrier of Sierpinski_Space by A9, A10, FUNCOP_1:7
.= {0,1} by Def9 ;
 z in dom ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) by A8, FUNCT_7:30;
then A13: g . z in ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) . z by A6;
percases ( z = i or z <> i ) ;
suppose z = i ; ::_thesis: g . z in (Carrier (I --> Sierpinski_Space)) . z
then  ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) . z = {1} by A8, FUNCT_7:31;
then  g . z = 1 by A13, TARSKI:def_1;
hence  g . z in (Carrier (I --> Sierpinski_Space)) . z by A11, A12, TARSKI:def_2; ::_thesis: verum
end;
suppose z <> i ; ::_thesis: g . z in (Carrier (I --> Sierpinski_Space)) . z
hence  g . z in (Carrier (I --> Sierpinski_Space)) . z by A13, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
 dom g = dom (Carrier (I --> Sierpinski_Space)) by A5, FUNCT_7:30;
hence  y in product (Carrier (I --> Sierpinski_Space)) by A4, A7, CARD_3:def_5; ::_thesis: verum
end;
then  x c= the carrier of (product (I --> Sierpinski_Space)) by A3, Def3;
hence  x in bool the carrier of (product (I --> Sierpinski_Space)) ; ::_thesis: verum
end;
then reconsider B =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  as Subset-Family of (product (I --> Sierpinski_Space)) ;
reconsider B = B as Subset-Family of (product (I --> Sierpinski_Space)) ;
A14: B c= product_prebasis (I --> Sierpinski_Space)
proof
 {1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in product_prebasis (I --> Sierpinski_Space) )
assume A15: x in B ; ::_thesis: x in product_prebasis (I --> Sierpinski_Space)
then consider i being Element of I such that
A16: x = product ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) ;
reconsider y = x as Subset of (product (Carrier (I --> Sierpinski_Space))) by A15, Def3;
 {1} in {{},{1},{0,1}} by ENUMSET1:def_1;
then  {1} in the topology of Sierpinski_Space by Def9;
then A17: V is open by PRE_TOPC:def_2;
 ( Sierpinski_Space = (I --> Sierpinski_Space) . i & y = product ((Carrier (I --> Sierpinski_Space)) +* (i,V)) ) by A16, FUNCOP_1:7;
hence  x in product_prebasis (I --> Sierpinski_Space) by A17, Def2; ::_thesis: verum
end;
reconsider P = product_prebasis (I --> Sierpinski_Space) as Subset-Family of (product (I --> Sierpinski_Space)) by Def3;
reconsider P = P as Subset-Family of (product (I --> Sierpinski_Space)) ;
 FinMeetCl P is Basis of (product (I --> Sierpinski_Space)) by A1, YELLOW_9:23;
then reconsider F = (FinMeetCl P) \ {{}} as Basis of (product (I --> Sierpinski_Space)) by Th2;
A18: F c= FinMeetCl B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in FinMeetCl B )
assume A19: x in F ; ::_thesis: x in FinMeetCl B
then reconsider y = x as Subset of (product (I --> Sierpinski_Space)) ;
 x in FinMeetCl P by A19, XBOOLE_0:def_5;
then consider Y1 being Subset-Family of (product (I --> Sierpinski_Space)) such that
A20: Y1 c= P and
A21: Y1 is finite and
A22: y = Intersect Y1 by CANTOR_1:def_3;
reconsider Y2 = Y1 /\ B as Subset-Family of (product (I --> Sierpinski_Space)) ;
A23: ( Y2 c= B & Y2 is finite ) by A21, FINSET_1:1, XBOOLE_1:17;
A24: the carrier of (product (I --> Sierpinski_Space)) = product (Carrier (I --> Sierpinski_Space)) by Def3;
A25: not x in {{}} by A19, XBOOLE_0:def_5;
A26: Intersect Y2 c= Intersect Y1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Intersect Y2 or z in Intersect Y1 )
assume A27: z in Intersect Y2 ; ::_thesis: z in Intersect Y1
then A28: z in product (Carrier (I --> Sierpinski_Space)) by A24;
 for Y being set st Y in Y1 holds
z in Y
proof
let Y be set ; ::_thesis: ( Y in Y1 implies z in Y )
assume A29: Y in Y1 ; ::_thesis: z in Y
then reconsider Y9 = Y as Subset of (product (Carrier (I --> Sierpinski_Space))) by Def3;
consider i being set , S being TopStruct , V being Subset of S such that
A30: i in I and
A31: V is open and
A32: S = (I --> Sierpinski_Space) . i and
A33: Y9 = product ((Carrier (I --> Sierpinski_Space)) +* (i,V)) by A20, A29, Def2;
reconsider V9 = V as Subset of Sierpinski_Space by A30, A32, FUNCOP_1:7;
 V in the topology of S by A31, PRE_TOPC:def_2;
then  V9 in the topology of Sierpinski_Space by A30, A32, FUNCOP_1:7;
then A34: V9 in {{},{1},{0,1}} by Def9;
A35: i in dom (Carrier (I --> Sierpinski_Space)) by A30, PARTFUN1:def_2;
A36: V9 <> {}
proof
 ( ((Carrier (I --> Sierpinski_Space)) +* (i,{})) . i = {} & i in dom ((Carrier (I --> Sierpinski_Space)) +* (i,{})) ) by A35, FUNCT_7:30, FUNCT_7:31;
then A37: {} in rng ((Carrier (I --> Sierpinski_Space)) +* (i,{})) by FUNCT_1:def_3;
assume  V9 = {} ; ::_thesis: contradiction
then  Y9 = {} by A33, A37, CARD_3:26;
then  y = {} by A22, A29, MSSUBFAM:3;
hence  contradiction by A25, TARSKI:def_1; ::_thesis: verum
end;
reconsider i9 = i as Element of I by A30;
A38: ex RR being 1-sorted st
( RR = (I --> Sierpinski_Space) . i & (Carrier (I --> Sierpinski_Space)) . i = the carrier of RR ) by A30, PRALG_1:def_13;
percases ( V9 = {1} or V9 = {0,1} ) by A34, A36, ENUMSET1:def_1;
suppose V9 = {1} ; ::_thesis: z in Y
then  Y9 = product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) by A33;
then  Y in B ;
then  Y in Y2 by A29, XBOOLE_0:def_4;
hence  z in Y by A27, SETFAM_1:43; ::_thesis: verum
end;
suppose V9 = {0,1} ; ::_thesis: z in Y
then V9 = the carrier of Sierpinski_Space by Def9
.= (Carrier (I --> Sierpinski_Space)) . i by A30, A38, FUNCOP_1:7 ;
hence  z in Y by A28, A33, FUNCT_7:35; ::_thesis: verum
end;
end;
end;
hence  z in Intersect Y1 by A27, SETFAM_1:43; ::_thesis: verum
end;
 Intersect Y1 c= Intersect Y2 by SETFAM_1:44, XBOOLE_1:17;
then  y = Intersect Y2 by A22, A26, XBOOLE_0:def_10;
hence  x in FinMeetCl B by A23, CANTOR_1:def_3; ::_thesis: verum
end;
  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  c= the topology of (product (I --> Sierpinski_Space)) by A14, A2, XBOOLE_1:1;
hence   {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum  }  is prebasis of (product (I --> Sierpinski_Space)) by A18, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum
end;

registration
let I be non empty set ;
let L be complete LATTICE;
cluster product (I --> L) ->  with_suprema complete ;
coherence
 ( product (I --> L) is with_suprema & product (I --> L) is complete )
proof
reconsider IB = I --> L as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I ;
 for i being Element of I holds IB . i is complete LATTICE by FUNCOP_1:7;
hence  ( product (I --> L) is with_suprema & product (I --> L) is complete ) by WAYBEL_3:31; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let X be lower-bounded algebraic LATTICE;
cluster product (I --> X) ->  algebraic ;
coherence
 product (I --> X) is algebraic
proof
set IB = I --> X;
 for i being Element of I holds (I --> X) . i is lower-bounded algebraic LATTICE by FUNCOP_1:7;
hence  product (I --> X) is algebraic by WAYBEL13:25; ::_thesis: verum
end;
end;

theorem Th14: :: WAYBEL18:14
for X being non empty set ex f being Function of (BoolePoset X),(product (X --> (BoolePoset 1))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
proof
let X be non empty set ; ::_thesis: ex f being Function of (BoolePoset X),(product (X --> (BoolePoset 1))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
set XB = X --> (BoolePoset 1);
deffunc H1( set ) ->  Element of K19(K20(X,{{},1})) = chi ($1,X);
consider f being Function such that
A1: dom f = bool X and
A2: for Y being set st Y in bool X holds
f . Y = H1(Y) from FUNCT_1:sch_3();
 LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def_2;
then A3: the carrier of (BoolePoset 1) = the carrier of (BooleLatt 1) by YELLOW_1:def_2
.= bool {{}} by CARD_1:49, LATTICE3:def_1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A4: rng f c= product (Carrier (X --> (BoolePoset 1)))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in product (Carrier (X --> (BoolePoset 1))) )
assume  y in rng f ; ::_thesis: y in product (Carrier (X --> (BoolePoset 1)))
then consider x being set  such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
A6: dom (chi (x,X)) = X by FUNCT_3:def_3
.= dom (Carrier (X --> (BoolePoset 1))) by PARTFUN1:def_2 ;
A7: for z being set st z in dom (Carrier (X --> (BoolePoset 1))) holds
(chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z
proof
let z be set ; ::_thesis: ( z in dom (Carrier (X --> (BoolePoset 1))) implies (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z )
assume  z in dom (Carrier (X --> (BoolePoset 1))) ; ::_thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z
then A8: z in X ;
then  ex R being 1-sorted st
( R = (X --> (BoolePoset 1)) . z & (Carrier (X --> (BoolePoset 1))) . z = the carrier of R ) by PRALG_1:def_13;
then A9: (Carrier (X --> (BoolePoset 1))) . z = {0,1} by A3, A8, FUNCOP_1:7;
percases ( z in x or not z in x ) ;
suppose z in x ; ::_thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z
then  (chi (x,X)) . z = 1 by A8, FUNCT_3:def_3;
hence  (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z by A9, TARSKI:def_2; ::_thesis: verum
end;
suppose not z in x ; ::_thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z
then  (chi (x,X)) . z = 0 by A8, FUNCT_3:def_3;
hence  (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z by A9, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
 chi (x,X) = y by A1, A2, A5;
hence  y in product (Carrier (X --> (BoolePoset 1))) by A6, A7, CARD_3:def_5; ::_thesis: verum
end;
 LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2;
then A10: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
A11: the carrier of (product (X --> (BoolePoset 1))) = product (Carrier (X --> (BoolePoset 1))) by YELLOW_1:def_4;
then reconsider f = f as Function of (BoolePoset X),(product (X --> (BoolePoset 1))) by A10, A1, A4, FUNCT_2:def_1, RELSET_1:4;
A12: for A, B being Element of (BoolePoset X) holds
( A <= B iff f . A <= f . B )
proof
let A, B be Element of (BoolePoset X); ::_thesis: ( A <= B iff f . A <= f . B )
A13: ( f . A = chi (A,X) & f . B = chi (B,X) ) by A10, A2;
hereby  ::_thesis: ( f . A <= f . B implies A <= B )
assume  A <= B ; ::_thesis: f . A <= f . B
then A14: A c= B by YELLOW_1:2;
 for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi ) )
assume A15: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take R = BoolePoset 1; ::_thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
percases ( i in A or not i in A ) ;
supposeA16: i in A ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
reconsider xi = 1, yi = 1 as Element of R by A3, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; ::_thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  xi = (chi (A,X)) . i by A15, A16, FUNCT_3:def_3; ::_thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus  yi = (chi (B,X)) . i by A14, A15, A16, FUNCT_3:def_3; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
supposeA17: not i in A ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi ) ::_thesis: verum
proof
percases ( i in B or not i in B ) ;
supposeA18: i in B ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
reconsider xi = 0 , yi = 1 as Element of R by A3, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; ::_thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  xi = (chi (A,X)) . i by A15, A17, FUNCT_3:def_3; ::_thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus  yi = (chi (B,X)) . i by A15, A18, FUNCT_3:def_3; ::_thesis: xi <= yi
 xi c= yi by XBOOLE_1:2;
hence  xi <= yi by YELLOW_1:2; ::_thesis: verum
end;
supposeA19: not i in B ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
reconsider xi = 0 , yi = 0 as Element of R by A3, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; ::_thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus  xi = (chi (A,X)) . i by A15, A17, FUNCT_3:def_3; ::_thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus  yi = (chi (B,X)) . i by A15, A19, FUNCT_3:def_3; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence  f . A <= f . B by A11, A13, YELLOW_1:def_4; ::_thesis: verum
end;
assume  f . A <= f . B ; ::_thesis: A <= B
then consider h1, h2 being Function such that
A20: h1 = f . A and
A21: h2 = f . B and
A22: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A11, YELLOW_1:def_4;
 A c= B
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in A or i in B )
assume A23: i in A ; ::_thesis: i in B
then consider R being RelStr , xi, yi being Element of R such that
A24: R = (X --> (BoolePoset 1)) . i and
A25: xi = h1 . i and
A26: yi = h2 . i and
A27: xi <= yi by A10, A22;
reconsider a = xi, b = yi as Element of (BoolePoset 1) by A10, A23, A24, FUNCOP_1:7;
A28: a <= b by A10, A23, A24, A27, FUNCOP_1:7;
A29: xi = (chi (A,X)) . i by A10, A2, A20, A25
.= 1 by A10, A23, FUNCT_3:def_3 ;
A30: yi <> 0
proof
assume  yi = 0 ; ::_thesis: contradiction
then  1 c= 0 by A29, A28, YELLOW_1:2;
hence  contradiction ; ::_thesis: verum
end;
A31: R = BoolePoset 1 by A10, A23, A24, FUNCOP_1:7;
(chi (B,X)) . i = h2 . i by A10, A2, A21
.= 1 by A3, A26, A31, A30, TARSKI:def_2 ;
hence  i in B by FUNCT_3:36; ::_thesis: verum
end;
hence  A <= B by YELLOW_1:2; ::_thesis: verum
end;
 product (Carrier (X --> (BoolePoset 1))) c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in product (Carrier (X --> (BoolePoset 1))) or z in rng f )
assume  z in product (Carrier (X --> (BoolePoset 1))) ; ::_thesis: z in rng f
then consider g being Function such that
A32: z = g and
A33: dom g = dom (Carrier (X --> (BoolePoset 1))) and
A34: for y being set st y in dom (Carrier (X --> (BoolePoset 1))) holds
g . y in (Carrier (X --> (BoolePoset 1))) . y by CARD_3:def_5;
set A = g " {1};
A35: g " {1} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in g " {1} or a in X )
assume  a in g " {1} ; ::_thesis: a in X
then  a in dom g by FUNCT_1:def_7;
hence  a in X by A33; ::_thesis: verum
end;
A36: dom (chi ((g " {1}),X)) = X by FUNCT_3:def_3
.= dom g by A33, PARTFUN1:def_2 ;
 for a being set st a in dom (chi ((g " {1}),X)) holds
(chi ((g " {1}),X)) . a = g . a
proof
let a be set ; ::_thesis: ( a in dom (chi ((g " {1}),X)) implies (chi ((g " {1}),X)) . a = g . a )
assume A37: a in dom (chi ((g " {1}),X)) ; ::_thesis: (chi ((g " {1}),X)) . a = g . a
then  a in X ;
then  a in dom (Carrier (X --> (BoolePoset 1))) by PARTFUN1:def_2;
then A38: g . a in (Carrier (X --> (BoolePoset 1))) . a by A34;
 ex R being 1-sorted st
( R = (X --> (BoolePoset 1)) . a & (Carrier (X --> (BoolePoset 1))) . a = the carrier of R ) by A37, PRALG_1:def_13;
then  (Carrier (X --> (BoolePoset 1))) . a = {0,1} by A3, A37, FUNCOP_1:7;
then A39: ( g . a = 0 or g . a = 1 ) by A38, TARSKI:def_2;
percases ( a in g " {1} or not a in g " {1} ) ;
suppose a in g " {1} ; ::_thesis: (chi ((g " {1}),X)) . a = g . a
then  ( (chi ((g " {1}),X)) . a = 1 & g . a in {1} ) by A37, FUNCT_1:def_7, FUNCT_3:def_3;
hence  (chi ((g " {1}),X)) . a = g . a by TARSKI:def_1; ::_thesis: verum
end;
supposeA40: not a in g " {1} ; ::_thesis: (chi ((g " {1}),X)) . a = g . a
 g . a <> 1
proof
assume  g . a = 1 ; ::_thesis: contradiction
then  g . a in {1} by TARSKI:def_1;
hence  contradiction by A36, A37, A40, FUNCT_1:def_7; ::_thesis: verum
end;
hence  (chi ((g " {1}),X)) . a = g . a by A37, A39, A40, FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
then z = chi ((g " {1}),X) by A32, A36, FUNCT_1:2
.= f . (g " {1}) by A2, A35 ;
hence  z in rng f by A1, A35, FUNCT_1:def_3; ::_thesis: verum
end;
then A41: rng f = the carrier of (product (X --> (BoolePoset 1))) by A11, XBOOLE_0:def_10;
take  f ; ::_thesis: ( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
 for A, B being Element of (BoolePoset X) st f . A = f . B holds
A = B
proof
let A, B be Element of (BoolePoset X); ::_thesis: ( f . A = f . B implies A = B )
assume A42: f . A = f . B ; ::_thesis: A = B
 ( f . A = chi (A,X) & f . B = chi (B,X) ) by A10, A2;
hence  A = B by A10, A42, FUNCT_3:38; ::_thesis: verum
end;
then  f is one-to-one by WAYBEL_1:def_1;
hence  f is isomorphic by A41, A12, WAYBEL_0:66; ::_thesis: for Y being Subset of X holds f . Y = chi (Y,X)
thus  for Y being Subset of X holds f . Y = chi (Y,X) by A2; ::_thesis: verum
end;

theorem Th15: :: WAYBEL18:15
for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the topology of T = the topology of (product (I --> Sierpinski_Space))
proof
let I be non empty set ; ::_thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the topology of T = the topology of (product (I --> Sierpinski_Space))
set IB = I --> (BoolePoset 1);
set IS = I --> Sierpinski_Space;
A1: the carrier of (product (I --> (BoolePoset 1))) = product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4;
 LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def_2;
then A2: the carrier of (BoolePoset 1) = the carrier of (BooleLatt 1) by YELLOW_1:def_2
.= bool {{}} by CARD_1:49, LATTICE3:def_1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A3: for i being set st i in dom (Carrier (I --> (BoolePoset 1))) holds
(Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier (I --> (BoolePoset 1))) implies (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i )
assume  i in dom (Carrier (I --> (BoolePoset 1))) ; ::_thesis: (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i
then A4: i in I ;
then consider R1 being 1-sorted  such that
A5: R1 = (I --> (BoolePoset 1)) . i and
A6: (Carrier (I --> (BoolePoset 1))) . i = the carrier of R1 by PRALG_1:def_13;
consider R2 being 1-sorted  such that
A7: R2 = (I --> Sierpinski_Space) . i and
A8: (Carrier (I --> Sierpinski_Space)) . i = the carrier of R2 by A4, PRALG_1:def_13;
the carrier of R1 = {0,1} by A2, A4, A5, FUNCOP_1:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A4, A7, FUNCOP_1:7 ;
hence  (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i by A6, A8; ::_thesis: verum
end;
reconsider P =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (ii,{1}))) where ii is Element of I : verum  }  as prebasis of (product (I --> Sierpinski_Space)) by Th13;
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); ::_thesis: the topology of T = the topology of (product (I --> Sierpinski_Space))
A9: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def_2
.= dom (Carrier (I --> Sierpinski_Space)) by PARTFUN1:def_2 ;
reconsider T9 = T as complete Scott TopLattice ;
A10: RelStr(# the carrier of T, the InternalRel of T #) = product (I --> (BoolePoset 1)) by YELLOW_9:def_4;
then  T9 is algebraic by WAYBEL_8:17;
then consider R being Basis of T9 such that
A11: R =  {  (uparrow yy) where yy is Element of T9 : yy in the carrier of (CompactSublatt T9)  }  by WAYBEL14:42;
A12: the carrier of T = product (Carrier (I --> (BoolePoset 1))) by A10, YELLOW_1:def_4
.= product (Carrier (I --> Sierpinski_Space)) by A9, A3, FUNCT_1:2
.= the carrier of (product (I --> Sierpinski_Space)) by Def3 ;
then reconsider P9 = P as Subset-Family of T ;
consider f being Function of (BoolePoset I),(product (I --> (BoolePoset 1))) such that
A13: f is isomorphic and
A14: for Y being Subset of I holds f . Y = chi (Y,I) by Th14;
A15: Carrier (I --> (BoolePoset 1)) = Carrier (I --> Sierpinski_Space) by A9, A3, FUNCT_1:2;
A16: FinMeetCl P c= R
proof
deffunc H1( set ) ->  set = product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in FinMeetCl P or X in R )
consider F being Function such that
A17: dom F = I and
A18: for e being set st e in I holds
F . e = H1(e) from FUNCT_1:sch_3();
assume A19: X in FinMeetCl P ; ::_thesis: X in R
then reconsider X9 = X as Subset of (product (I --> Sierpinski_Space)) ;
consider ZZ being Subset-Family of (product (I --> Sierpinski_Space)) such that
A20: ZZ c= P and
A21: ZZ is finite and
A22: X = Intersect ZZ by A19, CANTOR_1:def_3;
 P c= rng F
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in P or w in rng F )
assume  w in P ; ::_thesis: w in rng F
then consider e being Element of I such that
A23: w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) ;
 w = F . e by A18, A23;
hence  w in rng F by A17, FUNCT_1:def_3; ::_thesis: verum
end;
then  ZZ c= rng F by A20, XBOOLE_1:1;
then consider x9 being set  such that
A24: x9 c= dom F and
A25: x9 is finite and
A26: F .: x9 = ZZ by A21, ORDERS_1:85;
reconsider x9 = x9 as Subset of I by A17, A24;
reconsider x = x9 as Element of (BoolePoset I) by WAYBEL_8:26;
reconsider y = f . x as Element of (product (I --> (BoolePoset 1))) ;
set PP =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  ;
A27: ZZ c=  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in ZZ or w in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  )
assume  w in ZZ ; ::_thesis: w in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }
then consider e being set  such that
A28: e in dom F and
A29: e in x9 and
A30: w = F . e by A26, FUNCT_1:def_6;
reconsider e = e as Element of I by A17, A28;
 w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) by A18, A30;
hence  w in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  by A29; ::_thesis: verum
end;
  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  c= ZZ
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  or w in ZZ )
assume  w in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  ; ::_thesis: w in ZZ
then consider e being Element of I such that
A31: w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) and
A32: e in x9 ;
 w = F . e by A18, A31;
hence  w in ZZ by A17, A26, A32, FUNCT_1:def_6; ::_thesis: verum
end;
then A33: ZZ =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9  }  by A27, XBOOLE_0:def_10;
A34: uparrow y c= X9
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow y or z in X9 )
assume A35: z in uparrow y ; ::_thesis: z in X9
then reconsider z9 = z as Element of (product (I --> (BoolePoset 1))) ;
 y <= z9 by A35, WAYBEL_0:18;
then consider h1, h2 being Function such that
A36: h1 = y and
A37: h2 = z9 and
A38: for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A1, YELLOW_1:def_4;
 z in the carrier of (product (I --> (BoolePoset 1))) by A35;
then  z in product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4;
then A39: ex gg being Function st
( z = gg & dom gg = dom (Carrier (I --> (BoolePoset 1))) & ( for w being set st w in dom (Carrier (I --> (BoolePoset 1))) holds
gg . w in (Carrier (I --> (BoolePoset 1))) . w ) ) by CARD_3:def_5;
A40: h1 = chi (x,I) by A14, A36;
 for Z being set st Z in ZZ holds
z in Z
proof
let Z be set ; ::_thesis: ( Z in ZZ implies z in Z )
assume  Z in ZZ ; ::_thesis: z in Z
then consider j being Element of I such that
A41: Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) and
A42: j in x by A33;
consider RS being RelStr , xj, yj being Element of RS such that
A43: RS = (I --> (BoolePoset 1)) . j and
A44: xj = h1 . j and
A45: yj = h2 . j and
A46: xj <= yj by A38;
A47: RS = BoolePoset 1 by A43, FUNCOP_1:7;
A48: xj = 1 by A40, A42, A44, FUNCT_3:def_3;
A49: yj <> 0
proof
assume  yj = 0 ; ::_thesis: contradiction
then  1 c= 0 by A46, A48, A47, YELLOW_1:2;
hence  contradiction ; ::_thesis: verum
end;
reconsider b = yj as Element of (BoolePoset 1) by A43, FUNCOP_1:7;
A50: dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) = dom (Carrier (I --> Sierpinski_Space)) by FUNCT_7:30
.= I by PARTFUN1:def_2 ;
A51: b in the carrier of (BoolePoset 1) ;
A52: for w being set st w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
proof
let w be set ; ::_thesis: ( w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) implies h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w )
assume  w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then A53: w in dom (Carrier (I --> Sierpinski_Space)) by A50, PARTFUN1:def_2;
percases ( w = j or w <> j ) ;
suppose w = j ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then  ( ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = {1} & h2 . w = 1 ) by A2, A45, A51, A49, A53, FUNCT_7:31, TARSKI:def_2;
hence  h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by TARSKI:def_1; ::_thesis: verum
end;
suppose w <> j ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then  ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = (Carrier (I --> Sierpinski_Space)) . w by FUNCT_7:32;
hence  h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by A15, A39, A37, A53; ::_thesis: verum
end;
end;
end;
 dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) by A39, A37, A50, PARTFUN1:def_2;
hence  z in Z by A37, A41, A52, CARD_3:def_5; ::_thesis: verum
end;
hence  z in X9 by A10, A12, A22, A35, SETFAM_1:43; ::_thesis: verum
end;
A54: X9 c= uparrow y
proof
set h1 = chi (x,I);
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X9 or z in uparrow y )
assume A55: z in X9 ; ::_thesis: z in uparrow y
then reconsider z9 = z as Element of (product (I --> (BoolePoset 1))) by A10, A12;
 z in the carrier of (product (I --> (BoolePoset 1))) by A10, A12, A55;
then  z in product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4;
then consider h2 being Function such that
A56: z = h2 and
 dom h2 = dom (Carrier (I --> (BoolePoset 1))) and
A57: for w being set st w in dom (Carrier (I --> (BoolePoset 1))) holds
h2 . w in (Carrier (I --> (BoolePoset 1))) . w by CARD_3:def_5;
A58: for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) )
assume A59: i in I ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
then reconsider i9 = i as Element of I ;
 ex RB being 1-sorted st
( RB = (I --> (BoolePoset 1)) . i & (Carrier (I --> (BoolePoset 1))) . i = the carrier of RB ) by A59, PRALG_1:def_13;
then A60: (Carrier (I --> (BoolePoset 1))) . i = {0,1} by A2, A59, FUNCOP_1:7;
take RS = BoolePoset 1; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
A61: i in dom (Carrier (I --> (BoolePoset 1))) by A59, PARTFUN1:def_2;
then A62: h2 . i in (Carrier (I --> (BoolePoset 1))) . i by A57;
percases ( i in x or not i in x ) ;
supposeA63: i in x ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 1, yi = 1 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A59, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A63, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
A64: ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 = {1} by A9, A61, FUNCT_7:31;
 product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) in ZZ by A33, A63;
then  z in product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) by A22, A55, SETFAM_1:43;
then consider h29 being Function such that
A65: z = h29 and
 dom h29 = dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) and
A66: for w being set st w in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) holds
h29 . w in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . w by CARD_3:def_5;
 i9 in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) by A9, A61, FUNCT_7:30;
then  h29 . i9 in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 by A66;
hence  yi = h2 . i by A56, A65, A64, TARSKI:def_1; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
supposeA67: not i in x ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) ::_thesis: verum
proof
percases ( h2 . i = 0 or h2 . i = 1 ) by A60, A62, TARSKI:def_2;
supposeA68: h2 . i = 0 ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A59, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A59, A67, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
thus  yi = h2 . i by A68; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
supposeA69: h2 . i = 1 ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A59, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A59, A67, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
thus  yi = h2 . i by A69; ::_thesis: xi <= yi
 xi c= yi by XBOOLE_1:2;
hence  xi <= yi by YELLOW_1:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
 chi (x,I) = y by A14;
then  y <= z9 by A1, A56, A58, YELLOW_1:def_4;
hence  z in uparrow y by WAYBEL_0:18; ::_thesis: verum
end;
reconsider Y = y as Element of T9 by A10;
 x is compact by A25, WAYBEL_8:28;
then  y is compact by A13, WAYBEL13:28;
then  Y is compact by A10, WAYBEL_8:9;
then A70: Y in the carrier of (CompactSublatt T9) by WAYBEL_8:def_1;
uparrow Y = uparrow {Y} by WAYBEL_0:def_18
.= uparrow {y} by A10, WAYBEL_0:13
.= uparrow y by WAYBEL_0:def_18 ;
then  X = uparrow Y by A54, A34, XBOOLE_0:def_10;
hence  X in R by A11, A70; ::_thesis: verum
end;
A71: rng f = the carrier of (product (I --> (BoolePoset 1))) by A13, WAYBEL_0:66;
 R c= FinMeetCl P
proof
deffunc H1( Element of I) ->  set = product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in R or X in FinMeetCl P )
assume A72: X in R ; ::_thesis: X in FinMeetCl P
then consider Y being Element of T9 such that
A73: X = uparrow Y and
A74: Y in the carrier of (CompactSublatt T9) by A11;
reconsider X9 = X as Subset of (product (I --> Sierpinski_Space)) by A12, A72;
reconsider y = Y as Element of (product (I --> (BoolePoset 1))) by A10;
consider x being set  such that
A75: x in dom f and
A76: y = f . x by A71, FUNCT_1:def_3;
reconsider x = x as Element of (BoolePoset I) by A75;
 Y is compact by A74, WAYBEL_8:def_1;
then  y is compact by A10, WAYBEL_8:9;
then  x is compact by A13, A76, WAYBEL13:28;
then A77: x is finite by WAYBEL_8:28;
A78:  {  H1(jj) where jj is Element of I : jj in x  }  is finite from FRAENKEL:sch_21(A77);
set ZZ =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x  }  ;
reconsider x9 = x as Subset of I by WAYBEL_8:26;
A79:  {  (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x  }  c= P
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x  }  or z in P )
assume  z in  {  (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x  }  ; ::_thesis: z in P
then  ex j being Element of I st
( z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) & j in x9 ) ;
hence  z in P ; ::_thesis: verum
end;
then reconsider ZZ =  {  (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x  }  as Subset-Family of (product (I --> Sierpinski_Space)) by XBOOLE_1:1;
A80: uparrow Y = uparrow {Y} by WAYBEL_0:def_18
.= uparrow {y} by A10, WAYBEL_0:13
.= uparrow y by WAYBEL_0:def_18 ;
A81: Intersect ZZ c= X9
proof
set h1 = chi (x,I);
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Intersect ZZ or z in X9 )
assume A82: z in Intersect ZZ ; ::_thesis: z in X9
then reconsider z9 = z as Element of (product (I --> (BoolePoset 1))) by A10, A12;
 z in the carrier of (product (I --> (BoolePoset 1))) by A10, A12, A82;
then  z in product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4;
then consider h2 being Function such that
A83: z = h2 and
 dom h2 = dom (Carrier (I --> (BoolePoset 1))) and
A84: for w being set st w in dom (Carrier (I --> (BoolePoset 1))) holds
h2 . w in (Carrier (I --> (BoolePoset 1))) . w by CARD_3:def_5;
A85: for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) )
assume A86: i in I ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
then reconsider i9 = i as Element of I ;
 ex RB being 1-sorted st
( RB = (I --> (BoolePoset 1)) . i & (Carrier (I --> (BoolePoset 1))) . i = the carrier of RB ) by A86, PRALG_1:def_13;
then A87: (Carrier (I --> (BoolePoset 1))) . i = {0,1} by A2, A86, FUNCOP_1:7;
take RS = BoolePoset 1; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
A88: i in dom (Carrier (I --> (BoolePoset 1))) by A86, PARTFUN1:def_2;
then A89: h2 . i in (Carrier (I --> (BoolePoset 1))) . i by A84;
percases ( i in x or not i in x ) ;
supposeA90: i in x ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 1, yi = 1 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A86, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A86, A90, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
A91: ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 = {1} by A9, A88, FUNCT_7:31;
 product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) in ZZ by A90;
then  z in product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) by A82, SETFAM_1:43;
then consider h29 being Function such that
A92: z = h29 and
 dom h29 = dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) and
A93: for w being set st w in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) holds
h29 . w in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . w by CARD_3:def_5;
 i9 in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) by A9, A88, FUNCT_7:30;
then  h29 . i9 in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 by A93;
hence  yi = h2 . i by A83, A92, A91, TARSKI:def_1; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
supposeA94: not i in x ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) ::_thesis: verum
proof
percases ( h2 . i = 0 or h2 . i = 1 ) by A87, A89, TARSKI:def_2;
supposeA95: h2 . i = 0 ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A86, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A86, A94, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
thus  yi = h2 . i by A95; ::_thesis: xi <= yi
thus  xi <= yi ; ::_thesis: verum
end;
supposeA96: h2 . i = 1 ; ::_thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def_2;
take  xi ; ::_thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
take  yi ; ::_thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  RS = (I --> (BoolePoset 1)) . i by A86, FUNCOP_1:7; ::_thesis: ( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
thus  xi = (chi (x,I)) . i by A86, A94, FUNCT_3:def_3; ::_thesis: ( yi = h2 . i & xi <= yi )
thus  yi = h2 . i by A96; ::_thesis: xi <= yi
 xi c= yi by XBOOLE_1:2;
hence  xi <= yi by YELLOW_1:2; ::_thesis: verum
end;
end;
end;
end;
end;
end;
chi (x,I) = f . x9 by A14
.= y by A76 ;
then  y <= z9 by A1, A83, A85, YELLOW_1:def_4;
hence  z in X9 by A73, A80, WAYBEL_0:18; ::_thesis: verum
end;
 X9 c= Intersect ZZ
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X9 or z in Intersect ZZ )
assume A97: z in X9 ; ::_thesis: z in Intersect ZZ
then reconsider z9 = z as Element of (product (I --> (BoolePoset 1))) by A10, A12;
 y <= z9 by A73, A80, A97, WAYBEL_0:18;
then consider h1, h2 being Function such that
A98: h1 = y and
A99: h2 = z9 and
A100: for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A1, YELLOW_1:def_4;
 z in the carrier of (product (I --> (BoolePoset 1))) by A10, A12, A97;
then  z in product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4;
then A101: ex gg being Function st
( z = gg & dom gg = dom (Carrier (I --> (BoolePoset 1))) & ( for w being set st w in dom (Carrier (I --> (BoolePoset 1))) holds
gg . w in (Carrier (I --> (BoolePoset 1))) . w ) ) by CARD_3:def_5;
A102: h1 = f . x9 by A76, A98
.= chi (x,I) by A14 ;
 for Z being set st Z in ZZ holds
z in Z
proof
let Z be set ; ::_thesis: ( Z in ZZ implies z in Z )
assume  Z in ZZ ; ::_thesis: z in Z
then consider j being Element of I such that
A103: Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) and
A104: j in x ;
consider RS being RelStr , xj, yj being Element of RS such that
A105: RS = (I --> (BoolePoset 1)) . j and
A106: xj = h1 . j and
A107: yj = h2 . j and
A108: xj <= yj by A100;
reconsider a = xj, b = yj as Element of (BoolePoset 1) by A105, FUNCOP_1:7;
A109: a <= b by A105, A108, FUNCOP_1:7;
A110: xj = 1 by A102, A104, A106, FUNCT_3:def_3;
A111: yj <> 0
proof
assume  yj = 0 ; ::_thesis: contradiction
then  1 c= 0 by A110, A109, YELLOW_1:2;
hence  contradiction ; ::_thesis: verum
end;
A112: dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) = dom (Carrier (I --> Sierpinski_Space)) by FUNCT_7:30
.= I by PARTFUN1:def_2 ;
A113: b in the carrier of (BoolePoset 1) ;
A114: for w being set st w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
proof
let w be set ; ::_thesis: ( w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) implies h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w )
assume  w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then A115: w in dom (Carrier (I --> Sierpinski_Space)) by A112, PARTFUN1:def_2;
percases ( w = j or w <> j ) ;
suppose w = j ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then  ( ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = {1} & h2 . w = 1 ) by A2, A107, A113, A111, A115, FUNCT_7:31, TARSKI:def_2;
hence  h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by TARSKI:def_1; ::_thesis: verum
end;
suppose w <> j ; ::_thesis: h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
then  ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = (Carrier (I --> Sierpinski_Space)) . w by FUNCT_7:32;
hence  h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by A15, A101, A99, A115; ::_thesis: verum
end;
end;
end;
 dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) by A101, A99, A112, PARTFUN1:def_2;
hence  z in Z by A99, A103, A114, CARD_3:def_5; ::_thesis: verum
end;
hence  z in Intersect ZZ by A97, SETFAM_1:43; ::_thesis: verum
end;
then  X9 = Intersect ZZ by A81, XBOOLE_0:def_10;
hence  X in FinMeetCl P by A79, A78, CANTOR_1:def_3; ::_thesis: verum
end;
then  R = FinMeetCl P by A16, XBOOLE_0:def_10;
then  P9 is prebasis of T by A12, YELLOW_9:23;
hence  the topology of T = the topology of (product (I --> Sierpinski_Space)) by A12, YELLOW_9:26; ::_thesis: verum
end;

theorem Th16: :: WAYBEL18:16
for T, S being non empty TopSpace st the carrier of T = the carrier of S & the topology of T = the topology of S & T is injective holds
S is injective
proof
let T, S be non empty TopSpace; ::_thesis: ( the carrier of T = the carrier of S & the topology of T = the topology of S & T is injective implies S is injective )
assume that
A1: the carrier of T = the carrier of S and
A2: the topology of T = the topology of S and
A3: T is injective ; ::_thesis: S is injective
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for f being Function of X,S st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
let f be Function of X,S; ::_thesis: ( f is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f ) )
reconsider f9 = f as Function of X,T by A1;
A4: [#] S <> {} ;
assume A5: f is continuous ; ::_thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
A6: for P being Subset of T st P is open holds
f9 " P is open
proof
let P be Subset of T; ::_thesis: ( P is open implies f9 " P is open )
reconsider P9 = P as Subset of S by A1;
assume  P is open ; ::_thesis: f9 " P is open
then  P9 in the topology of S by A2, PRE_TOPC:def_2;
then  P9 is open by PRE_TOPC:def_2;
hence  f9 " P is open by A4, A5, TOPS_2:43; ::_thesis: verum
end;
let Y be non empty TopSpace; ::_thesis: ( X is SubSpace of Y implies ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f ) )
assume A7: X is SubSpace of Y ; ::_thesis: ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
A8: [#] T <> {} ;
then  f9 is continuous by A6, TOPS_2:43;
then consider h being Function of Y,T such that
A9: h is continuous and
A10: h | the carrier of X = f9 by A3, A7, Def5;
reconsider g = h as Function of Y,S by A1;
take  g ; ::_thesis: ( g is continuous & g | the carrier of X = f )
 for P being Subset of S st P is open holds
g " P is open
proof
let P be Subset of S; ::_thesis: ( P is open implies g " P is open )
reconsider P9 = P as Subset of T by A1;
assume  P is open ; ::_thesis: g " P is open
then  P9 in the topology of T by A2, PRE_TOPC:def_2;
then  P9 is open by PRE_TOPC:def_2;
hence  g " P is open by A8, A9, TOPS_2:43; ::_thesis: verum
end;
hence  g is continuous by A4, TOPS_2:43; ::_thesis: g | the carrier of X = f
thus  g | the carrier of X = f by A10; ::_thesis: verum
end;

theorem :: WAYBEL18:17
for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds T is injective
proof
let I be non empty set ; ::_thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds T is injective
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); ::_thesis: T is injective
set IB = I --> (BoolePoset 1);
set IS = I --> Sierpinski_Space;
A1: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def_2
.= dom (Carrier (I --> Sierpinski_Space)) by PARTFUN1:def_2 ;
A2: the topology of T = the topology of (product (I --> Sierpinski_Space)) by Th15;
 LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def_2;
then A3: the carrier of (BoolePoset 1) = the carrier of (BooleLatt 1) by YELLOW_1:def_2
.= bool {{}} by CARD_1:49, LATTICE3:def_1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A4: for i being set st i in dom (Carrier (I --> (BoolePoset 1))) holds
(Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier (I --> (BoolePoset 1))) implies (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i )
assume  i in dom (Carrier (I --> (BoolePoset 1))) ; ::_thesis: (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i
then A5: i in I ;
then consider R1 being 1-sorted  such that
A6: R1 = (I --> (BoolePoset 1)) . i and
A7: (Carrier (I --> (BoolePoset 1))) . i = the carrier of R1 by PRALG_1:def_13;
consider R2 being 1-sorted  such that
A8: R2 = (I --> Sierpinski_Space) . i and
A9: (Carrier (I --> Sierpinski_Space)) . i = the carrier of R2 by A5, PRALG_1:def_13;
the carrier of R1 = {0,1} by A3, A5, A6, FUNCOP_1:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A5, A8, FUNCOP_1:7 ;
hence  (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space)) . i by A7, A9; ::_thesis: verum
end;
 for i being Element of I holds (I --> Sierpinski_Space) . i is injective by FUNCOP_1:7;
then A10: product (I --> Sierpinski_Space) is injective by Th7;
 RelStr(# the carrier of T, the InternalRel of T #) = product (I --> (BoolePoset 1)) by YELLOW_9:def_4;
then  the carrier of T = product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4
.= product (Carrier (I --> Sierpinski_Space)) by A1, A4, FUNCT_1:2
.= the carrier of (product (I --> Sierpinski_Space)) by Def3 ;
hence  T is injective by A2, A10, Th16; ::_thesis: verum
end;

theorem Th18: :: WAYBEL18:18
for T being T_0-TopSpace ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
proof
let T be T_0-TopSpace; ::_thesis: ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
take M = the carrier of (InclPoset the topology of T); ::_thesis: ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
set J = M --> Sierpinski_Space;
reconsider PP =  {  (product ((Carrier (M --> Sierpinski_Space)) +* (m,{1}))) where m is Element of M : verum  }  as prebasis of (product (M --> Sierpinski_Space)) by Th13;
deffunc H1( set ) ->  Element of K19(K20( the topology of T,{{},1})) = chi ( {  u where u is Subset of T : ( $1 in u & u is open )  }  , the topology of T);
consider f being Function such that
A1: dom f = the carrier of T and
A2: for x being set st x in the carrier of T holds
f . x = H1(x) from FUNCT_1:sch_3();
 rng f c= the carrier of (product (M --> Sierpinski_Space))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of (product (M --> Sierpinski_Space)) )
assume  y in rng f ; ::_thesis: y in the carrier of (product (M --> Sierpinski_Space))
then consider x being set  such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
set ch = chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T);
A4: dom (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) = the topology of T by FUNCT_3:def_3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def_2 ;
A5: for z being set st z in dom (Carrier (M --> Sierpinski_Space)) holds
(chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z
proof
let z be set ; ::_thesis: ( z in dom (Carrier (M --> Sierpinski_Space)) implies (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z )
assume  z in dom (Carrier (M --> Sierpinski_Space)) ; ::_thesis: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z
then A6: z in M ;
then  z in the topology of T by YELLOW_1:1;
then  z in dom (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) by FUNCT_3:def_3;
then A7: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . z in rng (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) by FUNCT_1:def_3;
 ex R being 1-sorted st
( R = (M --> Sierpinski_Space) . z & (Carrier (M --> Sierpinski_Space)) . z = the carrier of R ) by A6, PRALG_1:def_13;
then (Carrier (M --> Sierpinski_Space)) . z = the carrier of Sierpinski_Space by A6, FUNCOP_1:7
.= {0,1} by Def9 ;
hence  (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . z in (Carrier (M --> Sierpinski_Space)) . z by A7; ::_thesis: verum
end;
 y = chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T) by A1, A2, A3;
then  y in product (Carrier (M --> Sierpinski_Space)) by A4, A5, CARD_3:def_5;
hence  y in the carrier of (product (M --> Sierpinski_Space)) by Def3; ::_thesis: verum
end;
then reconsider f = f as Function of T,(product (M --> Sierpinski_Space)) by A1, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: corestr f is being_homeomorphism
A8: rng (corestr f) = [#] (Image f) by FUNCT_2:def_3;
 for A being Subset of (product (M --> Sierpinski_Space)) st A in PP holds
f " A is open
proof
 {1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let A be Subset of (product (M --> Sierpinski_Space)); ::_thesis: ( A in PP implies f " A is open )
reconsider a = A as Subset of (product (Carrier (M --> Sierpinski_Space))) by Def3;
assume  A in PP ; ::_thesis: f " A is open
then consider i being Element of M such that
A9: a = product ((Carrier (M --> Sierpinski_Space)) +* (i,{1})) ;
A10: i in M ;
then A11: i in the topology of T by YELLOW_1:1;
then reconsider i9 = i as Subset of T ;
A12: i in dom (Carrier (M --> Sierpinski_Space)) by A10, PARTFUN1:def_2;
A13: i c= f " A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in i or z in f " A )
assume A14: z in i ; ::_thesis: z in f " A
set W =  {  u where u is Subset of T : ( z in u & u is open )  }  ;
 i9 is open by A11, PRE_TOPC:def_2;
then A15: i in  {  u where u is Subset of T : ( z in u & u is open )  }  by A14;
A16: for w being set st w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
(chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
proof
let w be set ; ::_thesis: ( w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) implies (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w )
assume  w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) ; ::_thesis: (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
then  w in dom (Carrier (M --> Sierpinski_Space)) by FUNCT_7:30;
then A17: w in M ;
then  w in the topology of T by YELLOW_1:1;
then A18: w in dom (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) by FUNCT_3:def_3;
percases ( w = i or w <> i ) ;
suppose w = i ; ::_thesis: (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
then  ( ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w = {1} & (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w = 1 ) by A11, A12, A15, FUNCT_3:def_3, FUNCT_7:31;
hence  (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by TARSKI:def_1; ::_thesis: verum
end;
supposeA19: w <> i ; ::_thesis: (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
A20: (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in rng (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) by A18, FUNCT_1:def_3;
 ex r being 1-sorted st
( r = (M --> Sierpinski_Space) . w & (Carrier (M --> Sierpinski_Space)) . w = the carrier of r ) by A17, PRALG_1:def_13;
then A21: (Carrier (M --> Sierpinski_Space)) . w = the carrier of Sierpinski_Space by A17, FUNCOP_1:7
.= {0,1} by Def9 ;
 ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w = (Carrier (M --> Sierpinski_Space)) . w by A19, FUNCT_7:32;
hence  (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by A21, A20; ::_thesis: verum
end;
end;
end;
A22: dom (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) = the topology of T by FUNCT_3:def_3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def_2
.= dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) by FUNCT_7:30 ;
A23: z in i9 by A14;
then  f . z = chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T) by A2;
then  f . z in A by A9, A22, A16, CARD_3:def_5;
hence  z in f " A by A1, A23, FUNCT_1:def_7; ::_thesis: verum
end;
A24: ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i = {1} by A12, FUNCT_7:31;
 f " A c= i
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f " A or z in i )
set W =  {  u where u is Subset of T : ( z in u & u is open )  }  ;
assume  z in f " A ; ::_thesis: z in i
then  ( f . z in a & f . z = chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T) ) by A2, FUNCT_1:def_7;
then consider g being Function such that
A25: chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T) = g and
 dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) and
A26: for w being set st w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
g . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w by A9, CARD_3:def_5;
 i in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) by A12, FUNCT_7:30;
then  g . i in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i by A26;
then  (chi ( {  u where u is Subset of T : ( z in u & u is open )  }  , the topology of T)) . i = 1 by A24, A25, TARSKI:def_1;
then  i in  {  u where u is Subset of T : ( z in u & u is open )  }  by FUNCT_3:36;
then  ex uu being Subset of T st
( i = uu & z in uu & uu is open ) ;
hence  z in i ; ::_thesis: verum
end;
then  f " A = i by A13, XBOOLE_0:def_10;
hence  f " A is open by A11, PRE_TOPC:def_2; ::_thesis: verum
end;
then  f is continuous by YELLOW_9:36;
then A27: ( dom (corestr f) = [#] T & corestr f is continuous ) by Th10, FUNCT_2:def_1;
A28: corestr f is one-to-one
proof
let x, y be Element of T; :: according to WAYBEL_1:def_1 ::_thesis: ( not (corestr f) . x = (corestr f) . y or x = y )
set U1 =  {  u where u is Subset of T : ( x in u & u is open )  }  ;
set U2 =  {  u where u is Subset of T : ( y in u & u is open )  }  ;
assume A29: (corestr f) . x = (corestr f) . y ; ::_thesis: x = y
thus  x = y ::_thesis: verum
proof
A30: ( f . x = chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T) & f . y = chi ( {  u where u is Subset of T : ( y in u & u is open )  }  , the topology of T) ) by A2;
assume  not x = y ; ::_thesis: contradiction
then consider V being Subset of T such that
A31: V is open and
A32: ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by T_0TOPSP:def_7;
A33: V in the topology of T by A31, PRE_TOPC:def_2;
percases ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by A32;
supposeA34: ( x in V & not y in V ) ; ::_thesis: contradiction
reconsider v = V as Subset of T ;
A35: not v in  {  u where u is Subset of T : ( y in u & u is open )  }
proof
assume  v in  {  u where u is Subset of T : ( y in u & u is open )  }  ; ::_thesis: contradiction
then  ex u being Subset of T st
( u = v & y in u & u is open ) ;
hence  contradiction by A34; ::_thesis: verum
end;
 v in  {  u where u is Subset of T : ( x in u & u is open )  }  by A31, A34;
then  (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . v = 1 by A33, FUNCT_3:def_3;
hence  contradiction by A29, A30, A33, A35, FUNCT_3:def_3; ::_thesis: verum
end;
supposeA36: ( y in V & not x in V ) ; ::_thesis: contradiction
reconsider v = V as Subset of T ;
A37: not v in  {  u where u is Subset of T : ( x in u & u is open )  }
proof
assume  v in  {  u where u is Subset of T : ( x in u & u is open )  }  ; ::_thesis: contradiction
then  ex u being Subset of T st
( u = v & x in u & u is open ) ;
hence  contradiction by A36; ::_thesis: verum
end;
 v in  {  u where u is Subset of T : ( y in u & u is open )  }  by A31, A36;
then  (chi ( {  u where u is Subset of T : ( y in u & u is open )  }  , the topology of T)) . v = 1 by A33, FUNCT_3:def_3;
hence  contradiction by A29, A30, A33, A37, FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
end;
A38: for V being Subset of T st V is open holds
f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
proof
let V be Subset of T; ::_thesis: ( V is open implies f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )
assume A39: V is open ; ::_thesis: f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) c= f .: V
let y be set ; ::_thesis: ( y in f .: V implies y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )
assume  y in f .: V ; ::_thesis: y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
then consider x being set  such that
A40: x in dom f and
A41: x in V and
A42: y = f . x by FUNCT_1:def_6;
 y in rng f by A40, A42, FUNCT_1:def_3;
then A43: y in the carrier of (Image f) by Th9;
set Q =  {  u where u is Subset of T : ( x in u & u is open )  }  ;
A44: V in  {  u where u is Subset of T : ( x in u & u is open )  }  by A39, A41;
A45: for W being set st W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
(chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
proof
let W be set ; ::_thesis: ( W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) implies (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W )
assume  W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) ; ::_thesis: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
then A46: W in dom (Carrier (M --> Sierpinski_Space)) by FUNCT_7:30;
then A47: W in M ;
then A48: W in the topology of T by YELLOW_1:1;
then A49: W in dom (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) by FUNCT_3:def_3;
percases ( W = V or W <> V ) ;
suppose W = V ; ::_thesis: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
then  ( ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W = {1} & (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W = 1 ) by A44, A46, A48, FUNCT_3:def_3, FUNCT_7:31;
hence  (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by TARSKI:def_1; ::_thesis: verum
end;
supposeA50: W <> V ; ::_thesis: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
A51: (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in rng (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) by A49, FUNCT_1:def_3;
 ex r being 1-sorted st
( r = (M --> Sierpinski_Space) . W & (Carrier (M --> Sierpinski_Space)) . W = the carrier of r ) by A47, PRALG_1:def_13;
then A52: (Carrier (M --> Sierpinski_Space)) . W = the carrier of Sierpinski_Space by A47, FUNCOP_1:7
.= {0,1} by Def9 ;
 ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W = (Carrier (M --> Sierpinski_Space)) . W by A50, FUNCT_7:32;
hence  (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by A52, A51; ::_thesis: verum
end;
end;
end;
A53: dom (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) = the topology of T by FUNCT_3:def_3
.= M by YELLOW_1:1
.= dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def_2
.= dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by FUNCT_7:30 ;
 y = chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T) by A2, A40, A42;
then  y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by A53, A45, CARD_3:def_5;
hence  y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) by A43, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) or y in f .: V )
assume A54: y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) ; ::_thesis: y in f .: V
then  y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by XBOOLE_0:def_4;
then consider g being Function such that
A55: y = g and
 dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) and
A56: for W being set st W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
g . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W by CARD_3:def_5;
 rng f = the carrier of (Image f) by Th9;
then  y in rng f by A54, XBOOLE_0:def_4;
then consider x being set  such that
A57: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
 V in the topology of T by A39, PRE_TOPC:def_2;
then  V in M by YELLOW_1:1;
then A58: V in dom (Carrier (M --> Sierpinski_Space)) by PARTFUN1:def_2;
then  V in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) by FUNCT_7:30;
then  g . V in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . V by A56;
then A59: g . V in {1} by A58, FUNCT_7:31;
set Q =  {  u where u is Subset of T : ( x in u & u is open )  }  ;
 y = chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T) by A2, A57;
then  (chi ( {  u where u is Subset of T : ( x in u & u is open )  }  , the topology of T)) . V = 1 by A55, A59, TARSKI:def_1;
then  V in  {  u where u is Subset of T : ( x in u & u is open )  }  by FUNCT_3:36;
then  ex u being Subset of T st
( u = V & x in u & u is open ) ;
hence  y in f .: V by A57, FUNCT_1:def_6; ::_thesis: verum
end;
A60: for V being Subset of T st V is open holds
((corestr f) ") " V is open
proof
let V be Subset of T; ::_thesis: ( V is open implies ((corestr f) ") " V is open )
A61: PP c= the topology of (product (M --> Sierpinski_Space)) by TOPS_2:64;
assume A62: V is open ; ::_thesis: ((corestr f) ") " V is open
then  V in the topology of T by PRE_TOPC:def_2;
then reconsider W = V as Element of M by YELLOW_1:1;
A63: product ((Carrier (M --> Sierpinski_Space)) +* (W,{1})) in PP ;
then reconsider Q = product ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) as Subset of (product (M --> Sierpinski_Space)) ;
 (corestr f) .: V = Q /\ ([#] (Image f)) by A38, A62;
then  (corestr f) .: V in the topology of (Image f) by A63, A61, PRE_TOPC:def_4;
then  (corestr f) .: V is open by PRE_TOPC:def_2;
hence  ((corestr f) ") " V is open by A8, A28, TOPS_2:54; ::_thesis: verum
end;
 [#] T <> {} ;
then  (corestr f) " is continuous by A60, TOPS_2:43;
hence  corestr f is being_homeomorphism by A8, A28, A27, TOPS_2:def_5; ::_thesis: verum
end;

theorem :: WAYBEL18:19
for T being T_0-TopSpace st T is injective holds
ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space)
proof
let T be T_0-TopSpace; ::_thesis: ( T is injective implies ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space) )
assume A1: T is injective ; ::_thesis: ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space)
 ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism by Th18;
hence  ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space) by A1, Th11; ::_thesis: verum
end;