waybel18.miz



    begin

    theorem :: WAYBEL18:1

    

     Th1: for X be set, A,B be Subset-Family of X st B = (A \ { {} }) or A = (B \/ { {} }) holds ( UniCl A) = ( UniCl B)

    proof

      let X be set;

      let A,B be Subset-Family of X;

      assume

       A1: B = (A \ { {} }) or A = (B \/ { {} });

      

       A2: ( UniCl A) c= ( UniCl B)

      proof

        let x be object;

        assume x in ( UniCl A);

        then

        consider Y be 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 object;

          assume

           A6: w in (Y \ { {} });

          per cases by A1;

            suppose

             A7: B = (A \ { {} });

            w in Y & not w in { {} } by A6, XBOOLE_0:def 5;

            hence thesis by A3, A7, XBOOLE_0:def 5;

          end;

            suppose

             A8: A = (B \/ { {} });

            w in Y & not w in { {} } by A6, XBOOLE_0:def 5;

            hence thesis by A3, A8, XBOOLE_0:def 3;

          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 thesis by A5, CANTOR_1:def 1;

      end;

      ( UniCl B) c= ( UniCl A) by A1, CANTOR_1: 9, XBOOLE_1: 7, XBOOLE_1: 36;

      hence thesis by A2;

    end;

    theorem :: WAYBEL18:2

    

     Th2: for T be TopSpace, K be Subset-Family of T holds K is Basis of T iff (K \ { {} }) is Basis of T

    proof

      let T be TopSpace, K be Subset-Family 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

        assume

         A3: 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;

        hence (K \ { {} }) is Basis of T by A4, CANTOR_1:def 2, TOPS_2: 64;

      end;

      assume

       A5: (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 object;

        assume

         A8: x in K;

        per cases ;

          suppose x = {} ;

          hence thesis by PRE_TOPC: 1;

        end;

          suppose x <> {} ;

          then not x in { {} } by TARSKI:def 1;

          then x in K9 by A8, XBOOLE_0:def 5;

          hence thesis by A6;

        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;

      hence thesis by A7, CANTOR_1:def 2, TOPS_2: 64;

    end;

    definition

      let F be Relation;

      :: WAYBEL18:def1

      attr F is TopStruct-yielding means

      : Def1: for x be object st x in ( rng F) holds x is TopStruct;

    end

    registration

      cluster TopStruct-yielding -> 1-sorted-yielding for Function;

      coherence

      proof

        let F be Function such that

         A1: F is TopStruct-yielding;

        let x be object;

        assume x in ( dom F);

        then (F . x) in ( rng F) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

    end

    registration

      let I be set;

      cluster TopStruct-yielding for ManySortedSet of I;

      existence

      proof

        take f = (I --> the TopSpace);

        let v be object;

        assume v in ( rng f);

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be set;

      cluster TopStruct-yielding non-Empty for ManySortedSet of I;

      existence

      proof

        set R = the non empty TopSpace;

        take J = (I --> R);

        thus J is TopStruct-yielding

        proof

          let x be object;

          assume x in ( rng J);

          hence thesis by TARSKI:def 1;

        end;

        thus J is non-Empty

        proof

          let S be 1-sorted;

          assume S in ( rng J);

          hence thesis by TARSKI:def 1;

        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

      func A . j -> TopStruct ;

      coherence

      proof

        ( dom A) = J by PARTFUN1:def 2;

        then (A . j) in ( rng A) by FUNCT_1:def 3;

        hence thesis by Def1;

      end;

    end

    definition

      let I be set;

      let J be TopStruct-yielding ManySortedSet of I;

      :: WAYBEL18:def2

      func product_prebasis J -> Subset-Family of ( product ( Carrier J)) means

      : Def2: for x be Subset of ( product ( Carrier J)) holds x in it iff ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & x = ( product (( Carrier J) +* (i,V)));

      existence

      proof

        defpred P[ Subset of ( product ( Carrier J))] means ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & $1 = ( product (( Carrier J) +* (i,V)));

        thus ex F be Subset-Family of ( product ( Carrier J)) st for x be Subset of ( product ( Carrier J)) holds x in F iff P[x] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let P1,P2 be Subset-Family of ( product ( Carrier J)) such that

         A1: for x be Subset of ( product ( Carrier J)) holds x in P1 iff ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & x = ( product (( Carrier J) +* (i,V))) and

         A2: for x be Subset of ( product ( Carrier J)) holds x in P2 iff ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & x = ( product (( Carrier J) +* (i,V)));

        

         A3: P2 c= P1

        proof

          let x be object;

          assume

           A4: x in P2;

          then

          reconsider x9 = x as Subset of ( product ( Carrier J));

          ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & x9 = ( product (( Carrier J) +* (i,V))) by A2, A4;

          hence thesis by A1;

        end;

        P1 c= P2

        proof

          let x be object;

          assume

           A5: x in P1;

          then

          reconsider x9 = x as Subset of ( product ( Carrier J));

          ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J . i) & x9 = ( product (( Carrier J) +* (i,V))) by A1, A5;

          hence thesis by A2;

        end;

        hence thesis by A3;

      end;

    end

    theorem :: WAYBEL18:3

    

     Th3: for X be set, A be Subset-Family of X holds TopStruct (# X, ( UniCl ( FinMeetCl A)) #) is TopSpace-like

    proof

      let X be set;

      let A be Subset-Family of X;

      per cases ;

        suppose

         A1: X = {} ;

        set T = TopStruct (# X, ( UniCl ( FinMeetCl A)) #);

        the carrier of T in ( FinMeetCl A) & ( FinMeetCl A) c= ( UniCl ( FinMeetCl A)) by CANTOR_1: 1, CANTOR_1: 8;

        hence the carrier of T in the topology of T;

        hence for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T by A1;

        thus thesis by A1;

      end;

        suppose X <> {} ;

        hence thesis by CANTOR_1: 15;

      end;

    end;

    definition

      let I be set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      :: WAYBEL18:def3

      func product J -> strict TopSpace means

      : Def3: the carrier of it = ( product ( Carrier J)) & ( product_prebasis J) is prebasis of it ;

      existence

      proof

        set X = ( product ( Carrier J));

        reconsider A = ( product_prebasis J) as Subset-Family of X;

        consider T be strict TopStruct such that

         A1: T = TopStruct (# X, ( UniCl ( FinMeetCl A)) #);

        reconsider T as strict TopSpace by A1, Th3;

        take T;

        thus the carrier of T = ( product ( Carrier J)) by A1;

        now

          assume {} in ( rng ( Carrier J));

          then

          consider i be object such that

           A2: i in ( dom ( Carrier J)) and

           A3: {} = (( Carrier J) . i) by FUNCT_1:def 3;

          consider R be 1-sorted such that

           A4: R = (J . i) and

           A5: {} = the carrier of R by A2, A3, PRALG_1:def 15;

          ( dom J) = I by PARTFUN1:def 2;

          then R in ( rng J) by A2, A4, FUNCT_1:def 3;

          then

          reconsider R as non empty 1-sorted by WAYBEL_3:def 7;

          the carrier of R = {} by A5;

          hence contradiction;

        end;

        then X is non empty by CARD_3: 26;

        hence thesis by A1, CANTOR_1: 18;

      end;

      uniqueness

      proof

        let T1,T2 be strict TopSpace such 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;

        now

          assume {} in ( rng ( Carrier J));

          then

          consider i be object such that

           A10: i in ( dom ( Carrier J)) and

           A11: {} = (( Carrier J) . i) by FUNCT_1:def 3;

          consider R be 1-sorted such that

           A12: R = (J . i) and

           A13: {} = the carrier of R by A10, A11, PRALG_1:def 15;

          ( dom J) = I by PARTFUN1:def 2;

          then R in ( rng J) by A10, A12, FUNCT_1:def 3;

          then

          reconsider R as non empty 1-sorted by WAYBEL_3:def 7;

          the carrier of R = {} by A13;

          hence contradiction;

        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 thesis;

      end;

    end

    registration

      let I be set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      cluster ( product J) -> non empty;

      coherence

      proof

         A1:

        now

          assume {} in ( rng ( Carrier J));

          then

          consider i be object such that

           A2: i in ( dom ( Carrier J)) and

           A3: {} = (( Carrier J) . i) by FUNCT_1:def 3;

          consider R be 1-sorted such that

           A4: R = (J . i) and

           A5: {} = the carrier of R by A2, A3, PRALG_1:def 15;

          ( dom J) = I by PARTFUN1:def 2;

          then R in ( rng J) by A2, A4, FUNCT_1:def 3;

          then

          reconsider R as non empty 1-sorted by WAYBEL_3:def 7;

          the carrier of R = {} by A5;

          hence contradiction;

        end;

        the carrier of ( product J) = ( product ( Carrier J)) by Def3;

        then the carrier of ( product J) <> {} by A1, CARD_3: 26;

        hence thesis;

      end;

    end

    definition

      let I be non empty set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      let i be Element of I;

      :: original: .

      redefine

      func J . i -> non empty TopStruct ;

      coherence

      proof

        ( dom J) = I by PARTFUN1:def 2;

        then (J . i) in ( rng J) by FUNCT_1:def 3;

        hence thesis by WAYBEL_3:def 7;

      end;

    end

    registration

      let I be set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      cluster ( product J) -> constituted-Functions;

      coherence

      proof

        the carrier of ( product J) = ( product ( Carrier J)) by Def3;

        hence thesis by MONOID_0: 80;

      end;

    end

    definition

      let I be non empty set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      let x be Element of ( product J);

      let i be Element of I;

      :: original: .

      redefine

      func x . i -> Element of (J . i) ;

      coherence

      proof

        

         A1: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

        (ex R be 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 15;

        hence thesis by A1, CARD_3: 9;

      end;

    end

    definition

      let I be non empty set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      let i be Element of I;

      :: WAYBEL18:def4

      func proj (J,i) -> Function of ( product J), (J . i) equals ( proj (( Carrier J),i));

      coherence

      proof

        consider f be 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 object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) and

           A4: y = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of ( product J) by A2, A3;

          (f . x) = (x . i) by A1, A3, CARD_3:def 16;

          hence thesis by A4;

        end;

        hence thesis by A1, A2, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: WAYBEL18:4

    

     Th4: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, P be Subset of (J . i) holds (( proj (J,i)) " P) = ( product (( Carrier J) +* (i,P)))

    proof

      let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, P be Subset of (J . i);

      set f = (( Carrier J) +* (i,P));

      

       A1: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

      

       A2: ( dom f) = ( dom ( Carrier J)) by FUNCT_7: 30

      .= I by PARTFUN1:def 2;

      

       A3: ( product f) c= (( proj (J,i)) " P)

      proof

        let x be object;

        assume x in ( product f);

        then

        consider g be Function such that

         A4: x = g and

         A5: ( dom g) = ( dom f) and

         A6: for y be object st y in ( dom f) holds (g . y) in (f . y) by CARD_3:def 5;

        

         A7: for j be object st j in ( dom ( Carrier J)) holds (g . j) in (( Carrier J) . j)

        proof

          let j be object;

          assume j in ( dom ( Carrier J));

          then

           A8: j in I;

          then

           A9: ex R be 1-sorted st R = (J . j) & (( Carrier J) . j) = the carrier of R by PRALG_1:def 15;

          per cases ;

            suppose

             A10: j = i;

            (f . i) = P by A1, FUNCT_7: 31;

            then (g . j) in P by A2, A6, A10;

            hence thesis by A9, A10;

          end;

            suppose j <> i;

            then (f . j) = (( Carrier J) . j) by FUNCT_7: 32;

            hence thesis by A2, A6, A8;

          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;

        (f . 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 thesis by A4, A13, FUNCT_1:def 7;

      end;

      (( proj (J,i)) " P) c= ( product f)

      proof

        let x be object;

        assume

         A14: x in (( proj (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 be Function such that

         A16: x = g and

         A17: ( dom g) = ( dom ( Carrier J)) and

         A18: for y be object st y in ( dom ( Carrier J)) holds (g . y) in (( Carrier J) . y) by CARD_3:def 5;

        

         A19: ( dom g) = ( dom f) by A17, FUNCT_7: 30;

        for j be object st j in ( dom f) holds (g . j) in (f . j)

        proof

          let j be object;

          assume j in ( dom f);

          then

           A20: (g . j) in (( Carrier J) . j) by A17, A18, A19;

          per cases ;

            suppose

             A21: i = 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 thesis by A1, A21, FUNCT_7: 31;

          end;

            suppose i <> j;

            hence thesis by A20, FUNCT_7: 32;

          end;

        end;

        hence thesis by A16, A19, CARD_3:def 5;

      end;

      hence thesis by A3;

    end;

    theorem :: WAYBEL18:5

    

     Th5: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I holds ( proj (J,i)) is continuous

    proof

      let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I;

      

       A1: for P be Subset of (J . i) st P is open holds (( proj (J,i)) " P) is open

      proof

        let P be Subset of (J . i);

        assume

         A2: P is open;

        (( proj (J,i)) " P) c= ( product ( Carrier J))

        proof

          let x be object;

          assume x in (( proj (J,i)) " P);

          then x in ( dom ( proj (( Carrier J),i))) by FUNCT_1:def 7;

          hence thesis;

        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 thesis by A3;

      end;

      ( [#] (J . i)) <> {} ;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: WAYBEL18:6

    

     Th6: for X be non empty TopSpace, I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, f be Function of X, ( product J) holds f is continuous iff for i be Element of I holds (( proj (J,i)) * f) is continuous

    proof

      let X be non empty TopSpace, I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, f be Function of X, ( product J);

      set B = ( product_prebasis J);

      hereby

        assume

         A1: f is continuous;

        let i be Element of I;

        ( proj (J,i)) is continuous by Th5;

        hence (( proj (J,i)) * f) is continuous by A1, TOPS_2: 46;

      end;

      assume

       A2: for i be Element of I holds (( proj (J,i)) * f) is continuous;

      

       A3: for P be Subset of ( product J) st P in B holds (f " P) is open

      proof

        let P be Subset of ( product J);

        reconsider p = P as Subset of ( product ( Carrier J)) by Def3;

        assume P in B;

        then

        consider i be set, T be TopStruct, V be 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 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 thesis by A8, RELAT_1: 146;

      end;

      B is prebasis of ( product J) by Def3;

      hence thesis by A3, YELLOW_9: 36;

    end;

    begin

    definition

      let Z be TopStruct;

      :: WAYBEL18:def5

      attr Z is injective means for X be non empty TopSpace holds for f be Function of X, Z st f is continuous holds for Y be non empty TopSpace st X is SubSpace of Y holds ex g be Function of Y, Z st g is continuous & (g | the carrier of X) = f;

    end

    theorem :: WAYBEL18:7

    

     Th7: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is injective holds ( product J) is injective

    proof

      let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J . i) is injective;

      set B = ( product_prebasis J);

      let X be non empty TopSpace;

      let f be Function of X, ( product J);

      assume

       A2: f is continuous;

      let Y be non empty TopSpace;

      defpred P[ object, object] means ex i1 be Element of I st i1 = $1 & ex g be 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;

      

       A4: for i be object st i in I holds ex u be object st P[i, u]

      proof

        let i be object;

        assume i in I;

        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 be Function of Y, (J . i1) such that

         A5: g is continuous & (g | the carrier of X) = (( proj (J,i1)) * f) by A3;

        take g, i1;

        thus thesis by A5;

      end;

      consider G be Function such that

       A6: ( dom G) = I and

       A7: for i be object st i in I holds P[i, (G . i)] from CLASSES1:sch 1( A4);

      G is Function-yielding

      proof

        let j be object;

        assume j in ( dom G);

        then ex i be Element of I st i = j & ex g be 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 thesis;

      end;

      then

      reconsider G as Function-yielding Function;

      

       A8: the carrier of Y c= ( dom <:G:>)

      proof

        let x be object;

        consider i be object such that

         A9: i in I by XBOOLE_0:def 1;

        assume

         A10: x in the carrier of Y;

        

         A11: for f9 be Function st f9 in ( rng G) holds x in ( dom f9)

        proof

          let f9 be Function;

          assume f9 in ( rng G);

          then

          consider k be object such that

           A12: k in ( dom G) and

           A13: f9 = (G . k) by FUNCT_1:def 3;

          ex i1 be Element of I st i1 = k & ex ff be 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 thesis by A10, A13, FUNCT_2:def 1;

        end;

        consider j be Element of I such that j = i and

         A14: ex g be 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 be 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 thesis by A11, FUNCT_6: 33;

      end;

      

       A16: ( product ( rngs G)) c= ( product ( Carrier J))

      proof

        let y be object;

        assume y in ( product ( rngs G));

        then

        consider h be Function such that

         A17: y = h and

         A18: ( dom h) = ( dom ( rngs G)) and

         A19: for x be object st x in ( dom ( rngs G)) holds (h . x) in (( rngs G) . x) by CARD_3:def 5;

        

         A20: ( dom h) = I by A6, A18, FUNCT_6: 60

        .= ( dom ( Carrier J)) by PARTFUN1:def 2;

        for x be object st x in ( dom ( Carrier J)) holds (h . x) in (( Carrier J) . x)

        proof

          let x be object;

          assume

           A21: x in ( dom ( Carrier J));

          then

           A22: x in I;

          then

          consider i be Element of I such that

           A23: i = x and

           A24: ex g be Function of Y, (J . i) st g is continuous & (g | the carrier of X) = (( proj (J,i)) * f) & (G . x) = g by A7;

          

           A25: ex R be 1-sorted st R = (J . x) & (( Carrier J) . x) = the carrier of R by A22, PRALG_1:def 15;

          consider g be Function of Y, (J . i) such that g is continuous and (g | the carrier of X) = (( proj (J,i)) * f) and

           A26: (G . x) = g by A24;

          x in ( dom G) by A6, A21;

          then

           A27: (( rngs G) . x) = ( rng g) by A26, FUNCT_6: 22;

          (h . x) in (( rngs G) . x) by A18, A19, A20, A21;

          hence thesis by A23, A27, A25;

        end;

        hence thesis by A17, A20, CARD_3:def 5;

      end;

      ( dom <:G:>) c= the carrier of Y

      proof

        let x be object;

        assume

         A28: x in ( dom <:G:>);

        consider j be object such that

         A29: j in I by XBOOLE_0:def 1;

        consider i be Element of I such that i = j and

         A30: ex g be Function of Y, (J . i) st g is continuous & (g | the carrier of X) = (( proj (J,i)) * f) & (G . j) = g by A7, A29;

        consider g be Function of Y, (J . i) such that g is continuous and (g | the carrier of X) = (( proj (J,i)) * f) and

         A31: (G . j) = g by A30;

        g in ( rng G) by A6, A29, A31, FUNCT_1:def 3;

        then x in ( dom g) by A28, FUNCT_6: 32;

        hence thesis;

      end;

      then

       A32: ( dom <:G:>) = the carrier of Y by A8;

      ( rng <:G:>) c= ( product ( rngs G)) by FUNCT_6: 29;

      then

       A33: ( rng <:G:>) c= ( product ( Carrier J)) by A16;

      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 A32, FUNCT_2:def 1, RELSET_1: 4;

      

       A34: ( 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;

      

       A35: for x be object st x in ( dom (h | the carrier of X)) holds ((h | the carrier of X) . x) = (f . x)

      proof

        let x be object;

        assume

         A36: x in ( dom (h | the carrier of X));

        then

         A37: x in ( dom h) by RELAT_1: 57;

        ((h | the carrier of X) . x) in ( rng (h | the carrier of X)) by A36, FUNCT_1:def 3;

        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 be Function such that

         A38: ((h | the carrier of X) . x) = z and

         A39: ( dom z) = ( dom ( Carrier J)) and for i be object st i in ( dom ( Carrier J)) holds (z . i) in (( Carrier J) . i) by CARD_3:def 5;

        (f . x) in ( rng f) by A34, A36, FUNCT_1:def 3;

        then (f . x) in the carrier of ( product J);

        then

         A40: (f . x) in ( product ( Carrier J)) by Def3;

        then

        consider y be Function such that

         A41: (f . x) = y and

         A42: ( dom y) = ( dom ( Carrier J)) and for i be object st i in ( dom ( Carrier J)) holds (y . i) in (( Carrier J) . i) by CARD_3:def 5;

        

         A43: x in the carrier of Y by A37;

        for j be object st j in ( dom y) holds (y . j) = (z . j)

        proof

          let j be object;

          assume j in ( dom y);

          then

           A44: j in I by A42;

          then

          consider i be Element of I such that

           A45: i = j and

           A46: ex g be Function of Y, (J . i) st g is continuous & (g | the carrier of X) = (( proj (J,i)) * f) & (G . j) = g by A7;

          

           A47: y in ( dom ( proj (( Carrier J),i))) by A40, A41, CARD_3:def 16;

          consider g be Function of Y, (J . i) such that g is continuous and

           A48: (g | the carrier of X) = (( proj (J,i)) * f) and

           A49: (G . j) = g by A46;

          x in ( dom h) & z = ( <:G:> . x) by A36, A43, A38, FUNCT_1: 49, FUNCT_2:def 1;

          

          hence (z . j) = (g . x) by A6, A44, A49, FUNCT_6: 34

          .= ((( proj (J,i)) * f) . x) by A36, A48, FUNCT_1: 49

          .= (( proj (( Carrier J),i)) . y) by A36, A41, FUNCT_2: 15

          .= (y . j) by A45, A47, CARD_3:def 16;

        end;

        hence thesis by A41, A42, A38, A39, FUNCT_1: 2;

      end;

      reconsider h as Function of Y, ( product J);

      

       A50: for P be Subset of ( product J) st P in B holds (h " P) is open

      proof

        let P be Subset of ( product J);

        reconsider p = P as Subset of ( product ( Carrier J)) by Def3;

        assume P in B;

        then

        consider i be set, T be TopStruct, V be Subset of T such that

         A51: i in I and

         A52: V is open and

         A53: T = (J . i) and

         A54: p = ( product (( Carrier J) +* (i,V))) by Def2;

        consider j be Element of I such that

         A55: j = i and

         A56: ex g be Function of Y, (J . j) st g is continuous & (g | the carrier of X) = (( proj (J,j)) * f) & (G . i) = g by A7, A51;

        reconsider V as Subset of (J . j) by A53, A55;

        

         A57: ( dom ( proj (J,j))) = ( product ( Carrier J)) by CARD_3:def 16;

        consider g be Function of Y, (J . j) such that

         A58: g is continuous and (g | the carrier of X) = (( proj (J,j)) * f) and

         A59: (G . i) = g by A56;

        

         A60: ( dom g) = the carrier of Y by FUNCT_2:def 1

        .= ( dom h) by FUNCT_2:def 1;

        

         A61: (( proj (J,j)) " V) = p by A54, A55, Th4;

        

         A62: (h " P) c= (g " V)

        proof

          let x be object;

          assume

           A63: x in (h " P);

          then

           A64: (h . x) in (( proj (J,j)) " V) by A61, FUNCT_1:def 7;

          then (h . x) in ( product ( Carrier J)) by A57, FUNCT_1:def 7;

          then

          consider y be Function such that

           A65: (h . x) = y and ( dom y) = ( dom ( Carrier J)) and for i be object 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 A64, FUNCT_1:def 7;

          then (( proj (J,j)) . (h . x)) = (y . j) by A65, CARD_3:def 16;

          then

           A66: (y . j) in V by A64, FUNCT_1:def 7;

          x in ( dom h) by A63, FUNCT_1:def 7;

          then

           A67: (g . x) = (y . j) by A6, A55, A59, A65, FUNCT_6: 34;

          x in ( dom g) by A60, A63, FUNCT_1:def 7;

          hence thesis by A66, A67, FUNCT_1:def 7;

        end;

        

         A68: (g " V) c= (h " P)

        proof

          let x be object;

          assume

           A69: x in (g " V);

          then

           A70: x in ( dom h) by A60, FUNCT_1:def 7;

          then

           A71: (h . x) in ( rng h) by FUNCT_1:def 3;

          then

          consider y be Function such that

           A72: (h . x) = y and ( dom y) = ( dom ( Carrier J)) and for i be object st i in ( dom ( Carrier J)) holds (y . i) in (( Carrier J) . i) by A33, CARD_3:def 5;

          (h . x) in ( product ( Carrier J)) by A33, A71;

          then y in ( dom ( proj (( Carrier J),j))) by A72, CARD_3:def 16;

          then

           A73: (( proj (J,j)) . (h . x)) = (y . j) by A72, CARD_3:def 16;

          (g . x) = (y . j) by A6, A55, A59, A70, A72, FUNCT_6: 34;

          then (( proj (J,j)) . (h . x)) in V by A69, A73, FUNCT_1:def 7;

          then (h . x) in (( proj (J,j)) " V) by A33, A57, A71, FUNCT_1:def 7;

          hence thesis by A61, A70, FUNCT_1:def 7;

        end;

        ( [#] (J . j)) <> {} ;

        then (g " V) is open by A52, A53, A55, A58, TOPS_2: 43;

        hence thesis by A62, A68, XBOOLE_0:def 10;

      end;

      take h;

      B is prebasis of ( product J) by Def3;

      hence h is continuous by A50, YELLOW_9: 36;

      thus thesis by A34, A35, FUNCT_1: 2;

    end;

    theorem :: WAYBEL18:8

    for T be non empty TopSpace st T is injective holds for S be non empty SubSpace of T st S is_a_retract_of T holds S is injective

    proof

      let T be non empty TopSpace;

      assume

       A1: T is injective;

      let S be non empty SubSpace of T;

      set p = ( incl S);

      assume S is_a_retract_of T;

      then

      consider r be continuous Function of T, S such that

       A2: r is being_a_retraction by BORSUK_1:def 17;

      let X be non empty TopSpace, F be Function of X, S;

      assume

       A3: F is continuous;

      reconsider f = (p * F) as Function of X, T;

      let Y be non empty TopSpace;

      assume

       A4: X is SubSpace of Y;

      p is continuous by TMAP_1: 87;

      then

      consider g be Function of Y, T such that

       A5: g is continuous and

       A6: (g | the carrier of X) = f by A1, A3, A4;

      take G = (r * g);

      

       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 be object st x in ( dom F) holds (F . x) = (G . x)

      proof

        let x be object;

        assume

         A10: x in ( dom F);

        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) = (p . 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 thesis by A8, A13, A11, FUNCT_2: 15;

      end;

      thus G is continuous by A5;

      

       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 thesis by A14, A9, FUNCT_1: 46;

    end;

    definition

      let X be 1-sorted, Y be TopStruct, f be Function of X, Y;

      :: WAYBEL18:def6

      func Image f -> SubSpace of Y equals (Y | ( rng f));

      coherence ;

    end

    registration

      let X be non empty 1-sorted, Y be non empty TopStruct, f be Function of X, Y;

      cluster ( Image f) -> non empty;

      coherence ;

    end

    theorem :: WAYBEL18:9

    

     Th9: for X be 1-sorted, Y be TopStruct, f be Function of X, Y holds the carrier of ( Image f) = ( rng f)

    proof

      let X be 1-sorted, Y be TopStruct, f be Function of X, Y;

      

      thus the carrier of ( Image f) = ( [#] (Y | ( rng f)))

      .= ( rng f) by PRE_TOPC:def 5;

    end;

    definition

      let X be 1-sorted, Y be non empty TopStruct, f be Function of X, Y;

      :: WAYBEL18:def7

      func corestr (f) -> Function of X, ( Image f) equals f;

      coherence

      proof

        the carrier of ( Image f) = ( rng f) & the carrier of X = ( dom f) by Th9, FUNCT_2:def 1;

        hence thesis by FUNCT_2: 1;

      end;

    end

    theorem :: WAYBEL18:10

    

     Th10: for X,Y be non empty TopSpace, f be Function of X, Y st f is continuous holds ( corestr f) is continuous

    proof

      let X,Y be non empty TopSpace;

      let f be Function of X, Y;

      

       A1: f is Function of ( dom f), ( rng f) by FUNCT_2: 1;

      

       A2: ( [#] Y) <> {} ;

      assume

       A3: f is continuous;

      

       A4: for R be 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;

        let R be Subset of ( Image f);

        assume R is open;

        then R in the topology of ( Image f);

        then

        consider Q be 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 as Subset of Y;

        Q is open by A7;

        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 thesis by A8, A9, A6, TOPS_1: 11;

      end;

      ( [#] ( Image f)) <> {} ;

      hence thesis by A4, TOPS_2: 43;

    end;

    registration

      let X be 1-sorted, Y be non empty TopStruct;

      let f be Function of X, Y;

      cluster ( corestr f) -> onto;

      coherence

      proof

        the carrier of ( Image f) = ( rng ( corestr f)) by Th9;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    definition

      let X,Y be TopStruct;

      :: WAYBEL18:def8

      pred X is_Retract_of Y means ex f be Function of Y, Y st f is continuous & (f * f) = f & (( Image f),X) are_homeomorphic ;

    end

    theorem :: WAYBEL18:11

    

     Th11: for T,S be non empty TopSpace st T is injective holds for f be Function of T, S st ( corestr f) is being_homeomorphism holds T is_Retract_of S

    proof

      let T,S be non empty TopSpace;

      assume

       A1: T is injective;

      let f be Function of T, S;

      consider g be Function of ( Image f), T such that

       A2: g = (( corestr f) " );

      assume

       A3: ( corestr f) is being_homeomorphism;

      then g is continuous by A2, TOPS_2:def 5;

      then

      consider h be Function of S, T such that

       A4: h is continuous and

       A5: (h | the carrier of ( Image f)) = g by A1;

      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 be object st x in the carrier of T holds ((h * f) . x) = x

      proof

        let x be object;

        assume

         A9: x in the carrier of T;

        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) qua Function " ) . (( corestr f) . x)) by A13, TOPS_2:def 4

        .= x by A10, A13, FUNCT_1: 34;

      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);

      set H = (h * ( incl ( Image F)));

      

       A15: ( dom H) = ( [#] ( 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 object;

        assume y in ( rng F);

        then

        consider x be object 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 thesis by A16, A21, FUNCT_1:def 3;

      end;

      

       A22: H is one-to-one

      proof

        let x,y be Element of ( Image F);

        assume

         A23: (H . x) = (H . 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 thesis by A6;

      end;

      

       A30: ( dom ( incl ( Image F))) = the carrier of ( Image F) by FUNCT_2:def 1;

      

       A31: ( rng H) = ( [#] T)

      proof

        thus ( rng H) c= ( [#] T);

        let y be object;

        assume

         A32: y in ( [#] T);

        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) = ( rng F) by A15, Th9;

        then

         A39: (f . y) in ( dom H) by A36, A34, FUNCT_1:def 3;

        (H . (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 thesis by A39, FUNCT_1:def 3;

      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 be Subset of S holds (f " P) = ((p * ( corestr f)) " P)

      proof

        let P be Subset of S;

        hereby

          let x be object;

          assume

           A43: x in (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;

        end;

        let x be object;

        assume

         A47: x in ((p * ( corestr 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 thesis by A41, A48, A50, FUNCT_1:def 7;

      end;

      

       A52: ( corestr f) is continuous by A3, TOPS_2:def 5;

      

       A53: for P be Subset of ( Image F) st P is open holds ((H " ) " P) is open

      proof

        let P be Subset of ( Image F);

        

         A54: p is continuous by TMAP_1: 87;

        (( incl ( Image F)) .: P) = P

        proof

          hereby

            let y be object;

            assume y in (( incl ( Image F)) .: P);

            then

            consider x be object 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;

          end;

          let y be object;

          assume

           A57: y in 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 thesis by A57, A59, FUNCT_1:def 6;

        end;

        then

         A60: (H .: P) = (h .: P) by RELAT_1: 126;

        assume P is open;

        then P in the topology of ( Image F);

        then

        consider Q be 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 as Subset of S;

        

         A63: (f " Q) = (h .: P)

        proof

          hereby

            let x be object;

            assume

             A64: x in (f " Q);

            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;

          end;

          let x be object;

          assume x in (h .: P);

          then

          consider y be object 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;

          hence thesis by A16, A76, FUNCT_1:def 7;

        end;

        Q is open by A61;

        then ((p * ( corestr f)) " Q) is open by A40, A52, A54, TOPS_2: 43;

        then (f " Q) is open by A42;

        hence thesis by A31, A22, A63, A60, TOPS_2: 54;

      end;

      

       A77: p is continuous by TMAP_1: 87;

      

       A78: ( [#] T) <> {} ;

      for P be Subset of S st P is open holds (F " P) is open

      proof

        let P be Subset of S;

        assume 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 thesis by RELAT_1: 146;

      end;

      hence F is continuous by A40, TOPS_2: 43;

      

      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;

      ( [#] ( Image F)) <> {} ;

      then ( incl ( Image F)) is continuous & (H " ) is continuous by A53, TMAP_1: 87, TOPS_2: 43;

      then H is being_homeomorphism by A4, A15, A31, A22, TOPS_2:def 5;

      hence thesis by T_0TOPSP:def 1;

    end;

    definition

      :: WAYBEL18:def9

      func Sierpinski_Space -> strict TopStruct means

      : Def9: the carrier of it = { 0 , 1} & the topology of it = { {} , {1}, { 0 , 1}};

      existence

      proof

        set c = { 0 , 1}, t = { {} , {1}, { 0 , 1}};

        t c= ( bool c)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A1: x in t;

          per cases by A1, ENUMSET1:def 1;

            suppose

             A2: x = {} ;

             {} c= c;

            hence thesis by A2;

          end;

            suppose x = {1};

            then xx c= c by ZFMISC_1: 7;

            hence thesis;

          end;

            suppose x = { 0 , 1};

            then xx c= c;

            hence thesis;

          end;

        end;

        then

        reconsider t as Subset-Family of c;

        take s = TopStruct (# c, t #);

        thus the carrier of s = { 0 , 1};

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      cluster Sierpinski_Space -> non empty TopSpace-like;

      coherence

      proof

        set IT = Sierpinski_Space ;

        thus IT is non empty by Def9;

         { 0 , 1} in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

        then the carrier of IT in { {} , {1}, { 0 , 1}} by Def9;

        hence the carrier of IT in the topology of IT by Def9;

        thus for a be Subset-Family of IT st a c= the topology of IT holds ( union a) in the topology of IT

        proof

          let a be Subset-Family of IT;

          assume a c= the topology of IT;

          then

           A1: a c= { {} , {1}, { 0 , 1}} by Def9;

          per cases by A1, ZFMISC_1: 118;

            suppose a = {} ;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1, ZFMISC_1: 2;

            hence thesis by Def9;

          end;

            suppose a = { {} };

            then ( union a) = {} by ZFMISC_1: 25;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

            hence thesis by Def9;

          end;

            suppose a = { {1}};

            then ( union a) = {1} by ZFMISC_1: 25;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

            hence thesis by Def9;

          end;

            suppose a = { { 0 , 1}};

            then ( union a) = { 0 , 1} by ZFMISC_1: 25;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

            hence thesis by Def9;

          end;

            suppose a = { {} , {1}};

            then ( union a) = ( {} \/ {1}) by ZFMISC_1: 75;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

            hence thesis by Def9;

          end;

            suppose a = { {1}, { 0 , 1}};

            

            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 thesis by Def9;

          end;

            suppose a = { {} , { 0 , 1}};

            then ( union a) = ( {} \/ { 0 , 1}) by ZFMISC_1: 75;

            then ( union a) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

            hence thesis by Def9;

          end;

            suppose a = { {} , {1}, { 0 , 1}};

            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 thesis by Def9;

          end;

        end;

        let a,b be Subset of IT;

        assume a in the topology of IT & b in the topology of IT;

        then

         A2: a in { {} , {1}, { 0 , 1}} & b in { {} , {1}, { 0 , 1}} by Def9;

        per cases by A2, ENUMSET1:def 1;

          suppose a = {} & b = {} ;

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = {} & b = {1};

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = {} & b = { 0 , 1};

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = {1} & b = {} ;

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = {1} & b = {1};

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = {1} & b = { 0 , 1};

          then (a /\ b) = {1} by ZFMISC_1: 13;

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = { 0 , 1} & b = {} ;

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = { 0 , 1} & b = {1};

          then (a /\ b) = {1} by ZFMISC_1: 13;

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

          suppose a = { 0 , 1} & b = { 0 , 1};

          then (a /\ b) in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

          hence thesis by Def9;

        end;

      end;

    end

    

     Lm1: Sierpinski_Space is T_0

    proof

      set S = Sierpinski_Space ;

      for x,y be Point of S st x <> y holds ex V be Subset of S 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 S;

        y in the carrier of S;

        then

         A1: y in { 0 , 1} by Def9;

         {1} c= { 0 , 1} by ZFMISC_1: 7;

        then

        reconsider V as Subset of S by Def9;

        x in the carrier of S;

        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 S by Def9;

        then

         A3: V is open;

        assume

         A4: x <> y;

        per cases by A4, A1, A2, TARSKI:def 2;

          suppose x = 0 & y = 1;

          then x in V & not y in V or y in V & not x in V by TARSKI:def 1;

          hence thesis by A3;

        end;

          suppose x = 1 & y = 0 ;

          then x in V & not y in V or y in V & not x in V by TARSKI:def 1;

          hence thesis by A3;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster Sierpinski_Space -> T_0;

      coherence by Lm1;

    end

    registration

      cluster Sierpinski_Space -> injective;

      coherence

      proof

        let X be non empty TopSpace;

        set S = Sierpinski_Space ;

        let f be Function of X, S;

        

         A1: ( [#] S) <> {} ;

         {1} c= { 0 , 1} by ZFMISC_1: 7;

        then

        reconsider u = {1} as Subset of S by Def9;

        u in { {} , {1}, { 0 , 1}} by ENUMSET1:def 1;

        then u in the topology of S by Def9;

        then

         A2: u is open;

        assume f is continuous;

        then (f " u) is open by A1, A2, TOPS_2: 43;

        then

         A3: (f " u) in the topology of X;

        let Y be non empty TopSpace;

        assume

         A4: X is SubSpace of Y;

        then

        consider V be 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 as Subset of Y;

        set g = ( chi (V,the carrier of Y));

        

         A7: ( dom g) = the carrier of Y by FUNCT_3:def 3;

        reconsider g as Function of Y, S by Def9;

        

         A8: the carrier of X c= the carrier of Y by A4, BORSUK_1: 1;

        

         A9: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume

           A10: x in ( dom f);

          then

           A11: x in the carrier of X;

          per cases ;

            suppose

             A12: x in V;

            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 thesis by A13, TARSKI:def 1;

          end;

            suppose

             A14: not x in V;

            (f . x) in ( rng f) by A10, FUNCT_1:def 3;

            then (f . x) in the carrier of S;

            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 thesis by A8, A10, A11, A14, A15, FUNCT_3:def 3, TARSKI:def 1;

          end;

        end;

        take g;

        

         A16: V is open by A5;

        for P be Subset of S st P is open holds (g " P) is open

        proof

          let P be Subset of S;

          assume P is open;

          then P in the topology of S;

          then

           A17: P in { {} , {1}, { 0 , 1}} by Def9;

          per cases by A17, ENUMSET1:def 1;

            suppose P = {} ;

            then (g " P) = {} ;

            then (g " P) in the topology of Y by PRE_TOPC: 1;

            hence thesis;

          end;

            suppose

             A18: P = {1};

            

             A19: (g " P) c= V

            proof

              let x be object;

              assume

               A20: x in (g " P);

              then (g . x) in {1} by A18, FUNCT_1:def 7;

              then (g . x) = 1 by TARSKI:def 1;

              hence thesis by A20, FUNCT_3:def 3;

            end;

            V c= (g " P)

            proof

              let x be object;

              assume

               A21: x in V;

              then (g . x) = 1 by FUNCT_3:def 3;

              then (g . x) in {1} by TARSKI:def 1;

              hence thesis by A7, A18, A21, FUNCT_1:def 7;

            end;

            hence thesis by A16, A19, XBOOLE_0:def 10;

          end;

            suppose P = { 0 , 1};

            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 thesis;

          end;

        end;

        hence g is continuous by A1, TOPS_2: 43;

        (( 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 thesis by A9, FUNCT_1: 46;

      end;

    end

    registration

      let I be set;

      let S be non empty 1-sorted;

      cluster (I --> S) -> non-Empty;

      coherence

      proof

        let s be 1-sorted;

        assume s in ( rng (I --> S));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be set;

      let T be TopStruct;

      cluster (I --> T) -> TopStruct-yielding;

      coherence

      proof

        let x be object;

        assume x in ( rng (I --> T));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let I be non empty set;

      let L be non empty antisymmetric RelStr;

      cluster ( product (I --> L)) -> antisymmetric;

      coherence

      proof

        for i be Element of I holds ((I --> L) . i) is antisymmetric;

        hence thesis by WAYBEL_3: 30;

      end;

    end

    registration

      let I be non empty set;

      let L be non empty transitive RelStr;

      cluster ( product (I --> L)) -> transitive;

      coherence

      proof

        for i be Element of I holds ((I --> L) . i) is transitive;

        hence thesis by WAYBEL_3: 29;

      end;

    end

    theorem :: WAYBEL18:12

    for T be Scott TopAugmentation of ( BoolePoset { 0 }) holds the topology of T = the topology of Sierpinski_Space

    proof

      let T be Scott TopAugmentation of ( BoolePoset { 0 });

      

       A1: ( LattPOSet ( BooleLatt { 0 })) = RelStr (# the carrier of ( BooleLatt { 0 }), ( LattRel ( BooleLatt { 0 })) #) by LATTICE3:def 2;

      

       A2: the RelStr of T = ( BoolePoset { 0 }) by YELLOW_9:def 4;

      

      then

       A3: the carrier of T = the carrier of ( LattPOSet ( BooleLatt { 0 })) by YELLOW_1:def 2

      .= ( bool { 0 }) by A1, LATTICE3:def 1

      .= { 0 , 1} by CARD_1: 49, ZFMISC_1: 24;

      then

      reconsider j = { 0 }, z = 0 as Element of ( BoolePoset { 0 }) by A2, TARSKI:def 2, CARD_1: 49;

       A4:

      now

        let x be object;

        assume x in the topology of Sierpinski_Space ;

        then

         A5: x in { {} , { { 0 }}, { 0 , { 0 }}} by Def9, CARD_1: 49;

        per cases by A5, ENUMSET1:def 1, CARD_1: 49;

          suppose x = {} ;

          hence x in the topology of T by PRE_TOPC: 1;

        end;

          suppose

           A6: x = { { 0 }};

          then

          reconsider x9 = x as Subset of T by A3, ZFMISC_1: 7, CARD_1: 49;

          for a,b be Element of T st a in x9 & a <= b holds b in x9

          proof

            let a,b be Element of T;

            assume that

             A7: a in x9 and

             A8: a <= b;

            

             A9: a = { 0 } by A6, A7, TARSKI:def 1;

            

             A10: b <> 0

            proof

              assume

               A11: b = 0 ;

               [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 { 0 } c= {} by YELLOW_1: 2;

              hence thesis;

            end;

            b = 0 or b = 1 by A3, TARSKI:def 2;

            hence thesis by A6, A10, TARSKI:def 1, CARD_1: 49;

          end;

          then

           A12: x9 is upper by WAYBEL_0:def 20;

          for D be 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;

            assume

             A13: ( sup D) in x9;

            D <> { 0 }

            proof

              assume D = { 0 };

              

              then ( sup D) = ( sup {z}) by A2, YELLOW_0: 17, YELLOW_0: 26

              .= 0 by YELLOW_0: 39;

              hence thesis by A6, A13, TARSKI:def 1;

            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, CARD_1: 49;

            hence thesis by A14, XBOOLE_0: 3;

          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;

        end;

          suppose x = { 0 , 1};

          hence x in the topology of T by A3, PRE_TOPC:def 1;

        end;

      end;

      reconsider c = {z} as Subset of T by A2;

      now

        set a = 0 , b = { 0 };

        let y be object;

        

         A15: not b in {z};

        a c= b & a in {z} by TARSKI:def 1;

        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;

        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;

        hence y in the topology of Sierpinski_Space by Def9;

      end;

      hence thesis by A4, TARSKI: 2;

    end;

    theorem :: WAYBEL18:13

    

     Th13: for I be non empty set holds the set of all ( product (( Carrier (I --> Sierpinski_Space )) +* (i, {1}))) where i be Element of I is prebasis of ( product (I --> Sierpinski_Space ))

    proof

      let I be non empty set;

      set IS = (I --> Sierpinski_Space ), pB = the set of all ( product (( Carrier IS) +* (i, {1}))) where i be Element of I;

      set P = ( product_prebasis IS);

      

       A1: P is prebasis of ( product IS) by Def3;

      then

       A2: P c= the topology of ( product IS) by TOPS_2: 64;

      pB c= ( bool the carrier of ( product IS))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in pB;

        then

        consider i be Element of I such that

         A3: x = ( product (( Carrier IS) +* (i, {1})));

        ( product (( Carrier IS) +* (i, {1}))) c= ( product ( Carrier IS))

        proof

          let y be object;

          assume y in ( product (( Carrier IS) +* (i, {1})));

          then

          consider g be Function such that

           A4: y = g and

           A5: ( dom g) = ( dom (( Carrier IS) +* (i, {1}))) and

           A6: for z be object st z in ( dom (( Carrier IS) +* (i, {1}))) holds (g . z) in ((( Carrier IS) +* (i, {1})) . z) by CARD_3:def 5;

          

           A7: for z be object st z in ( dom ( Carrier IS)) holds (g . z) in (( Carrier IS) . z)

          proof

            let z be object;

            assume

             A8: z in ( dom ( Carrier IS));

            then

             A9: z in I;

            then

            consider R be 1-sorted such that

             A10: R = (IS . z) and

             A11: (( Carrier IS) . z) = the carrier of R by PRALG_1:def 15;

            

             A12: the carrier of R = the carrier of Sierpinski_Space by A9, A10, FUNCOP_1: 7

            .= { 0 , 1} by Def9;

            z in ( dom (( Carrier IS) +* (i, {1}))) by A8, FUNCT_7: 30;

            then

             A13: (g . z) in ((( Carrier IS) +* (i, {1})) . z) by A6;

            per cases ;

              suppose z = i;

              then ((( Carrier IS) +* (i, {1})) . z) = {1} by A8, FUNCT_7: 31;

              then (g . z) = 1 by A13, TARSKI:def 1;

              hence thesis by A11, A12, TARSKI:def 2;

            end;

              suppose z <> i;

              hence thesis by A13, FUNCT_7: 32;

            end;

          end;

          ( dom g) = ( dom ( Carrier IS)) by A5, FUNCT_7: 30;

          hence thesis by A4, A7, CARD_3:def 5;

        end;

        then xx c= the carrier of ( product IS) by A3, Def3;

        hence thesis;

      end;

      then

      reconsider B = pB as Subset-Family of ( product IS);

      reconsider B as Subset-Family of ( product IS);

      

       A14: B c= P

      proof

         {1} c= { 0 , 1} by ZFMISC_1: 7;

        then

        reconsider V = {1} as Subset of Sierpinski_Space by Def9;

        let x be object;

        assume

         A15: x in B;

        then

        consider i be Element of I such that

         A16: x = ( product (( Carrier IS) +* (i, {1})));

        reconsider y = x as Subset of ( product ( Carrier IS)) 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;

         Sierpinski_Space = (IS . i) & y = ( product (( Carrier IS) +* (i,V))) by A16;

        hence thesis by A17, Def2;

      end;

      reconsider P as Subset-Family of ( product IS) by Def3;

      reconsider P as Subset-Family of ( product IS);

      ( FinMeetCl P) is Basis of ( product IS) by A1, YELLOW_9: 23;

      then

      reconsider F = (( FinMeetCl P) \ { {} }) as Basis of ( product IS) by Th2;

      

       A18: F c= ( FinMeetCl B)

      proof

        let x be object;

        assume

         A19: x in F;

        then

        reconsider y = x as Subset of ( product IS);

        x in ( FinMeetCl P) by A19, XBOOLE_0:def 5;

        then

        consider Y1 be Subset-Family of ( product IS) 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 IS);

        

         A23: Y2 c= B & Y2 is finite by A21, FINSET_1: 1, XBOOLE_1: 17;

        

         A24: the carrier of ( product IS) = ( product ( Carrier IS)) by Def3;

        

         A25: not x in { {} } by A19, XBOOLE_0:def 5;

        

         A26: ( Intersect Y2) c= ( Intersect Y1)

        proof

          let z be object;

          assume

           A27: z in ( Intersect Y2);

          then

           A28: z in ( product ( Carrier IS)) by A24;

          for Y be set st Y in Y1 holds z in Y

          proof

            let Y be set;

            assume

             A29: Y in Y1;

            then

            reconsider Y9 = Y as Subset of ( product ( Carrier IS)) by Def3;

            consider i be set, S be TopStruct, V be Subset of S such that

             A30: i in I and

             A31: V is open and

             A32: S = (IS . i) and

             A33: Y9 = ( product (( Carrier IS) +* (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;

            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 IS)) by A30, PARTFUN1:def 2;

            

             A36: V9 <> {}

            proof

              ((( Carrier IS) +* (i, {} )) . i) = {} & i in ( dom (( Carrier IS) +* (i, {} ))) by A35, FUNCT_7: 30, FUNCT_7: 31;

              then

               A37: {} in ( rng (( Carrier IS) +* (i, {} ))) by FUNCT_1:def 3;

              assume V9 = {} ;

              then Y9 = {} by A33, A37, CARD_3: 26;

              then y = {} by A22, A29, MSSUBFAM: 3;

              hence thesis by A25, TARSKI:def 1;

            end;

            reconsider i9 = i as Element of I by A30;

            

             A38: ex RR be 1-sorted st RR = (IS . i) & (( Carrier IS) . i) = the carrier of RR by A30, PRALG_1:def 15;

            per cases by A34, A36, ENUMSET1:def 1;

              suppose V9 = {1};

              then Y9 = ( product (( Carrier IS) +* (i9, {1}))) by A33;

              then Y in B;

              then Y in Y2 by A29, XBOOLE_0:def 4;

              hence thesis by A27, SETFAM_1: 43;

            end;

              suppose V9 = { 0 , 1};

              

              then V9 = the carrier of Sierpinski_Space by Def9

              .= (( Carrier IS) . i) by A30, A38, FUNCOP_1: 7;

              hence thesis by A28, A33, FUNCT_7: 35;

            end;

          end;

          hence thesis by A27, SETFAM_1: 43;

        end;

        ( Intersect Y1) c= ( Intersect Y2) by SETFAM_1: 44, XBOOLE_1: 17;

        then y = ( Intersect Y2) by A22, A26;

        hence thesis by A23, CANTOR_1:def 3;

      end;

      pB c= the topology of ( product IS) by A14, A2;

      hence thesis by A18, CANTOR_1:def 4, TOPS_2: 64;

    end;

    registration

      let I be non empty set;

      let L be complete LATTICE;

      cluster ( product (I --> L)) -> with_suprema complete;

      coherence

      proof

        reconsider IB = (I --> L) as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

        for i be Element of I holds (IB . i) is complete LATTICE;

        hence thesis by WAYBEL_3: 31;

      end;

    end

    registration

      let I be non empty set;

      let X be algebraic lower-bounded LATTICE;

      cluster ( product (I --> X)) -> algebraic;

      coherence

      proof

        set IB = (I --> X);

        for i be Element of I holds (IB . i) is algebraic lower-bounded LATTICE;

        hence thesis by WAYBEL13: 25;

      end;

    end

    theorem :: WAYBEL18:14

    

     Th14: for X be non empty set holds ex f be Function of ( BoolePoset X), ( product (X --> ( BoolePoset { 0 }))) st f is isomorphic & for Y be Subset of X holds (f . Y) = ( chi (Y,X))

    proof

      let X be non empty set;

      set XB = (X --> ( BoolePoset { 0 }));

      deffunc F( set) = ( chi ($1,X));

      consider f be Function such that

       A1: ( dom f) = ( bool X) and

       A2: for Y be set st Y in ( bool X) holds (f . Y) = F(Y) from FUNCT_1:sch 5;

      ( LattPOSet ( BooleLatt { 0 })) = RelStr (# the carrier of ( BooleLatt { 0 }), ( LattRel ( BooleLatt { 0 })) #) by LATTICE3:def 2;

      

      then

       A3: the carrier of ( BoolePoset { 0 }) = the carrier of ( BooleLatt { 0 }) by YELLOW_1:def 2

      .= ( bool { {} }) by LATTICE3:def 1

      .= { 0 , 1} by CARD_1: 49, ZFMISC_1: 24;

      

       A4: ( rng f) c= ( product ( Carrier XB))

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A5: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        

         A6: ( dom ( chi (x,X))) = X by FUNCT_3:def 3

        .= ( dom ( Carrier XB)) by PARTFUN1:def 2;

        

         A7: for z be object st z in ( dom ( Carrier XB)) holds (( chi (x,X)) . z) in (( Carrier XB) . z)

        proof

          let z be object;

          assume z in ( dom ( Carrier XB));

          then

           A8: z in X;

          then ex R be 1-sorted st R = (XB . z) & (( Carrier XB) . z) = the carrier of R by PRALG_1:def 15;

          then

           A9: (( Carrier XB) . z) = { 0 , 1} by A3, A8, FUNCOP_1: 7;

          per cases ;

            suppose z in x;

            then (( chi (x,X)) . z) = 1 by A8, FUNCT_3:def 3;

            hence thesis by A9, TARSKI:def 2;

          end;

            suppose not z in x;

            then (( chi (x,X)) . z) = 0 by A8, FUNCT_3:def 3;

            hence thesis by A9, TARSKI:def 2;

          end;

        end;

        ( chi (x,X)) = y by A1, A2, A5;

        hence thesis by A6, A7, CARD_3:def 5;

      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 XB) = ( product ( Carrier XB)) by YELLOW_1:def 4;

      then

      reconsider f as Function of ( BoolePoset X), ( product (X --> ( BoolePoset { 0 }))) by A10, A1, A4, FUNCT_2:def 1, RELSET_1: 4;

      

       A12: for A,B be Element of ( BoolePoset X) holds A <= B iff (f . A) <= (f . B)

      proof

        let A,B be Element of ( BoolePoset X);

        

         A13: (f . A) = ( chi (A,X)) & (f . B) = ( chi (B,X)) by A10, A2;

        hereby

          assume A <= B;

          then

           A14: A c= B by YELLOW_1: 2;

          for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (XB . i) & xi = (( chi (A,X)) . i) & yi = (( chi (B,X)) . i) & xi <= yi

          proof

            let i be object;

            assume

             A15: i in X;

            take R = ( BoolePoset { 0 });

            per cases ;

              suppose

               A16: i in A;

              reconsider xi = 1, yi = 1 as Element of R by A3, TARSKI:def 2;

              take xi, yi;

              thus R = (XB . i) by A15, FUNCOP_1: 7;

              thus xi = (( chi (A,X)) . i) by A15, A16, FUNCT_3:def 3;

              thus yi = (( chi (B,X)) . i) by A14, A15, A16, FUNCT_3:def 3;

              thus xi <= yi;

            end;

              suppose

               A17: not i in A;

              thus thesis

              proof

                per cases ;

                  suppose

                   A18: i in B;

                  reconsider xi = 0 , yi = 1 as Element of R by A3, TARSKI:def 2;

                  take xi, yi;

                  thus R = (XB . i) by A15, FUNCOP_1: 7;

                  thus xi = (( chi (A,X)) . i) by A15, A17, FUNCT_3:def 3;

                  thus yi = (( chi (B,X)) . i) by A15, A18, FUNCT_3:def 3;

                  xi c= yi;

                  hence xi <= yi by YELLOW_1: 2;

                end;

                  suppose

                   A19: not i in B;

                  reconsider xi = 0 , yi = 0 as Element of R by A3, TARSKI:def 2;

                  take xi, yi;

                  thus R = (XB . i) by A15, FUNCOP_1: 7;

                  thus xi = (( chi (A,X)) . i) by A15, A17, FUNCT_3:def 3;

                  thus yi = (( chi (B,X)) . i) by A15, A19, FUNCT_3:def 3;

                  thus xi <= yi;

                end;

              end;

            end;

          end;

          hence (f . A) <= (f . B) by A11, A13, YELLOW_1:def 4;

        end;

        assume (f . A) <= (f . B);

        then

        consider h1,h2 be Function such that

         A20: h1 = (f . A) and

         A21: h2 = (f . B) and

         A22: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (XB . i) & xi = (h1 . i) & yi = (h2 . i) & xi <= yi by A11, YELLOW_1:def 4;

        A c= B

        proof

          let i be object;

          assume

           A23: i in A;

          then

          consider R be RelStr, xi,yi be Element of R such that

           A24: R = (XB . 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 { 0 }) 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 ;

            then { 0 } c= 0 by A29, A28, YELLOW_1: 2, CARD_1: 49;

            hence thesis;

          end;

          

           A31: R = ( BoolePoset { 0 }) 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 thesis by FUNCT_3: 36;

        end;

        hence thesis by YELLOW_1: 2;

      end;

      ( product ( Carrier XB)) c= ( rng f)

      proof

        let z be object;

        assume z in ( product ( Carrier XB));

        then

        consider g be Function such that

         A32: z = g and

         A33: ( dom g) = ( dom ( Carrier XB)) and

         A34: for y be object st y in ( dom ( Carrier XB)) holds (g . y) in (( Carrier XB) . y) by CARD_3:def 5;

        set A = (g " {1});

        

         A35: A c= X

        proof

          let a be object;

          assume a in A;

          then a in ( dom g) by FUNCT_1:def 7;

          hence thesis by A33;

        end;

        

         A36: ( dom ( chi (A,X))) = X by FUNCT_3:def 3

        .= ( dom g) by A33, PARTFUN1:def 2;

        for a be object st a in ( dom ( chi (A,X))) holds (( chi (A,X)) . a) = (g . a)

        proof

          let a be object;

          assume

           A37: a in ( dom ( chi (A,X)));

          then a in X;

          then a in ( dom ( Carrier XB)) by PARTFUN1:def 2;

          then

           A38: (g . a) in (( Carrier XB) . a) by A34;

          ex R be 1-sorted st R = (XB . a) & (( Carrier XB) . a) = the carrier of R by A37, PRALG_1:def 15;

          then (( Carrier XB) . a) = { 0 , 1} by A3, A37, FUNCOP_1: 7;

          then

           A39: (g . a) = 0 or (g . a) = 1 by A38, TARSKI:def 2;

          per cases ;

            suppose a in A;

            then (( chi (A,X)) . a) = 1 & (g . a) in {1} by A37, FUNCT_1:def 7, FUNCT_3:def 3;

            hence thesis by TARSKI:def 1;

          end;

            suppose

             A40: not a in A;

            (g . a) <> 1

            proof

              assume (g . a) = 1;

              then (g . a) in {1} by TARSKI:def 1;

              hence thesis by A36, A37, A40, FUNCT_1:def 7;

            end;

            hence thesis by A37, A39, A40, FUNCT_3:def 3;

          end;

        end;

        

        then z = ( chi (A,X)) by A32, A36, FUNCT_1: 2

        .= (f . A) by A2, A35;

        hence thesis by A1, A35, FUNCT_1:def 3;

      end;

      then

       A41: ( rng f) = the carrier of ( product XB) by A11;

      take f;

      for A,B be Element of ( BoolePoset X) st (f . A) = (f . B) holds A = B

      proof

        let A,B be Element of ( BoolePoset X);

        assume

         A42: (f . A) = (f . B);

        (f . A) = ( chi (A,X)) & (f . B) = ( chi (B,X)) by A10, A2;

        hence thesis by A10, A42, FUNCT_3: 38;

      end;

      then f is one-to-one;

      hence f is isomorphic by A41, A12, WAYBEL_0: 66;

      thus thesis by A2;

    end;

    theorem :: WAYBEL18:15

    

     Th15: for I be non empty set holds for T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 }))) holds the topology of T = the topology of ( product (I --> Sierpinski_Space ))

    proof

      let I be non empty set;

      set IB = (I --> ( BoolePoset { 0 })), IS = (I --> Sierpinski_Space );

      

       A1: the carrier of ( product IB) = ( product ( Carrier IB)) by YELLOW_1:def 4;

      ( LattPOSet ( BooleLatt { 0 })) = RelStr (# the carrier of ( BooleLatt { 0 }), ( LattRel ( BooleLatt { 0 })) #) by LATTICE3:def 2;

      

      then

       A2: the carrier of ( BoolePoset { 0 }) = the carrier of ( BooleLatt { 0 }) by YELLOW_1:def 2

      .= ( bool { {} }) by LATTICE3:def 1

      .= { 0 , 1} by CARD_1: 49, ZFMISC_1: 24;

      

       A3: for i be object st i in ( dom ( Carrier IB)) holds (( Carrier IB) . i) = (( Carrier IS) . i)

      proof

        let i be object;

        assume i in ( dom ( Carrier IB));

        then

         A4: i in I;

        then

        consider R1 be 1-sorted such that

         A5: R1 = (IB . i) and

         A6: (( Carrier IB) . i) = the carrier of R1 by PRALG_1:def 15;

        consider R2 be 1-sorted such that

         A7: R2 = (IS . i) and

         A8: (( Carrier IS) . i) = the carrier of R2 by A4, PRALG_1:def 15;

        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 thesis by A6, A8;

      end;

      reconsider P = the set of all ( product (( Carrier IS) +* (ii, {1}))) where ii be Element of I as prebasis of ( product (I --> Sierpinski_Space )) by Th13;

      let T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 })));

      

       A9: ( dom ( Carrier IB)) = I by PARTFUN1:def 2

      .= ( dom ( Carrier IS)) by PARTFUN1:def 2;

      reconsider T9 = T as complete Scott TopLattice;

      

       A10: the RelStr of T = ( product (I --> ( BoolePoset { 0 }))) by YELLOW_9:def 4;

      then T9 is algebraic by WAYBEL_8: 17;

      then

      consider R be Basis of T9 such that

       A11: R = { ( uparrow yy) where yy be Element of T9 : yy in the carrier of ( CompactSublatt T9) } by WAYBEL14: 42;

      

       A12: the carrier of T = ( product ( Carrier (I --> ( BoolePoset { 0 })))) 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 be Function of ( BoolePoset I), ( product IB) such that

       A13: f is isomorphic and

       A14: for Y be Subset of I holds (f . Y) = ( chi (Y,I)) by Th14;

      

       A15: ( Carrier IB) = ( Carrier IS) by A9, A3, FUNCT_1: 2;

      

       A16: ( FinMeetCl P) c= R

      proof

        deffunc F( object) = ( product (( Carrier IS) +* ($1, {1})));

        let X be object;

        consider F be Function such that

         A17: ( dom F) = I and

         A18: for e be object st e in I holds (F . e) = F(e) from FUNCT_1:sch 3;

        assume

         A19: X in ( FinMeetCl P);

        then

        reconsider X9 = X as Subset of ( product IS);

        consider ZZ be Subset-Family of ( product IS) 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 object;

          assume w in P;

          then

          consider e be Element of I such that

           A23: w = ( product (( Carrier IS) +* (e, {1})));

          w = (F . e) by A18, A23;

          hence thesis by A17, FUNCT_1:def 3;

        end;

        then ZZ c= ( rng F) by A20;

        then

        consider x9 be 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 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 IB);

        set PP = { ( product (( Carrier IS) +* (i, {1}))) where i be Element of I : i in x9 };

        

         A27: ZZ c= PP

        proof

          let w be object;

          assume w in ZZ;

          then

          consider e be object 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 as Element of I by A17, A28;

          w = ( product (( Carrier IS) +* (e, {1}))) by A18, A30;

          hence thesis by A29;

        end;

        PP c= ZZ

        proof

          let w be object;

          assume w in PP;

          then

          consider e be Element of I such that

           A31: w = ( product (( Carrier IS) +* (e, {1}))) and

           A32: e in x9;

          w = (F . e) by A18, A31;

          hence thesis by A17, A26, A32, FUNCT_1:def 6;

        end;

        then

         A33: ZZ = PP by A27;

        

         A34: ( uparrow y) c= X9

        proof

          let z be object;

          assume

           A35: z in ( uparrow y);

          then

          reconsider z9 = z as Element of ( product IB);

          y <= z9 by A35, WAYBEL_0: 18;

          then

          consider h1,h2 be Function such that

           A36: h1 = y and

           A37: h2 = z9 and

           A38: for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (IB . i) & xi = (h1 . i) & yi = (h2 . i) & xi <= yi by A1, YELLOW_1:def 4;

          z in the carrier of ( product IB) by A35;

          then z in ( product ( Carrier IB)) by YELLOW_1:def 4;

          then

           A39: ex gg be Function st z = gg & ( dom gg) = ( dom ( Carrier IB)) & for w be object st w in ( dom ( Carrier IB)) holds (gg . w) in (( Carrier IB) . w) by CARD_3:def 5;

          

           A40: h1 = ( chi (x,I)) by A14, A36;

          for Z be set st Z in ZZ holds z in Z

          proof

            let Z be set;

            assume Z in ZZ;

            then

            consider j be Element of I such that

             A41: Z = ( product (( Carrier IS) +* (j, {1}))) and

             A42: j in x by A33;

            consider RS be RelStr, xj,yj be Element of RS such that

             A43: RS = (IB . j) and

             A44: xj = (h1 . j) and

             A45: yj = (h2 . j) and

             A46: xj <= yj by A38;

            

             A47: RS = ( BoolePoset { 0 }) by A43;

            

             A48: xj = 1 by A40, A42, A44, FUNCT_3:def 3;

            

             A49: yj <> 0

            proof

              assume yj = 0 ;

              then { 0 } c= 0 by A46, A48, A47, YELLOW_1: 2, CARD_1: 49;

              hence thesis;

            end;

            reconsider b = yj as Element of ( BoolePoset { 0 }) by A43;

            

             A50: ( dom (( Carrier IS) +* (j, {1}))) = ( dom ( Carrier IS)) by FUNCT_7: 30

            .= I by PARTFUN1:def 2;

            

             A51: b in the carrier of ( BoolePoset { 0 });

            

             A52: for w be object st w in ( dom (( Carrier IS) +* (j, {1}))) holds (h2 . w) in ((( Carrier IS) +* (j, {1})) . w)

            proof

              let w be object;

              assume w in ( dom (( Carrier IS) +* (j, {1})));

              then

               A53: w in ( dom ( Carrier IS)) by A50, PARTFUN1:def 2;

              per cases ;

                suppose w = j;

                then ((( Carrier IS) +* (j, {1})) . w) = {1} & (h2 . w) = 1 by A2, A45, A51, A49, A53, FUNCT_7: 31, TARSKI:def 2;

                hence thesis by TARSKI:def 1;

              end;

                suppose w <> j;

                then ((( Carrier IS) +* (j, {1})) . w) = (( Carrier IS) . w) by FUNCT_7: 32;

                hence thesis by A15, A39, A37, A53;

              end;

            end;

            ( dom h2) = ( dom (( Carrier IS) +* (j, {1}))) by A39, A37, A50, PARTFUN1:def 2;

            hence thesis by A37, A41, A52, CARD_3:def 5;

          end;

          hence thesis by A10, A12, A22, A35, SETFAM_1: 43;

        end;

        

         A54: X9 c= ( uparrow y)

        proof

          set h1 = ( chi (x,I));

          let z be object;

          assume

           A55: z in X9;

          then

          reconsider z9 = z as Element of ( product IB) by A10, A12;

          z in the carrier of ( product IB) by A10, A12, A55;

          then z in ( product ( Carrier IB)) by YELLOW_1:def 4;

          then

          consider h2 be Function such that

           A56: z = h2 and ( dom h2) = ( dom ( Carrier IB)) and

           A57: for w be object st w in ( dom ( Carrier IB)) holds (h2 . w) in (( Carrier IB) . w) by CARD_3:def 5;

          

           A58: for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (IB . i) & xi = (h1 . i) & yi = (h2 . i) & xi <= yi

          proof

            let i be object;

            assume

             A59: i in I;

            then

            reconsider i9 = i as Element of I;

            ex RB be 1-sorted st RB = (IB . i) & (( Carrier IB) . i) = the carrier of RB by A59, PRALG_1:def 15;

            then

             A60: (( Carrier IB) . i) = { 0 , 1} by A2, A59, FUNCOP_1: 7;

            take RS = ( BoolePoset { 0 });

            

             A61: i in ( dom ( Carrier IB)) by A59, PARTFUN1:def 2;

            then

             A62: (h2 . i) in (( Carrier IB) . i) by A57;

            per cases ;

              suppose

               A63: i in x;

              reconsider xi = 1, yi = 1 as Element of RS by A2, TARSKI:def 2;

              take xi, yi;

              thus RS = (IB . i) by A59, FUNCOP_1: 7;

              thus xi = (h1 . i) by A63, FUNCT_3:def 3;

              

               A64: ((( Carrier IS) +* (i9, {1})) . i9) = {1} by A9, A61, FUNCT_7: 31;

              ( product (( Carrier IS) +* (i9, {1}))) in ZZ by A33, A63;

              then z in ( product (( Carrier IS) +* (i9, {1}))) by A22, A55, SETFAM_1: 43;

              then

              consider h29 be Function such that

               A65: z = h29 and ( dom h29) = ( dom (( Carrier IS) +* (i9, {1}))) and

               A66: for w be object st w in ( dom (( Carrier IS) +* (i9, {1}))) holds (h29 . w) in ((( Carrier IS) +* (i9, {1})) . w) by CARD_3:def 5;

              i9 in ( dom (( Carrier IS) +* (i9, {1}))) by A9, A61, FUNCT_7: 30;

              then (h29 . i9) in ((( Carrier IS) +* (i9, {1})) . i9) by A66;

              hence yi = (h2 . i) by A56, A65, A64, TARSKI:def 1;

              thus xi <= yi;

            end;

              suppose

               A67: not i in x;

              thus thesis

              proof

                per cases by A60, A62, TARSKI:def 2;

                  suppose

                   A68: (h2 . i) = 0 ;

                  reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def 2;

                  take xi, yi;

                  thus RS = (IB . i) by A59, FUNCOP_1: 7;

                  thus xi = (h1 . i) by A59, A67, FUNCT_3:def 3;

                  thus yi = (h2 . i) by A68;

                  thus xi <= yi;

                end;

                  suppose

                   A69: (h2 . i) = 1;

                  reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def 2;

                  take xi, yi;

                  thus RS = (IB . i) by A59, FUNCOP_1: 7;

                  thus xi = (h1 . i) by A59, A67, FUNCT_3:def 3;

                  thus yi = (h2 . i) by A69;

                  xi c= yi;

                  hence xi <= yi by YELLOW_1: 2;

                end;

              end;

            end;

          end;

          h1 = y by A14;

          then y <= z9 by A1, A56, A58, YELLOW_1:def 4;

          hence thesis by WAYBEL_0: 18;

        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 thesis by A11, A70;

      end;

      

       A71: ( rng f) = the carrier of ( product IB) by A13, WAYBEL_0: 66;

      R c= ( FinMeetCl P)

      proof

        deffunc F( Element of I) = ( product (( Carrier IS) +* ($1, {1})));

        let X be object;

        assume

         A72: X in R;

        then

        consider Y be 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 IS) by A12, A72;

        reconsider y = Y as Element of ( product IB) by A10;

        consider x be object such that

         A75: x in ( dom f) and

         A76: y = (f . x) by A71, FUNCT_1:def 3;

        reconsider 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: { F(jj) where jj be Element of I : jj in x } is finite from FRAENKEL:sch 21( A77);

        set ZZ = { ( product (( Carrier IS) +* (jj, {1}))) where jj be Element of I : jj in x };

        reconsider x9 = x as Subset of I by WAYBEL_8: 26;

        

         A79: ZZ c= P

        proof

          let z be object;

          assume z in ZZ;

          then ex j be Element of I st z = ( product (( Carrier IS) +* (j, {1}))) & j in x9;

          hence thesis;

        end;

        then

        reconsider ZZ as Subset-Family of ( product IS) 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 object;

          assume

           A82: z in ( Intersect ZZ);

          then

          reconsider z9 = z as Element of ( product IB) by A10, A12;

          z in the carrier of ( product IB) by A10, A12, A82;

          then z in ( product ( Carrier IB)) by YELLOW_1:def 4;

          then

          consider h2 be Function such that

           A83: z = h2 and ( dom h2) = ( dom ( Carrier IB)) and

           A84: for w be object st w in ( dom ( Carrier IB)) holds (h2 . w) in (( Carrier IB) . w) by CARD_3:def 5;

          

           A85: for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (IB . i) & xi = (h1 . i) & yi = (h2 . i) & xi <= yi

          proof

            let i be object;

            assume

             A86: i in I;

            then

            reconsider i9 = i as Element of I;

            ex RB be 1-sorted st RB = (IB . i) & (( Carrier IB) . i) = the carrier of RB by A86, PRALG_1:def 15;

            then

             A87: (( Carrier IB) . i) = { 0 , 1} by A2, A86, FUNCOP_1: 7;

            take RS = ( BoolePoset { 0 });

            

             A88: i in ( dom ( Carrier IB)) by A86, PARTFUN1:def 2;

            then

             A89: (h2 . i) in (( Carrier IB) . i) by A84;

            per cases ;

              suppose

               A90: i in x;

              reconsider xi = 1, yi = 1 as Element of RS by A2, TARSKI:def 2;

              take xi, yi;

              thus RS = (IB . i) by A86, FUNCOP_1: 7;

              thus xi = (h1 . i) by A86, A90, FUNCT_3:def 3;

              

               A91: ((( Carrier IS) +* (i9, {1})) . i9) = {1} by A9, A88, FUNCT_7: 31;

              ( product (( Carrier IS) +* (i9, {1}))) in ZZ by A90;

              then z in ( product (( Carrier IS) +* (i9, {1}))) by A82, SETFAM_1: 43;

              then

              consider h29 be Function such that

               A92: z = h29 and ( dom h29) = ( dom (( Carrier IS) +* (i9, {1}))) and

               A93: for w be object st w in ( dom (( Carrier IS) +* (i9, {1}))) holds (h29 . w) in ((( Carrier IS) +* (i9, {1})) . w) by CARD_3:def 5;

              i9 in ( dom (( Carrier IS) +* (i9, {1}))) by A9, A88, FUNCT_7: 30;

              then (h29 . i9) in ((( Carrier IS) +* (i9, {1})) . i9) by A93;

              hence yi = (h2 . i) by A83, A92, A91, TARSKI:def 1;

              thus xi <= yi;

            end;

              suppose

               A94: not i in x;

              thus thesis

              proof

                per cases by A87, A89, TARSKI:def 2;

                  suppose

                   A95: (h2 . i) = 0 ;

                  reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def 2;

                  take xi, yi;

                  thus RS = (IB . i) by A86, FUNCOP_1: 7;

                  thus xi = (h1 . i) by A86, A94, FUNCT_3:def 3;

                  thus yi = (h2 . i) by A95;

                  thus xi <= yi;

                end;

                  suppose

                   A96: (h2 . i) = 1;

                  reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def 2;

                  take xi, yi;

                  thus RS = (IB . i) by A86, FUNCOP_1: 7;

                  thus xi = (h1 . i) by A86, A94, FUNCT_3:def 3;

                  thus yi = (h2 . i) by A96;

                  xi c= yi;

                  hence xi <= yi by YELLOW_1: 2;

                end;

              end;

            end;

          end;

          h1 = (f . x9) by A14

          .= y by A76;

          then y <= z9 by A1, A83, A85, YELLOW_1:def 4;

          hence thesis by A73, A80, WAYBEL_0: 18;

        end;

        X9 c= ( Intersect ZZ)

        proof

          let z be object;

          assume

           A97: z in X9;

          then

          reconsider z9 = z as Element of ( product IB) by A10, A12;

          y <= z9 by A73, A80, A97, WAYBEL_0: 18;

          then

          consider h1,h2 be Function such that

           A98: h1 = y and

           A99: h2 = z9 and

           A100: for i be object st i in I holds ex R be RelStr, xi,yi be Element of R st R = (IB . i) & xi = (h1 . i) & yi = (h2 . i) & xi <= yi by A1, YELLOW_1:def 4;

          z in the carrier of ( product IB) by A10, A12, A97;

          then z in ( product ( Carrier IB)) by YELLOW_1:def 4;

          then

           A101: ex gg be Function st z = gg & ( dom gg) = ( dom ( Carrier IB)) & for w be object st w in ( dom ( Carrier IB)) holds (gg . w) in (( Carrier IB) . w) by CARD_3:def 5;

          

           A102: h1 = (f . x9) by A76, A98

          .= ( chi (x,I)) by A14;

          for Z be set st Z in ZZ holds z in Z

          proof

            let Z be set;

            assume Z in ZZ;

            then

            consider j be Element of I such that

             A103: Z = ( product (( Carrier IS) +* (j, {1}))) and

             A104: j in x;

            consider RS be RelStr, xj,yj be Element of RS such that

             A105: RS = (IB . 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 { 0 }) by A105;

            

             A109: a <= b by A105, A108;

            

             A110: xj = 1 by A102, A104, A106, FUNCT_3:def 3;

            

             A111: yj <> 0

            proof

              assume yj = 0 ;

              then { 0 } c= 0 by A110, A109, YELLOW_1: 2, CARD_1: 49;

              hence thesis;

            end;

            

             A112: ( dom (( Carrier IS) +* (j, {1}))) = ( dom ( Carrier IS)) by FUNCT_7: 30

            .= I by PARTFUN1:def 2;

            

             A113: b in the carrier of ( BoolePoset { 0 });

            

             A114: for w be object st w in ( dom (( Carrier IS) +* (j, {1}))) holds (h2 . w) in ((( Carrier IS) +* (j, {1})) . w)

            proof

              let w be object;

              assume w in ( dom (( Carrier IS) +* (j, {1})));

              then

               A115: w in ( dom ( Carrier IS)) by A112, PARTFUN1:def 2;

              per cases ;

                suppose w = j;

                then ((( Carrier IS) +* (j, {1})) . w) = {1} & (h2 . w) = 1 by A2, A107, A113, A111, A115, FUNCT_7: 31, TARSKI:def 2;

                hence thesis by TARSKI:def 1;

              end;

                suppose w <> j;

                then ((( Carrier IS) +* (j, {1})) . w) = (( Carrier IS) . w) by FUNCT_7: 32;

                hence thesis by A15, A101, A99, A115;

              end;

            end;

            ( dom h2) = ( dom (( Carrier IS) +* (j, {1}))) by A101, A99, A112, PARTFUN1:def 2;

            hence thesis by A99, A103, A114, CARD_3:def 5;

          end;

          hence thesis by A97, SETFAM_1: 43;

        end;

        then X9 = ( Intersect ZZ) by A81;

        hence thesis by A79, A78, CANTOR_1:def 3;

      end;

      then R = ( FinMeetCl P) by A16;

      then P9 is prebasis of T by A12, YELLOW_9: 23;

      hence thesis by A12, YELLOW_9: 26;

    end;

    theorem :: WAYBEL18:16

    

     Th16: for T,S be 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;

      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;

      let X be non empty TopSpace;

      let f be Function of X, S;

      reconsider f9 = f as Function of X, T by A1;

      

       A4: ( [#] S) <> {} ;

      assume

       A5: f is continuous;

      

       A6: for P be Subset of T st P is open holds (f9 " P) is open

      proof

        let P be Subset of T;

        reconsider P9 = P as Subset of S by A1;

        assume P is open;

        then P9 in the topology of S by A2;

        then P9 is open;

        hence thesis by A4, A5, TOPS_2: 43;

      end;

      let Y be non empty TopSpace;

      assume

       A7: X is SubSpace of Y;

      

       A8: ( [#] T) <> {} ;

      then f9 is continuous by A6, TOPS_2: 43;

      then

      consider h be Function of Y, T such that

       A9: h is continuous and

       A10: (h | the carrier of X) = f9 by A3, A7;

      reconsider g = h as Function of Y, S by A1;

      take g;

      for P be Subset of S st P is open holds (g " P) is open

      proof

        let P be Subset of S;

        reconsider P9 = P as Subset of T by A1;

        assume P is open;

        then P9 in the topology of T by A2;

        then P9 is open;

        hence thesis by A8, A9, TOPS_2: 43;

      end;

      hence g is continuous by A4, TOPS_2: 43;

      thus thesis by A10;

    end;

    theorem :: WAYBEL18:17

    for I be non empty set holds for T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 }))) holds T is injective

    proof

      let I be non empty set, T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 })));

      set IB = (I --> ( BoolePoset { 0 })), IS = (I --> Sierpinski_Space );

      

       A1: ( dom ( Carrier IB)) = I by PARTFUN1:def 2

      .= ( dom ( Carrier IS)) by PARTFUN1:def 2;

      

       A2: the topology of T = the topology of ( product (I --> Sierpinski_Space )) by Th15;

      ( LattPOSet ( BooleLatt { 0 })) = RelStr (# the carrier of ( BooleLatt { 0 }), ( LattRel ( BooleLatt { 0 })) #) by LATTICE3:def 2;

      

      then

       A3: the carrier of ( BoolePoset { 0 }) = the carrier of ( BooleLatt { 0 }) by YELLOW_1:def 2

      .= ( bool { {} }) by LATTICE3:def 1

      .= { 0 , 1} by CARD_1: 49, ZFMISC_1: 24;

      

       A4: for i be object st i in ( dom ( Carrier IB)) holds (( Carrier IB) . i) = (( Carrier IS) . i)

      proof

        let i be object;

        assume i in ( dom ( Carrier IB));

        then

         A5: i in I;

        then

        consider R1 be 1-sorted such that

         A6: R1 = (IB . i) and

         A7: (( Carrier IB) . i) = the carrier of R1 by PRALG_1:def 15;

        consider R2 be 1-sorted such that

         A8: R2 = (IS . i) and

         A9: (( Carrier IS) . i) = the carrier of R2 by A5, PRALG_1:def 15;

        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 thesis by A7, A9;

      end;

      for i be Element of I holds ((I --> Sierpinski_Space ) . i) is injective;

      then

       A10: ( product (I --> Sierpinski_Space )) is injective by Th7;

       the RelStr of T = ( product (I --> ( BoolePoset { 0 }))) by YELLOW_9:def 4;

      

      then the carrier of T = ( product ( Carrier (I --> ( BoolePoset { 0 })))) 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 thesis by A2, A10, Th16;

    end;

    theorem :: WAYBEL18:18

    

     Th18: for T be T_0-TopSpace holds ex M be non empty set, f be Function of T, ( product (M --> Sierpinski_Space )) st ( corestr f) is being_homeomorphism

    proof

      let T be T_0-TopSpace;

      take M = the carrier of ( InclPoset the topology of T);

      set J = (M --> Sierpinski_Space );

      reconsider PP = the set of all ( product (( Carrier J) +* (m, {1}))) where m be Element of M as prebasis of ( product J) by Th13;

      deffunc F( object) = ( chi ({ u where u be Subset of T : $1 in u & u is open },the topology of T));

      consider f be Function such that

       A1: ( dom f) = the carrier of T and

       A2: for x be object st x in the carrier of T holds (f . x) = F(x) from FUNCT_1:sch 3;

      ( rng f) c= the carrier of ( product J)

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        set ch = ( chi ({ u where u be Subset of T : x in u & u is open },the topology of T));

        

         A4: ( dom ch) = the topology of T by FUNCT_3:def 3

        .= M by YELLOW_1: 1

        .= ( dom ( Carrier J)) by PARTFUN1:def 2;

        

         A5: for z be object st z in ( dom ( Carrier J)) holds (ch . z) in (( Carrier J) . z)

        proof

          let z be object;

          assume z in ( dom ( Carrier J));

          then

           A6: z in M;

          then z in the topology of T by YELLOW_1: 1;

          then z in ( dom ch) by FUNCT_3:def 3;

          then

           A7: (ch . z) in ( rng ch) by FUNCT_1:def 3;

          ex R be 1-sorted st R = (J . z) & (( Carrier J) . z) = the carrier of R by A6, PRALG_1:def 15;

          

          then (( Carrier J) . z) = the carrier of Sierpinski_Space by A6, FUNCOP_1: 7

          .= { 0 , 1} by Def9;

          hence thesis by A7;

        end;

        y = ch by A1, A2, A3;

        then y in ( product ( Carrier J)) by A4, A5, CARD_3:def 5;

        hence thesis by Def3;

      end;

      then

      reconsider f as Function of T, ( product J) by A1, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      

       A8: ( rng ( corestr f)) = ( [#] ( Image f)) by FUNCT_2:def 3;

      for A be Subset of ( product J) 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 J);

        reconsider a = A as Subset of ( product ( Carrier J)) by Def3;

        assume A in PP;

        then

        consider i be Element of M such that

         A9: a = ( product (( Carrier J) +* (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 J)) by A10, PARTFUN1:def 2;

        

         A13: i c= (f " A)

        proof

          let z be object;

          assume

           A14: z in i;

          set W = { u where u be Subset of T : z in u & u is open };

          i9 is open by A11;

          then

           A15: i in W by A14;

          

           A16: for w be object st w in ( dom (( Carrier J) +* (i,V))) holds (( chi (W,the topology of T)) . w) in ((( Carrier J) +* (i,V)) . w)

          proof

            let w be object;

            assume w in ( dom (( Carrier J) +* (i,V)));

            then w in ( dom ( Carrier J)) 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 (W,the topology of T))) by FUNCT_3:def 3;

            per cases ;

              suppose w = i;

              then ((( Carrier J) +* (i,V)) . w) = {1} & (( chi (W,the topology of T)) . w) = 1 by A11, A12, A15, FUNCT_3:def 3, FUNCT_7: 31;

              hence thesis by TARSKI:def 1;

            end;

              suppose

               A19: w <> i;

              

               A20: (( chi (W,the topology of T)) . w) in ( rng ( chi (W,the topology of T))) by A18, FUNCT_1:def 3;

              ex r be 1-sorted st r = (J . w) & (( Carrier J) . w) = the carrier of r by A17, PRALG_1:def 15;

              

              then

               A21: (( Carrier J) . w) = the carrier of Sierpinski_Space by A17, FUNCOP_1: 7

              .= { 0 , 1} by Def9;

              ((( Carrier J) +* (i,V)) . w) = (( Carrier J) . w) by A19, FUNCT_7: 32;

              hence thesis by A21, A20;

            end;

          end;

          

           A22: ( dom ( chi (W,the topology of T))) = the topology of T by FUNCT_3:def 3

          .= M by YELLOW_1: 1

          .= ( dom ( Carrier J)) by PARTFUN1:def 2

          .= ( dom (( Carrier J) +* (i,V))) by FUNCT_7: 30;

          

           A23: z in i9 by A14;

          then (f . z) = ( chi (W,the topology of T)) by A2;

          then (f . z) in A by A9, A22, A16, CARD_3:def 5;

          hence thesis by A1, A23, FUNCT_1:def 7;

        end;

        

         A24: ((( Carrier J) +* (i,V)) . i) = {1} by A12, FUNCT_7: 31;

        (f " A) c= i

        proof

          let z be object;

          set W = { u where u be Subset of T : z in u & u is open };

          assume z in (f " A);

          then (f . z) in a & (f . z) = ( chi (W,the topology of T)) by A2, FUNCT_1:def 7;

          then

          consider g be Function such that

           A25: ( chi (W,the topology of T)) = g and ( dom g) = ( dom (( Carrier J) +* (i,V))) and

           A26: for w be object st w in ( dom (( Carrier J) +* (i,V))) holds (g . w) in ((( Carrier J) +* (i,V)) . w) by A9, CARD_3:def 5;

          i in ( dom (( Carrier J) +* (i,V))) by A12, FUNCT_7: 30;

          then (g . i) in ((( Carrier J) +* (i,V)) . i) by A26;

          then (( chi (W,the topology of T)) . i) = 1 by A24, A25, TARSKI:def 1;

          then i in W by FUNCT_3: 36;

          then ex uu be Subset of T st i = uu & z in uu & uu is open;

          hence thesis;

        end;

        then (f " A) = i by A13;

        hence thesis by A11;

      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;

        set U1 = { u where u be Subset of T : x in u & u is open };

        set U2 = { u where u be Subset of T : y in u & u is open };

        assume

         A29: (( corestr f) . x) = (( corestr f) . y);

        thus x = y

        proof

          

           A30: (f . x) = ( chi (U1,the topology of T)) & (f . y) = ( chi (U2,the topology of T)) by A2;

          assume not thesis;

          then

          consider V be 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;

          per cases by A32;

            suppose

             A34: x in V & not y in V;

            reconsider v = V as Subset of T;

            

             A35: not v in U2

            proof

              assume not thesis;

              then ex u be Subset of T st u = v & y in u & u is open;

              hence thesis by A34;

            end;

            v in U1 by A31, A34;

            then (( chi (U1,the topology of T)) . v) = 1 by A33, FUNCT_3:def 3;

            hence thesis by A29, A30, A33, A35, FUNCT_3:def 3;

          end;

            suppose

             A36: y in V & not x in V;

            reconsider v = V as Subset of T;

            

             A37: not v in U1

            proof

              assume not thesis;

              then ex u be Subset of T st u = v & x in u & u is open;

              hence thesis by A36;

            end;

            v in U2 by A31, A36;

            then (( chi (U2,the topology of T)) . v) = 1 by A33, FUNCT_3:def 3;

            hence thesis by A29, A30, A33, A37, FUNCT_3:def 3;

          end;

        end;

      end;

      

       A38: for V be Subset of T st V is open holds (f .: V) = (( product (( Carrier J) +* (V, {1}))) /\ the carrier of ( Image f))

      proof

        let V be Subset of T;

        assume

         A39: V is open;

        hereby

          let y be object;

          assume y in (f .: V);

          then

          consider x be object 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 be Subset of T : x in u & u is open };

          

           A44: V in Q by A39, A41;

          

           A45: for W be object st W in ( dom (( Carrier J) +* (V, {1}))) holds (( chi (Q,the topology of T)) . W) in ((( Carrier J) +* (V, {1})) . W)

          proof

            let W be object;

            assume W in ( dom (( Carrier J) +* (V, {1})));

            then

             A46: W in ( dom ( Carrier J)) 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 (Q,the topology of T))) by FUNCT_3:def 3;

            per cases ;

              suppose W = V;

              then ((( Carrier J) +* (V, {1})) . W) = {1} & (( chi (Q,the topology of T)) . W) = 1 by A44, A46, A48, FUNCT_3:def 3, FUNCT_7: 31;

              hence thesis by TARSKI:def 1;

            end;

              suppose

               A50: W <> V;

              

               A51: (( chi (Q,the topology of T)) . W) in ( rng ( chi (Q,the topology of T))) by A49, FUNCT_1:def 3;

              ex r be 1-sorted st r = (J . W) & (( Carrier J) . W) = the carrier of r by A47, PRALG_1:def 15;

              

              then

               A52: (( Carrier J) . W) = the carrier of Sierpinski_Space by A47, FUNCOP_1: 7

              .= { 0 , 1} by Def9;

              ((( Carrier J) +* (V, {1})) . W) = (( Carrier J) . W) by A50, FUNCT_7: 32;

              hence thesis by A52, A51;

            end;

          end;

          

           A53: ( dom ( chi (Q,the topology of T))) = the topology of T by FUNCT_3:def 3

          .= M by YELLOW_1: 1

          .= ( dom ( Carrier J)) by PARTFUN1:def 2

          .= ( dom (( Carrier J) +* (V, {1}))) by FUNCT_7: 30;

          y = ( chi (Q,the topology of T)) by A2, A40, A42;

          then y in ( product (( Carrier J) +* (V, {1}))) by A53, A45, CARD_3:def 5;

          hence y in (( product (( Carrier J) +* (V, {1}))) /\ the carrier of ( Image f)) by A43, XBOOLE_0:def 4;

        end;

        let y be object;

        assume

         A54: y in (( product (( Carrier J) +* (V, {1}))) /\ the carrier of ( Image f));

        then y in ( product (( Carrier J) +* (V, {1}))) by XBOOLE_0:def 4;

        then

        consider g be Function such that

         A55: y = g and ( dom g) = ( dom (( Carrier J) +* (V, {1}))) and

         A56: for W be object st W in ( dom (( Carrier J) +* (V, {1}))) holds (g . W) in ((( Carrier J) +* (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 be object such that

         A57: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        V in the topology of T by A39;

        then V in M by YELLOW_1: 1;

        then

         A58: V in ( dom ( Carrier J)) by PARTFUN1:def 2;

        then V in ( dom (( Carrier J) +* (V, {1}))) by FUNCT_7: 30;

        then (g . V) in ((( Carrier J) +* (V, {1})) . V) by A56;

        then

         A59: (g . V) in {1} by A58, FUNCT_7: 31;

        set Q = { u where u be Subset of T : x in u & u is open };

        y = ( chi (Q,the topology of T)) by A2, A57;

        then (( chi (Q,the topology of T)) . V) = 1 by A55, A59, TARSKI:def 1;

        then V in Q by FUNCT_3: 36;

        then ex u be Subset of T st u = V & x in u & u is open;

        hence thesis by A57, FUNCT_1:def 6;

      end;

      

       A60: for V be Subset of T st V is open holds ((( corestr f) " ) " V) is open

      proof

        let V be Subset of T;

        

         A61: PP c= the topology of ( product J) by TOPS_2: 64;

        assume

         A62: V is open;

        then V in the topology of T;

        then

        reconsider W = V as Element of M by YELLOW_1: 1;

        

         A63: ( product (( Carrier J) +* (W, {1}))) in PP;

        then

        reconsider Q = ( product (( Carrier J) +* (V, {1}))) as Subset of ( product J);

        (( 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;

        hence thesis by A8, A28, TOPS_2: 54;

      end;

      ( [#] T) <> {} ;

      then (( corestr f) " ) is continuous by A60, TOPS_2: 43;

      hence thesis by A8, A28, A27, TOPS_2:def 5;

    end;

    theorem :: WAYBEL18:19

    for T be T_0-TopSpace st T is injective holds ex M be non empty set st T is_Retract_of ( product (M --> Sierpinski_Space ))

    proof

      let T be T_0-TopSpace;

      assume

       A1: T is injective;

      ex M be non empty set, f be Function of T, ( product (M --> Sierpinski_Space )) st ( corestr f) is being_homeomorphism by Th18;

      hence thesis by A1, Th11;

    end;