yellow17.miz



    begin

    theorem :: YELLOW17:1

    

     Th1: for F be Function, i,xi be set, Ai be Subset of (F . i) holds (( proj (F,i)) " {xi}) meets (( proj (F,i)) " Ai) implies xi in Ai

    proof

      let F be Function, i be set, xi be set, Ai be Subset of (F . i);

      set f = the Element of ((( proj (F,i)) " {xi}) /\ (( proj (F,i)) " Ai));

      assume

       A1: ((( proj (F,i)) " {xi}) /\ (( proj (F,i)) " Ai)) <> {} ;

      then f in (( proj (F,i)) " {xi}) by XBOOLE_0:def 4;

      then (( proj (F,i)) . f) in {xi} by FUNCT_1:def 7;

      then

       A2: (( proj (F,i)) . f) = xi by TARSKI:def 1;

      f in (( proj (F,i)) " Ai) by A1, XBOOLE_0:def 4;

      hence thesis by A2, FUNCT_1:def 7;

    end;

    theorem :: YELLOW17:2

    

     Th2: for F,f be Function, i,xi be set st xi in (F . i) & f in ( product F) holds (f +* (i,xi)) in ( product F)

    proof

      let F,f be Function, i,xi be set;

      assume

       A1: xi in (F . i);

      assume

       A2: f in ( product F);

      

       A3: for x be object st x in ( dom F) holds ((f +* (i,xi)) . x) in (F . x)

      proof

        let x be object;

        assume

         A4: x in ( dom F);

        per cases ;

          suppose

           A5: i = x;

          thus ((f +* (i,xi)) . x) in (F . x)

          proof

            per cases ;

              suppose i in ( dom f);

              hence thesis by A1, A5, FUNCT_7: 31;

            end;

              suppose not i in ( dom f);

              then (f +* (i,xi)) = f by FUNCT_7:def 3;

              hence thesis by A2, A4, CARD_3: 9;

            end;

          end;

        end;

          suppose i <> x;

          then ((f +* (i,xi)) . x) = (f . x) by FUNCT_7: 32;

          hence thesis by A2, A4, CARD_3: 9;

        end;

      end;

      ( dom f) = ( dom F) by A2, CARD_3: 9;

      then ( dom (f +* (i,xi))) = ( dom F) by FUNCT_7: 30;

      hence thesis by A3, CARD_3: 9;

    end;

    theorem :: YELLOW17:3

    

     Th3: for F be Function, i be set st i in ( dom F) holds ( rng ( proj (F,i))) c= (F . i) & (( product F) <> {} implies ( rng ( proj (F,i))) = (F . i))

    proof

      let F be Function, i be set;

      assume

       A1: i in ( dom F);

      thus

       A2: ( rng ( proj (F,i))) c= (F . i)

      proof

        let x be object;

        assume x in ( rng ( proj (F,i)));

        then

        consider f9 be object such that

         A3: f9 in ( dom ( proj (F,i))) and

         A4: x = (( proj (F,i)) . f9) by FUNCT_1:def 3;

        f9 in ( product F) by A3;

        then

        consider f be Function such that

         A5: f9 = f and ( dom f) = ( dom F) and

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

        (( proj (F,i)) . f) = (f . i) by A3, A5, CARD_3:def 16;

        hence thesis by A1, A4, A5, A6;

      end;

      assume

       A7: ( product F) <> {} ;

      thus ( rng ( proj (F,i))) c= (F . i) by A2;

      let x be object;

      set f9 = the Element of ( product F);

      consider f be Function such that

       A8: f9 = f and

       A9: ( dom f) = ( dom F) and for x be object st x in ( dom F) holds (f . x) in (F . x) by A7, CARD_3:def 5;

      assume x in (F . i);

      then (f +* (i,x)) in ( product F) by A7, A8, Th2;

      then

       A10: (f +* (i,x)) in ( dom ( proj (F,i))) by CARD_3:def 16;

      ((f +* (i,x)) . i) = x by A1, A9, FUNCT_7: 31;

      then (( proj (F,i)) . (f +* (i,x))) = x by A10, CARD_3:def 16;

      hence thesis by A10, FUNCT_1:def 3;

    end;

    theorem :: YELLOW17:4

    

     Th4: for F be Function, i be set st i in ( dom F) holds (( proj (F,i)) " (F . i)) = ( product F)

    proof

      let F be Function, i be set;

      assume

       A1: i in ( dom F);

      ( dom ( proj (F,i))) = ( product F) by CARD_3:def 16;

      hence (( proj (F,i)) " (F . i)) c= ( product F) by RELAT_1: 132;

      let f9 be object;

      assume

       A2: f9 in ( product F);

      then

      consider f be Function such that

       A3: f9 = f and ( dom f) = ( dom F) and

       A4: for x be object st x in ( dom F) holds (f . x) in (F . x) by CARD_3:def 5;

      

       A5: f in ( dom ( proj (F,i))) by A2, A3, CARD_3:def 16;

      (f . i) in (F . i) by A1, A4;

      then (( proj (F,i)) . f) in (F . i) by A5, CARD_3:def 16;

      hence thesis by A3, A5, FUNCT_1:def 7;

    end;

    theorem :: YELLOW17:5

    

     Th5: for F,f be Function, i,xi be set st xi in (F . i) & i in ( dom F) & f in ( product F) holds (f +* (i,xi)) in (( proj (F,i)) " {xi})

    proof

      let F,f be Function, i,xi be set;

      assume that

       A1: xi in (F . i) and

       A2: i in ( dom F) and

       A3: f in ( product F);

      (f +* (i,xi)) in ( product F) by A1, A3, Th2;

      then

       A4: (f +* (i,xi)) in ( dom ( proj (F,i))) by CARD_3:def 16;

      i in ( dom f) by A2, A3, CARD_3: 9;

      then ((f +* (i,xi)) . i) = xi by FUNCT_7: 31;

      then ((f +* (i,xi)) . i) in {xi} by TARSKI:def 1;

      then (( proj (F,i)) . (f +* (i,xi))) in {xi} by A4, CARD_3:def 16;

      hence thesis by A4, FUNCT_1:def 7;

    end;

    

     Lm1: for F,g be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2) st i1 <> i2 & g in ( product F) holds (g +* (i1,xi1)) in (( proj (F,i2)) " Ai2) implies g in (( proj (F,i2)) " Ai2)

    proof

      let F,g be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2);

      assume that

       A1: i1 <> i2 and

       A2: g in ( product F);

      

       A3: g in ( dom ( proj (F,i2))) by A2, CARD_3:def 16;

      assume (g +* (i1,xi1)) in (( proj (F,i2)) " Ai2);

      then (g +* (i1,xi1)) in ( dom ( proj (F,i2))) & (( proj (F,i2)) . (g +* (i1,xi1))) in Ai2 by FUNCT_1:def 7;

      then ((g +* (i1,xi1)) . i2) in Ai2 by CARD_3:def 16;

      then (g . i2) in Ai2 by A1, FUNCT_7: 32;

      then (( proj (F,i2)) . g) in Ai2 by A3, CARD_3:def 16;

      hence thesis by A3, FUNCT_1:def 7;

    end;

    theorem :: YELLOW17:6

    

     Th6: for F,f be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2) st xi1 in (F . i1) & f in ( product F) holds i1 <> i2 implies (f in (( proj (F,i2)) " Ai2) iff (f +* (i1,xi1)) in (( proj (F,i2)) " Ai2))

    proof

      let F,f be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2);

      assume that

       A1: xi1 in (F . i1) and

       A2: f in ( product F);

      assume

       A3: i1 <> i2;

      thus f in (( proj (F,i2)) " Ai2) implies (f +* (i1,xi1)) in (( proj (F,i2)) " Ai2)

      proof

        

         A4: ((f +* (i1,xi1)) +* (i1,(f . i1))) = (f +* (i1,(f . i1))) by FUNCT_7: 34

        .= f by FUNCT_7: 35;

        assume f in (( proj (F,i2)) " Ai2);

        hence thesis by A1, A2, A3, A4, Lm1, Th2;

      end;

      assume (f +* (i1,xi1)) in (( proj (F,i2)) " Ai2);

      hence thesis by A2, A3, Lm1;

    end;

    theorem :: YELLOW17:7

    

     Th7: for F be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2) st ( product F) <> {} & xi1 in (F . i1) & i1 in ( dom F) & i2 in ( dom F) & Ai2 <> (F . i2) holds (( proj (F,i1)) " {xi1}) c= (( proj (F,i2)) " Ai2) iff i1 = i2 & xi1 in Ai2

    proof

      let F be Function, i1,i2,xi1 be set, Ai2 be Subset of (F . i2);

      assume that

       A1: ( product F) <> {} and

       A2: xi1 in (F . i1) and

       A3: i1 in ( dom F) and

       A4: i2 in ( dom F) and

       A5: Ai2 <> (F . i2);

      set f9 = the Element of ( product F);

      consider f be Function such that

       A6: f9 = f and

       A7: ( dom f) = ( dom F) and for x be object st x in ( dom F) holds (f . x) in (F . x) by A1, CARD_3:def 5;

       not (F . i2) c= Ai2 by A5;

      then

      consider xi2 be object such that

       A8: xi2 in (F . i2) and

       A9: not xi2 in Ai2;

      reconsider xi2 as Element of (F . i2) by A8;

      

       A10: ((f +* (i2,xi2)) . i2) = xi2 by A4, A7, FUNCT_7: 31;

      thus (( proj (F,i1)) " {xi1}) c= (( proj (F,i2)) " Ai2) implies i1 = i2 & xi1 in Ai2

      proof

        assume

         A11: (( proj (F,i1)) " {xi1}) c= (( proj (F,i2)) " Ai2);

        thus

         A12: i1 = i2

        proof

          assume

           A13: i1 <> i2;

          (f +* (i2,xi2)) in ( product F) & ((f +* (i2,xi2)) +* (i1,xi1)) in (( proj (F,i1)) " {xi1}) by A1, A2, A3, A8, A6, Th2, Th5;

          then (f +* (i2,xi2)) in (( proj (F,i2)) " Ai2) by A2, A11, A13, Th6;

          then (f +* (i2,xi2)) in ( dom ( proj (F,i2))) & (( proj (F,i2)) . (f +* (i2,xi2))) in Ai2 by FUNCT_1:def 7;

          hence contradiction by A9, A10, CARD_3:def 16;

        end;

        xi1 in ( rng ( proj (F,i1))) by A1, A2, A3, Th3;

        then {xi1} c= ( rng ( proj (F,i1))) by ZFMISC_1: 31;

        then {xi1} c= Ai2 by A11, A12, FUNCT_1: 88;

        hence thesis by ZFMISC_1: 31;

      end;

      assume that

       A14: i1 = i2 and

       A15: xi1 in Ai2;

       {xi1} c= Ai2 by A15, ZFMISC_1: 31;

      hence thesis by A14, RELAT_1: 143;

    end;

    scheme :: YELLOW17:sch1

    ElProductEx { I() -> non empty set , J() -> TopStruct-yielding non-Empty ManySortedSet of I() , P[ object, object] } :

ex f be Element of ( product J()) st for i be Element of I() holds P[(f . i), i]

      provided

       A1: for i be Element of I() holds ex x be Element of (J() . i) st P[x, i];

      defpred Q[ object, object] means P[$2, $1] & for i9 be Element of I() st $1 = i9 holds $2 in the carrier of (J() . i9);

      

       A2: for i be object st i in I() holds ex x be object st Q[i, x]

      proof

        let i be object;

        assume i in I();

        then

        reconsider i1 = i as Element of I();

        consider x be Element of (J() . i1) such that

         A3: P[x, i1] by A1;

        take x;

        thus P[x, i] by A3;

        let i9 be Element of I();

        assume i = i9;

        hence thesis;

      end;

      consider f be Function such that

       A4: ( dom f) = I() and

       A5: for i be object st i in I() holds Q[i, (f . i)] from CLASSES1:sch 1( A2);

      

       A6: for x be object st x in ( dom ( Carrier J())) holds (f . x) in (( Carrier J()) . x)

      proof

        let x be object;

        assume x in ( dom ( Carrier J()));

        then

        reconsider x9 = x as Element of I();

        (f . x9) in the carrier of (J() . x9) by A5;

        hence thesis by YELLOW_6: 2;

      end;

      ( dom f) = ( dom ( Carrier J())) by A4, PARTFUN1:def 2;

      then f in ( product ( Carrier J())) by A6, CARD_3: 9;

      then

      reconsider f as Element of ( product J()) by WAYBEL18:def 3;

      take f;

      let i be Element of I();

      thus thesis by A5;

    end;

    theorem :: YELLOW17:8

    

     Th8: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, f be Element of ( product J) holds (( proj (J,i)) . f) = (f . i)

    proof

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

      f in the carrier of ( product J);

      then f in ( product ( Carrier J)) by WAYBEL18:def 3;

      then f in ( dom ( proj (( Carrier J),i))) by CARD_3:def 16;

      then (( proj (( Carrier J),i)) . f) = (f . i) by CARD_3:def 16;

      hence thesis by WAYBEL18:def 4;

    end;

    theorem :: YELLOW17:9

    

     Th9: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, xi be Element of (J . i), Ai be Subset of (J . i) holds (( proj (J,i)) " {xi}) meets (( proj (J,i)) " Ai) implies xi in Ai

    proof

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

      assume ((( proj (J,i)) " {xi}) /\ (( proj (J,i)) " Ai)) <> {} ;

      then ((( proj (( Carrier J),i)) " {xi}) /\ (( proj (J,i)) " Ai)) <> {} by WAYBEL18:def 4;

      then ((( proj (( Carrier J),i)) " {xi}) /\ (( proj (( Carrier J),i)) " Ai)) <> {} by WAYBEL18:def 4;

      then

       A1: (( proj (( Carrier J),i)) " {xi}) meets (( proj (( Carrier J),i)) " Ai);

      Ai c= the carrier of (J . i);

      then Ai c= (( Carrier J) . i) by YELLOW_6: 2;

      hence thesis by A1, Th1;

    end;

    theorem :: YELLOW17:10

    

     Th10: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I holds (( proj (J,i)) " ( [#] (J . i))) = ( [#] ( product J))

    proof

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

      i in I;

      then i in ( dom ( Carrier J)) by PARTFUN1:def 2;

      then (( proj (( Carrier J),i)) " (( Carrier J) . i)) = ( product ( Carrier J)) by Th4;

      then (( proj (( Carrier J),i)) " (( Carrier J) . i)) = ( [#] ( product J)) by WAYBEL18:def 3;

      then (( proj (( Carrier J),i)) " ( [#] (J . i))) = ( [#] ( product J)) by YELLOW_6: 2;

      hence thesis by WAYBEL18:def 4;

    end;

    theorem :: YELLOW17:11

    

     Th11: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, xi be Element of (J . i), f be Element of ( product J) holds (f +* (i,xi)) in (( proj (J,i)) " {xi})

    proof

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

      xi in the carrier of (J . i);

      then

       A1: xi in (( Carrier J) . i) by YELLOW_6: 2;

      f in the carrier of ( product J);

      then

       A2: f in ( product ( Carrier J)) by WAYBEL18:def 3;

      i in I;

      then i in ( dom ( Carrier J)) by PARTFUN1:def 2;

      then (f +* (i,xi)) in (( proj (( Carrier J),i)) " {xi}) by A1, A2, Th5;

      hence thesis by WAYBEL18:def 4;

    end;

    theorem :: YELLOW17:12

    

     Th12: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i1,i2 be Element of I, xi1 be Element of (J . i1), Ai2 be Subset of (J . i2) st Ai2 <> ( [#] (J . i2)) holds (( proj (J,i1)) " {xi1}) c= (( proj (J,i2)) " Ai2) iff i1 = i2 & xi1 in Ai2

    proof

      let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i1,i2 be Element of I, xi1 be Element of (J . i1), Ai2 be Subset of (J . i2);

      reconsider Ai29 = Ai2 as Subset of (( Carrier J) . i2) by YELLOW_6: 2;

      i2 in I;

      then

       A1: i2 in ( dom ( Carrier J)) by PARTFUN1:def 2;

      assume Ai2 <> ( [#] (J . i2));

      then

       A2: Ai29 <> (( Carrier J) . i2) by YELLOW_6: 2;

      xi1 in the carrier of (J . i1);

      then

       A3: xi1 in (( Carrier J) . i1) by YELLOW_6: 2;

      i1 in I;

      then ( product ( Carrier J)) <> {} & i1 in ( dom ( Carrier J)) by PARTFUN1:def 2;

      then (( proj (( Carrier J),i1)) " {xi1}) c= (( proj (( Carrier J),i2)) " Ai29) iff i1 = i2 & xi1 in Ai29 by A1, A3, A2, Th7;

      then (( proj (J,i1)) " {xi1}) c= (( proj (( Carrier J),i2)) " Ai2) iff i1 = i2 & xi1 in Ai29 by WAYBEL18:def 4;

      hence thesis by WAYBEL18:def 4;

    end;

    theorem :: YELLOW17:13

    

     Th13: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i1,i2 be Element of I, xi1 be Element of (J . i1), Ai2 be Subset of (J . i2), f be Element of ( product J) st i1 <> i2 holds f in (( proj (J,i2)) " Ai2) iff (f +* (i1,xi1)) in (( proj (J,i2)) " Ai2)

    proof

      let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i1,i2 be Element of I, xi1 be Element of (J . i1), Ai2 be Subset of (J . i2), f be Element of ( product J);

      reconsider Ai29 = Ai2 as Subset of (( Carrier J) . i2) by YELLOW_6: 2;

      xi1 in the carrier of (J . i1);

      then

       A1: xi1 in (( Carrier J) . i1) by YELLOW_6: 2;

      f in the carrier of ( product J);

      then

       A2: f in ( product ( Carrier J)) by WAYBEL18:def 3;

      assume i1 <> i2;

      then f in (( proj (( Carrier J),i2)) " Ai29) iff (f +* (i1,xi1)) in (( proj (( Carrier J),i2)) " Ai29) by A1, A2, Th6;

      hence thesis by WAYBEL18:def 4;

    end;

    begin

    theorem :: YELLOW17:14

    

     Th14: for T be non empty TopStruct holds T is compact iff for F be Subset-Family of T st F is open & ( [#] T) c= ( union F) holds ex G be Subset-Family of T st G c= F & ( [#] T) c= ( union G) & G is finite

    proof

      let T be non empty TopStruct;

      thus T is compact implies for F be Subset-Family of T st F is open & ( [#] T) c= ( union F) holds ex G be Subset-Family of T st G c= F & ( [#] T) c= ( union G) & G is finite

      proof

        assume

         A1: T is compact;

        let F be Subset-Family of T;

        assume that

         A2: F is open and

         A3: ( [#] T) c= ( union F);

        F is Cover of T by A3, TOPMETR: 1;

        then

        consider G be Subset-Family of T such that

         A4: G c= F & G is Cover of T & G is finite by A1, A2;

        take G;

        thus thesis by A4, TOPMETR: 1;

      end;

      assume

       A5: for F be Subset-Family of T st F is open & ( [#] T) c= ( union F) holds ex G be Subset-Family of T st G c= F & ( [#] T) c= ( union G) & G is finite;

      let F be Subset-Family of T;

      assume that

       A6: F is Cover of T and

       A7: F is open;

      ( [#] T) c= ( union F) by A6, TOPMETR: 1;

      then

      consider G be Subset-Family of T such that

       A8: G c= F & ( [#] T) c= ( union G) & G is finite by A5, A7;

      take G;

      thus thesis by A8, TOPMETR: 1;

    end;

    theorem :: YELLOW17:15

    

     Th15: for T be non empty TopSpace, B be prebasis of T holds T is compact iff for F be Subset of B st ( [#] T) c= ( union F) holds ex G be finite Subset of F st ( [#] T) c= ( union G)

    proof

      let T be non empty TopSpace, B be prebasis of T;

      set x = the carrier of T;

      the carrier of T in the topology of T by PRE_TOPC:def 1;

      then

      reconsider x as Element of ( InclPoset the topology of T) by YELLOW_1: 1;

      x is compact iff x << x by WAYBEL_3:def 2;

      hence thesis by WAYBEL_3: 37, WAYBEL_7: 31;

    end;

    begin

    theorem :: YELLOW17:16

    

     Th16: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, A be set st A in ( product_prebasis J) holds ex i be Element of I, Ai be Subset of (J . i) st Ai is open & (( proj (J,i)) " Ai) = A

    proof

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

      assume A in ( product_prebasis J);

      then

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

       A1: i in I and

       A2: Ai is open and

       A3: T = (J . i) and

       A4: A = ( product (( Carrier J) +* (i,Ai))) by WAYBEL18:def 2;

      reconsider i as Element of I by A1;

      reconsider Ai as Subset of (J . i) by A3;

      take i;

      take Ai;

      thus Ai is open by A2, A3;

      thus thesis by A4, WAYBEL18: 4;

    end;

    theorem :: YELLOW17:17

    

     Th17: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, xi be Element of (J . i), A be set st A in ( product_prebasis J) & (( proj (J,i)) " {xi}) c= A holds A = ( [#] ( product J)) or ex Ai be Subset of (J . i) st Ai <> ( [#] (J . i)) & xi in Ai & Ai is open & A = (( proj (J,i)) " Ai)

    proof

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

      assume A in ( product_prebasis J);

      then

      consider i1 be Element of I, Ai1 be Subset of (J . i1) such that

       A1: Ai1 is open and

       A2: (( proj (J,i1)) " Ai1) = A by Th16;

      assume

       A3: (( proj (J,i)) " {xi}) c= A;

      assume not A = ( [#] ( product J));

      then

       A4: Ai1 <> ( [#] (J . i1)) by A2, Th10;

      then

      reconsider Ai = Ai1 as Subset of (J . i) by A3, A2, Th12;

      take Ai;

      thus Ai <> ( [#] (J . i)) by A3, A2, A4, Th12;

      thus xi in Ai by A3, A2, A4, Th12;

      (J . i) = (J . i1) by A3, A2, A4, Th12;

      hence Ai is open by A1;

      thus thesis by A3, A2, A4, Th12;

    end;

    theorem :: YELLOW17:18

    

     Th18: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, Fi be non empty Subset-Family of (J . i) st ( [#] (J . i)) c= ( union Fi) holds ( [#] ( product J)) c= ( union the set of all (( proj (J,i)) " Ai) where Ai be Element of Fi)

    proof

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

      assume

       A1: ( [#] (J . i)) c= ( union Fi);

      let f be object;

      assume

       A2: f in ( [#] ( product J));

      then

      reconsider f9 = f as Element of ( product J);

      (f9 . i) in ( [#] (J . i));

      then

      consider Ai0 be set such that

       A3: (f9 . i) in Ai0 and

       A4: Ai0 in Fi by A1, TARSKI:def 4;

      f9 in ( product ( Carrier J)) by A2, WAYBEL18:def 3;

      then f9 in ( dom ( proj (( Carrier J),i))) by CARD_3:def 16;

      then

       A5: f9 in ( dom ( proj (J,i))) by WAYBEL18:def 4;

      reconsider Ai0 as Element of Fi by A4;

      (( proj (J,i)) . f9) in Ai0 by A3, Th8;

      then (( proj (J,i)) " Ai0) in the set of all (( proj (J,i)) " Ai) where Ai be Element of Fi & f9 in (( proj (J,i)) " Ai0) by A5, FUNCT_1:def 7;

      hence thesis by TARSKI:def 4;

    end;

    theorem :: YELLOW17:19

    

     Th19: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, xi be Element of (J . i), G be Subset of ( product_prebasis J) st (( proj (J,i)) " {xi}) c= ( union G) & (for A be set st A in ( product_prebasis J) & A in G holds not (( proj (J,i)) " {xi}) c= A) holds ( [#] ( product J)) c= ( union G)

    proof

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

      assume that

       A1: (( proj (J,i)) " {xi}) c= ( union G) and

       A2: for A be set st A in ( product_prebasis J) & A in G holds not (( proj (J,i)) " {xi}) c= A;

      let f be object;

      assume f in ( [#] ( product J));

      then

      reconsider f9 = f as Element of ( product J);

      set g = (f9 +* (i,xi));

      

       A3: g in (( proj (J,i)) " {xi}) by Th11;

      then

      consider Ag be set such that

       A4: g in Ag and

       A5: Ag in G by A1, TARSKI:def 4;

      consider i2 be Element of I, Ai2 be Subset of (J . i2) such that Ai2 is open and

       A6: (( proj (J,i2)) " Ai2) = Ag by A5, Th16;

      

       A7: Ai2 <> ( [#] (J . i2))

      proof

        assume Ai2 = ( [#] (J . i2));

        

        then (( proj (J,i2)) " Ai2) = ( [#] ( product J)) by Th10

        .= the carrier of ( product J);

        hence contradiction by A2, A5, A6;

      end;

      

       A8: not (( proj (J,i)) " {xi}) c= (( proj (J,i2)) " Ai2) by A2, A5, A6;

      i <> i2

      proof

        assume

         A9: i = i2;

        then

        reconsider Ai29 = Ai2 as Subset of (J . i);

        ((( proj (J,i)) " {xi}) /\ (( proj (J,i)) " Ai29)) <> {} by A3, A4, A6, A9, XBOOLE_0:def 4;

        then

         A10: (( proj (J,i)) " {xi}) meets (( proj (J,i)) " Ai29);

         not xi in Ai2 by A8, A7, A9, Th12;

        hence contradiction by A10, Th9;

      end;

      then f in (( proj (J,i2)) " Ai2) by A4, A6, Th13;

      hence thesis by A5, A6, TARSKI:def 4;

    end;

    theorem :: YELLOW17:20

    

     Th20: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, F be Subset of ( product_prebasis J) holds (for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G)) implies for xi be Element of (J . i), G be finite Subset of F st (( proj (J,i)) " {xi}) c= ( union G) holds ex A be set st A in ( product_prebasis J) & A in G & (( proj (J,i)) " {xi}) c= A

    proof

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

      assume

       A1: for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G);

      let xi be Element of (J . i), G be finite Subset of F;

      reconsider G9 = G as Subset of ( product_prebasis J) by XBOOLE_1: 1;

      assume

       A2: (( proj (J,i)) " {xi}) c= ( union G);

      assume for A be set st A in ( product_prebasis J) & A in G holds not (( proj (J,i)) " {xi}) c= A;

      then ( [#] ( product J)) c= ( union G9) by A2, Th19;

      hence contradiction by A1;

    end;

    theorem :: YELLOW17:21

    

     Th21: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, F be Subset of ( product_prebasis J) holds (for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G)) implies for xi be Element of (J . i), G be finite Subset of F st (( proj (J,i)) " {xi}) c= ( union G) holds ex Ai be Subset of (J . i) st Ai <> ( [#] (J . i)) & xi in Ai & (( proj (J,i)) " Ai) in G & Ai is open

    proof

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

      assume

       A1: for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G);

      let xi be Element of (J . i), G be finite Subset of F;

      assume (( proj (J,i)) " {xi}) c= ( union G);

      then

      consider A be set such that

       A2: A in ( product_prebasis J) and

       A3: A in G and

       A4: (( proj (J,i)) " {xi}) c= A by A1, Th20;

      A <> ( [#] ( product J))

      proof

        reconsider G1 = {A} as finite Subset of F by A3, ZFMISC_1: 31;

        assume A = ( [#] ( product J));

        then ( union G1) = ( [#] ( product J)) by ZFMISC_1: 25;

        hence contradiction by A1;

      end;

      then

      consider Ai be Subset of (J . i) such that

       A5: Ai <> ( [#] (J . i)) and

       A6: xi in Ai and

       A7: Ai is open and

       A8: A = (( proj (J,i)) " Ai) by A2, A4, Th17;

      take Ai;

      thus Ai <> ( [#] (J . i)) by A5;

      thus xi in Ai by A6;

      thus (( proj (J,i)) " Ai) in G by A3, A8;

      thus thesis by A7;

    end;

    theorem :: YELLOW17:22

    

     Th22: for I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I, i be Element of I, F be Subset of ( product_prebasis J) st (for i be Element of I holds (J . i) is compact) & (for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G)) holds ex xi be Element of (J . i) st for G be finite Subset of F holds not (( proj (J,i)) " {xi}) c= ( union G)

    proof

      defpred P[ set] means not contradiction;

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

      assume that

       A1: for i be Element of I holds (J . i) is compact and

       A2: for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G);

      deffunc F( set) = (( proj (J,i)) " $1);

      defpred P[ object, object] means ex A be set st A = $2 & $1 in A & (( proj (J,i)) " A) in F & for V be Subset of (J . i) st V = $2 holds V is open;

      assume

       A3: for xi be Element of (J . i) holds ex G be finite Subset of F st (( proj (J,i)) " {xi}) c= ( union G);

      

       A4: for xi be object st xi in the carrier of (J . i) holds ex Ai be object st Ai in ( bool the carrier of (J . i)) & P[xi, Ai]

      proof

        let xi be object;

        assume xi in the carrier of (J . i);

        then

        reconsider xi9 = xi as Element of (J . i);

        consider G be finite Subset of F such that

         A5: (( proj (J,i)) " {xi9}) c= ( union G) by A3;

        consider Ai be Subset of (J . i) such that Ai <> ( [#] (J . i)) and

         A6: xi in Ai and

         A7: (( proj (J,i)) " Ai) in G and

         A8: Ai is open by A2, A5, Th21;

        take Ai;

        thus Ai in ( bool the carrier of (J . i));

        take Ai;

        thus Ai = Ai;

        thus xi in Ai by A6;

        thus (( proj (J,i)) " Ai) in F by A7;

        let V be Subset of (J . i);

        assume V = Ai;

        hence thesis by A8;

      end;

      consider h be Function such that

       A9: ( dom h) = the carrier of (J . i) and

       A10: ( rng h) c= ( bool the carrier of (J . i)) and

       A11: for xi be object st xi in the carrier of (J . i) holds P[xi, (h . xi)] from FUNCT_1:sch 6( A4);

      reconsider bGip = ( rng h) as Subset-Family of (J . i) by A10;

      reconsider bGip as Subset-Family of (J . i);

      

       A12: ( [#] (J . i)) c= ( union bGip)

      proof

        let x be object;

        assume

         A13: x in ( [#] (J . i));

        then P[x, (h . x)] by A11;

        then

        consider A be set such that

         A14: A = (h . x) & x in A & (( proj (J,i)) " A) in F & for V be Subset of (J . i) st V = (h . x) holds V is open;

        x in (h . x) & (h . x) in bGip by A9, FUNCT_1:def 3, A14, A13;

        hence thesis by TARSKI:def 4;

      end;

      for P be Subset of (J . i) holds P in bGip implies P is open

      proof

        let P be Subset of (J . i);

        assume P in bGip;

        then

        consider x be object such that

         A15: x in ( dom h) & P = (h . x) by FUNCT_1:def 3;

         P[x, (h . x)] by A9, A11, A15;

        hence thesis by A15;

      end;

      then

       A16: bGip is open by TOPS_2:def 1;

      (J . i) is compact by A1;

      then

      consider Gip be Subset-Family of (J . i) such that

       A17: Gip c= bGip and

       A18: ( [#] (J . i)) c= ( union Gip) and

       A19: Gip is finite by A12, A16, Th14;

      reconsider Gip as non empty finite Subset-Family of (J . i) by A18, A19, ZFMISC_1: 2;

      set Gp = { F(Ai) where Ai be Element of Gip : P[Ai] };

      

       A20: Gp c= F

      proof

        let A be object;

        assume A in Gp;

        then

        consider Ai be Element of Gip such that

         A21: A = (( proj (J,i)) " Ai);

        Ai in Gip;

        then

        consider x be object such that

         A22: x in ( dom h) & (h . x) = Ai by A17, FUNCT_1:def 3;

         P[x, (h . x)] by A9, A11, A22;

        hence thesis by A21, A22;

      end;

      Gp is finite from PRE_CIRC:sch 1;

      then

      reconsider Gp as finite Subset of F by A20;

      ( [#] ( product J)) c= ( union Gp) by A18, Th18;

      hence contradiction by A2;

    end;

    ::$Notion-Name

    theorem :: YELLOW17:23

    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 compact holds ( product J) is compact

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

      reconsider B = ( product_prebasis J) as prebasis of ( product J) by WAYBEL18:def 3;

      assume not ( product J) is compact;

      then

      consider F be Subset of B such that

       A2: ( [#] ( product J)) c= ( union F) and

       A3: for G be finite Subset of F holds not ( [#] ( product J)) c= ( union G) by Th15;

      defpred P[ set, Element of I] means for G be finite Subset of F holds not (( proj (J,$2)) " {$1}) c= ( union G);

      

       A4: for i be Element of I holds ex xi be Element of (J . i) st P[xi, i] by A1, A3, Th22;

      consider f be Element of ( product J) such that

       A5: for i be Element of I holds P[(f . i), i] from ElProductEx( A4);

      f in ( [#] ( product J));

      then

      consider A be set such that

       A6: f in A and

       A7: A in F by A2, TARSKI:def 4;

      reconsider G = {A} as finite Subset of F by A7, ZFMISC_1: 31;

      consider i be Element of I, Ai be Subset of (J . i) such that Ai is open and

       A8: (( proj (J,i)) " Ai) = A by A7, Th16;

      (( proj (J,i)) . f) in Ai by A6, A8, FUNCT_1:def 7;

      then (f . i) in Ai by Th8;

      then {(f . i)} c= Ai by ZFMISC_1: 31;

      then (( proj (J,i)) " {(f . i)}) c= A by A8, RELAT_1: 143;

      then (( proj (J,i)) " {(f . i)}) c= ( union G) by ZFMISC_1: 25;

      hence contradiction by A5;

    end;