tops_5.miz



    begin

    theorem :: TOPS_5:1

    

     Th1: for f be one-to-one Function, y be object st ( rng f) = {y} holds ( dom f) = {((f " ) . y)}

    proof

      let f be one-to-one Function, y be object;

      assume

       A1: ( rng f) = {y};

      then y in ( rng f) by TARSKI:def 1;

      then

      consider x0 be object such that

       A2: x0 in ( dom f) & (f . x0) = y by FUNCT_1:def 3;

      for x be object holds x in ( dom f) iff x = ((f " ) . y)

      proof

        let x be object;

        hereby

          assume

           A3: x in ( dom f);

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

          then (f . x) = y by A1, TARSKI:def 1;

          hence x = ((f " ) . y) by A3, FUNCT_1: 34;

        end;

        assume x = ((f " ) . y);

        hence thesis by A2, FUNCT_1: 34;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TOPS_5:2

    

     Th2: for f be one-to-one Function, y1,y2 be object st ( rng f) = {y1, y2} holds ( dom f) = {((f " ) . y1), ((f " ) . y2)}

    proof

      let f be one-to-one Function, y1,y2 be object;

      assume

       A1: ( rng f) = {y1, y2};

      then

       A2: y1 in ( rng f) & y2 in ( rng f) by TARSKI:def 2;

      then

      consider x1 be object such that

       A3: x1 in ( dom f) & (f . x1) = y1 by FUNCT_1:def 3;

      consider x2 be object such that

       A4: x2 in ( dom f) & (f . x2) = y2 by A2, FUNCT_1:def 3;

      for x be object holds x in ( dom f) iff x = ((f " ) . y1) or x = ((f " ) . y2)

      proof

        let x be object;

        thus x in ( dom f) implies x = ((f " ) . y1) or x = ((f " ) . y2)

        proof

          assume

           A5: x in ( dom f);

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

          then (f . x) = y1 or (f . x) = y2 by A1, TARSKI:def 2;

          hence thesis by A5, FUNCT_1: 34;

        end;

        thus thesis by A3, A4, FUNCT_1: 34;

      end;

      hence thesis by TARSKI:def 2;

    end;

    registration

      let X,Y be set;

      cluster emptyX -definedY -valued one-to-one for Function;

      existence

      proof

        take f = the empty one-to-one Function;

        ( dom f) = {} & ( rng f) = {} ;

        hence thesis by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1: 2;

      end;

    end

    registration

      let T,S be set;

      let f be Function of T, S;

      let G be finite Subset-Family of T;

      cluster (f .: G) -> finite;

      coherence

      proof

        defpred P[ object, object] means ex A be Subset of T st $1 = A & $2 = (f .: A);

        

         A1: for x,y1,y2 be object st x in G & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A2: for x be object st x in G holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in G;

          then

          reconsider A = x as Subset of T;

          take (f .: A), A;

          thus thesis;

        end;

        consider g be Function such that

         A3: ( dom g) = G & for x be object st x in G holds P[x, (g . x)] from FUNCT_1:sch 2( A1, A2);

        for y be object holds y in ( rng g) iff y in (f .: G)

        proof

          let y be object;

          hereby

            assume y in ( rng g);

            then

            consider x be object such that

             A4: x in ( dom g) & (g . x) = y by FUNCT_1:def 3;

            ex A be Subset of T st x = A & y = (f .: A) by A3, A4;

            hence y in (f .: G) by A3, A4, FUNCT_2:def 10;

          end;

          assume

           A6: y in (f .: G);

          then

          reconsider B = y as Subset of S;

          consider A be Subset of T such that

           A7: A in G & B = (f .: A) by A6, FUNCT_2:def 10;

          ex A0 be Subset of T st A = A0 & (g . A) = (f .: A0) by A3, A7;

          hence thesis by A3, A7, FUNCT_1:def 3;

        end;

        then ( rng g) = (f .: G) by TARSKI: 2;

        hence thesis by A3, FINSET_1: 8;

      end;

    end

    theorem :: TOPS_5:3

    

     Th3: for A be set, F be Subset-Family of A, R be Relation holds (R .: ( meet F)) c= ( meet { (R .: X) where X be Subset of A : X in F })

    proof

      let A be set, F be Subset-Family of A, R be Relation;

      per cases ;

        suppose ( meet F) = {} ;

        then (R .: ( meet F)) = {} ;

        hence thesis by XBOOLE_1: 2;

      end;

        suppose ( meet F) <> {} ;

        then

        consider X0 be object such that

         A1: X0 in F by SETFAM_1: 1, XBOOLE_0:def 1;

        reconsider X0 as Subset of A by A1;

        

         A2: (R .: X0) in { (R .: X) where X be Subset of A : X in F } by A1;

        let y be object;

        assume y in (R .: ( meet F));

        then

        consider x be object such that

         A3: [x, y] in R & x in ( meet F) by RELAT_1:def 13;

        now

          let Y be set;

          assume Y in { (R .: X) where X be Subset of A : X in F };

          then

          consider X be Subset of A such that

           A4: Y = (R .: X) & X in F;

          x in X by A3, A4, SETFAM_1:def 1;

          hence y in Y by A3, A4, RELAT_1:def 13;

        end;

        hence y in ( meet { (R .: X) where X be Subset of A : X in F }) by A2, SETFAM_1:def 1;

      end;

    end;

    theorem :: TOPS_5:4

    

     Th4: for A be set, F be Subset-Family of A, f be one-to-one Function holds (f .: ( meet F)) = ( meet { (f .: X) where X be Subset of A : X in F })

    proof

      let A be set, F be Subset-Family of A, f be one-to-one Function;

      set S = { (f .: X) where X be Subset of A : X in F };

      

       A7: ( meet S) c= (f .: ( meet F))

      proof

        let y be object;

        assume

         A1: y in ( meet S);

        then

        consider z be object such that

         A2: z in S by XBOOLE_0:def 1, SETFAM_1: 1;

        consider X0 be Subset of A such that

         A3: z = (f .: X0) & X0 in F by A2;

        

         A4: y in (f .: X0) by A1, A2, A3, SETFAM_1:def 1;

        ex x be object st x in ( dom f) & x in ( meet F) & y = (f . x)

        proof

          consider x0 be object such that

           A5: x0 in ( dom f) & x0 in X0 & y = (f . x0) by A4, FUNCT_1:def 6;

          take x0;

          for X be set st X in F holds x0 in X

          proof

            let X be set;

            assume X in F;

            then (f .: X) in S;

            then y in (f .: X) by A1, SETFAM_1:def 1;

            then

            consider x be object such that

             A6: x in ( dom f) & x in X & y = (f . x) by FUNCT_1:def 6;

            thus thesis by A5, A6, FUNCT_1:def 4;

          end;

          hence thesis by A3, A5, SETFAM_1:def 1;

        end;

        hence thesis by FUNCT_1:def 6;

      end;

      (f .: ( meet F)) c= ( meet S) by Th3;

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: TOPS_5:5

    

     Th5: for X be set, Y be non empty set, f be Function of X, Y holds { (f " {y}) where y be Element of Y : y in ( rng f) } is a_partition of X

    proof

      let X be set, Y be non empty set, f be Function of X, Y;

      set P = { (f " {y}) where y be Element of Y : y in ( rng f) };

      for x be object holds x in X iff ex A be set st x in A & A in P

      proof

        let x be object;

        hereby

          assume

           A1: x in X;

          then

           A2: (f . x) in ( rng f) & (f . x) in Y by FUNCT_2: 4, FUNCT_2: 5;

          reconsider A = (f " {(f . x)}) as set;

          take A;

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

          hence x in A by A1, FUNCT_2: 38;

          thus A in P by A2;

        end;

        given A be set such that

         A3: x in A & A in P;

        consider y be Element of Y such that

         A4: (f " {y}) = A & y in ( rng f) by A3;

        thus x in X by A3, A4;

      end;

      then

       A5: ( union P) = X by TARSKI:def 4;

      

       A6: for A be Subset of X st A in P holds A <> {} & for B be Subset of X st B in P holds A = B or A misses B

      proof

        let A be Subset of X;

        assume A in P;

        then

        consider y1 be Element of Y such that

         A7: A = (f " {y1}) & y1 in ( rng f);

        consider x be object such that

         A8: x in X & y1 = (f . x) by A7, FUNCT_2: 11;

        (f . x) in {y1} by A8, TARSKI:def 1;

        hence A <> {} by A7, A8, FUNCT_2: 38;

        let B be Subset of X;

        assume B in P;

        then ex y2 be Element of Y st B = (f " {y2}) & y2 in ( rng f);

        hence thesis by A7, ZFMISC_1: 11, FUNCT_1: 71;

      end;

      P c= ( bool X)

      proof

        let x be object;

        assume x in P;

        then ex y be Element of Y st (f " {y}) = x & y in ( rng f);

        hence thesis;

      end;

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

    end;

    theorem :: TOPS_5:6

    for X be non empty set, x,y be object st (X --> x) = (X --> y) holds x = y

    proof

      let X be non empty set, x,y be object;

      assume

       A1: (X --> x) = (X --> y);

      ( rng (X --> x)) = {x} & ( rng (X --> y)) = {y} by FUNCOP_1: 8;

      hence thesis by A1, ZFMISC_1: 3;

    end;

    theorem :: TOPS_5:7

    

     Th7: for i be object, J be ManySortedSet of {i} holds J = ( {i} --> (J . i))

    proof

      let i be object, J be ManySortedSet of {i};

      

       A1: ( dom J) = {i} by PARTFUN1:def 2

      .= ( dom ( {i} --> (J . i)));

      for x be object st x in ( dom J) holds (J . x) = (( {i} --> (J . i)) . x)

      proof

        let x be object;

        assume x in ( dom J);

        then

         A2: x = i by TARSKI:def 1;

        (( {i} --> (J . i)) . i) = ((i .--> (J . i)) . i) by FUNCOP_1:def 9

        .= (J . i) by FUNCOP_1: 72;

        hence thesis by A2;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: TOPS_5:8

    

     Th8: for I be 2 -element set, i,j be Element of I st i <> j holds I = {i, j}

    proof

      let I be 2 -element set;

      let i,j be Element of I;

      assume

       A1: i <> j;

      for x be object holds x = i or x = j iff x in I

      proof

        let x be object;

        thus x = i or x = j implies x in I;

        assume

         A2: x in I;

        assume x <> i & x <> j;

        then

         A3: ( card {x, i, j}) = 3 by A1, CARD_2: 58;

         {x, i, j} c= I

        proof

          let z be object;

          assume z in {x, i, j};

          then z = x or z = i or z = j by ENUMSET1:def 1;

          hence thesis by A2;

        end;

        then ( card {x, i, j}) c= ( card I) by CARD_1: 11;

        then

         A4: { 0 , 1, 2} c= 2 by A3, CARD_1:def 7, CARD_1: 51;

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

        then 2 in 2 by A4;

        hence contradiction;

      end;

      hence I = {i, j} by TARSKI:def 2;

    end;

    theorem :: TOPS_5:9

    

     Th9: for I be 2 -element set, f be ManySortedSet of I holds for i,j be Element of I st i <> j holds f = ((i,j) --> ((f . i),(f . j)))

    proof

      let I be 2 -element set, f be ManySortedSet of I;

      let i,j be Element of I;

      assume

       A1: i <> j;

      ( dom f) = I by PARTFUN1:def 2

      .= {i, j} by A1, Th8;

      hence thesis by FUNCT_4: 66;

    end;

    theorem :: TOPS_5:10

    

     Th10: for a,b,c,d be object st a <> b holds ((a,b) --> (c,d)) = ((b,a) --> (d,c))

    proof

      let a,b,c,d be object;

      assume

       A1: a <> b;

      

       A2: ( dom ((a,b) --> (c,d))) = {a, b} by FUNCT_4: 62;

      then

       A3: ( dom ((a,b) --> (c,d))) = ( dom ((b,a) --> (d,c))) by FUNCT_4: 62;

      for x be object st x in ( dom ((a,b) --> (c,d))) holds (((a,b) --> (c,d)) . x) = (((b,a) --> (d,c)) . x)

      proof

        let x be object;

        assume x in ( dom ((a,b) --> (c,d)));

        per cases by A2, TARSKI:def 2;

          suppose

           A4: x = a;

          

          hence (((a,b) --> (c,d)) . x) = c by A1, FUNCT_4: 63

          .= (((b,a) --> (d,c)) . x) by A4, FUNCT_4: 63;

        end;

          suppose

           A5: x = b;

          

          hence (((a,b) --> (c,d)) . x) = d by FUNCT_4: 63

          .= (((b,a) --> (d,c)) . x) by A1, A5, FUNCT_4: 63;

        end;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: TOPS_5:11

    

     Th11: for f be Function, i,j be object st i in ( dom f) & j in ( dom f) holds f = (f +* ((i,j) --> ((f . i),(f . j))))

    proof

      let f be Function, i,j be object;

      assume

       A1: i in ( dom f) & j in ( dom f);

      

      thus f = (f +* (j .--> (f . j))) by A1, FUNCT_4: 7, LATTICE2: 5

      .= ((f +* (i .--> (f . i))) +* (j .--> (f . j))) by A1, FUNCT_4: 7, LATTICE2: 5

      .= (f +* ((i .--> (f . i)) +* (j .--> (f . j)))) by FUNCT_4: 14

      .= (f +* ((i,j) --> ((f . i),(f . j)))) by FUNCT_4:def 4;

    end;

    theorem :: TOPS_5:12

    

     Th12: for x,y,z be object holds ((x .--> y) +* (x .--> z)) = (x .--> z)

    proof

      let x,y,z be object;

      

       A1: ( dom (x .--> y)) = ( dom ( {x} --> y)) by FUNCOP_1:def 9

      .= {x};

      ( dom (x .--> z)) = ( dom ( {x} --> z)) by FUNCOP_1:def 9

      .= {x};

      hence thesis by A1, FUNCT_4: 19;

    end;

    registration

      cluster non non-empty for Function;

      existence

      proof

        take the empty-yielding ManySortedSet of the non empty set;

        thus thesis;

      end;

    end

    theorem :: TOPS_5:13

    

     Th13: for X,Y be non empty set, y be Element of Y holds (X --> y) in ( product (X --> Y))

    proof

      let X,Y be non empty set, y be Element of Y;

      set f = (X --> y);

      

       A1: ( dom f) = X

      .= ( dom (X --> Y));

      for x be object st x in ( dom (X --> Y)) holds (f . x) in ((X --> Y) . x)

      proof

        let x be object;

        assume

         A2: x in ( dom (X --> Y));

        then

         A3: ((X --> Y) . x) = Y by FUNCOP_1: 7;

        (f . x) = y by A2, FUNCOP_1: 7;

        hence thesis by A3;

      end;

      hence thesis by A1, CARD_3:def 5;

    end;

    theorem :: TOPS_5:14

    

     Th14: for X be non empty set, Y be set, Z be Subset of Y holds ( product (X --> Z)) c= ( product (X --> Y))

    proof

      let X be non empty set, Y be set, Z be Subset of Y;

      let x be object;

      assume x in ( product (X --> Z));

      then

      consider g be Function such that

       A1: x = g & ( dom g) = ( dom (X --> Z)) and

       A2: for y be object st y in ( dom (X --> Z)) holds (g . y) in ((X --> Z) . y) by CARD_3:def 5;

      now

        let y be object;

        assume

         a4: y in ( dom (X --> Y));

        then

         A4: y in X;

        

         A5: ((X --> Z) . y) = Z & ((X --> Y) . y) = Y by a4, FUNCOP_1: 7;

        y in ( dom (X --> Z)) by A4;

        then (g . y) in ((X --> Z) . y) by A2;

        hence (g . y) in ((X --> Y) . y) by A5;

      end;

      hence thesis by A1, CARD_3:def 5;

    end;

    theorem :: TOPS_5:15

    

     Th15: for X be non empty set, i be object holds ( product ( {i} --> X)) = { ( {i} --> x) where x be Element of X : not contradiction }

    proof

      let X be non empty set, i be object;

      set S = { ( {i} --> x) where x be Element of X : not contradiction };

      for z be object holds z in ( product ( {i} --> X)) iff z in S

      proof

        let z be object;

        hereby

          assume z in ( product ( {i} --> X));

          then

          consider f be Function such that

           A1: z = f & ( dom f) = ( dom ( {i} --> X)) and

           A2: for y be object st y in ( dom ( {i} --> X)) holds (f . y) in (( {i} --> X) . y) by CARD_3:def 5;

          

           A3: ( dom f) = {i} by A1;

          for y be object st y in ( dom f) holds (f . y) = (f . i) by A1, TARSKI:def 1;

          then

           A4: f = ( {i} --> (f . i)) by A3, FUNCOP_1: 11;

          i in ( dom ( {i} --> X)) by TARSKI:def 1;

          then (f . i) in (( {i} --> X) . i) by A2;

          then (f . i) in ((i .--> X) . i) by FUNCOP_1:def 9;

          then (f . i) in X by FUNCOP_1: 72;

          hence z in S by A1, A4;

        end;

        assume z in S;

        then ex x be Element of X st z = ( {i} --> x);

        hence thesis by Th13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_5:16

    

     Th16: for X be non empty set, i,f be object holds f in ( product ( {i} --> X)) iff ex x be Element of X st f = ( {i} --> x)

    proof

      let X be non empty set, i,f be object;

      hereby

        assume f in ( product ( {i} --> X));

        then f in { ( {i} --> x) where x be Element of X : not contradiction } by Th15;

        hence ex x be Element of X st f = ( {i} --> x);

      end;

      assume ex x be Element of X st f = ( {i} --> x);

      then f in { ( {i} --> x) where x be Element of X : not contradiction };

      hence thesis by Th15;

    end;

    theorem :: TOPS_5:17

    for X be non empty set, i be object, x be Element of X holds (( proj (( {i} --> X),i)) . ( {i} --> x)) = x

    proof

      let X be non empty set, i be object, x be Element of X;

      ( {i} --> x) in ( product ( {i} --> X)) by Th13;

      then ( {i} --> x) in ( dom ( proj (( {i} --> X),i))) by CARD_3:def 16;

      

      hence (( proj (( {i} --> X),i)) . ( {i} --> x)) = (( {i} --> x) . i) by CARD_3:def 16

      .= ((i .--> x) . i) by FUNCOP_1:def 9

      .= x by FUNCOP_1: 72;

    end;

    

     Lm1: for f be Function holds ( rng f) = { {} } implies ( product f) = {}

    proof

      let f be Function;

      assume ( rng f) = { {} };

      then {} in ( rng f) by TARSKI:def 1;

      hence thesis by CARD_3: 26;

    end;

    theorem :: TOPS_5:18

    for X,Y be set holds X <> {} & Y = {} iff ( product (X --> Y)) = {}

    proof

      let X,Y be set;

      hereby

        assume X <> {} & Y = {} ;

        then ( rng (X --> Y)) = { {} } by FUNCOP_1: 8;

        then {} in ( rng (X --> Y)) by TARSKI:def 1;

        hence ( product (X --> Y)) = {} by CARD_3: 26;

      end;

      assume ( product (X --> Y)) = {} ;

      hence thesis;

    end;

    registration

      let f be empty Function, x be object;

      cluster ( proj (f,x)) -> trivial;

      coherence

      proof

        ( dom ( proj (f,x))) = { {} } by CARD_3: 10, CARD_3:def 16;

        hence thesis;

      end;

    end

    theorem :: TOPS_5:19

    

     Th19: for f be trivial Function, x be object st x in ( dom f) holds ( proj (f,x)) is one-to-one

    proof

      let f be trivial Function, x be object;

      assume

       A1: x in ( dom f);

      then

      consider t be object such that

       A2: ( dom f) = {t} by ZFMISC_1: 131;

      

       A3: ( dom f) = {x} by A1, A2, TARSKI:def 1;

      set F = ( proj (f,x));

      for y,z be object st y in ( dom F) & z in ( dom F) & (F . y) = (F . z) holds y = z

      proof

        let y,z be object;

        assume

         A4: y in ( dom F) & z in ( dom F) & (F . y) = (F . z);

        then

        consider g be Function such that

         A5: y = g & ( dom g) = ( dom f) and for s be object st s in ( dom f) holds (g . s) in (f . s) by CARD_3:def 5;

        consider h be Function such that

         A6: z = h & ( dom h) = ( dom f) and for s be object st s in ( dom f) holds (h . s) in (f . s) by A4, CARD_3:def 5;

        

         A7: (g . x) = (F . z) by A4, A5, CARD_3:def 16

        .= (h . x) by A4, A6, CARD_3:def 16;

        for s be object st s in ( dom g) holds (g . s) = (h . s)

        proof

          let s be object;

          assume s in ( dom g);

          then s = x by A3, A5, TARSKI:def 1;

          hence thesis by A7;

        end;

        hence thesis by A5, A6, FUNCT_1: 2;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    registration

      let x,y be object;

      cluster ( proj ((x .--> y),x)) -> one-to-one;

      coherence

      proof

        x in {x} by TARSKI:def 1;

        then x in ( dom ( {x} --> y));

        then

         A1: x in ( dom (x .--> y)) by FUNCOP_1:def 9;

        x is set & y is set by TARSKI: 1;

        hence thesis by A1, Th19;

      end;

    end

    registration

      let I be 1 -element set, J be ManySortedSet of I, i be Element of I;

      cluster ( proj (J,i)) -> one-to-one;

      coherence

      proof

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

        then J is trivial & i in ( dom J);

        hence thesis by Th19;

      end;

    end

    theorem :: TOPS_5:20

    for X be non empty set, Y be Subset of X, i be object holds (( proj (( {i} --> X),i)) .: ( product ( {i} --> Y))) = Y

    proof

      let X be non empty set, Y be Subset of X, i be object;

      per cases ;

        suppose

         A1: Y is empty;

        then ( rng ( {i} --> Y)) = { {} } by FUNCOP_1: 8;

        then ( product ( {i} --> Y)) = {} by Lm1;

        hence thesis by A1;

      end;

        suppose

         A2: Y is non empty;

        for x be object holds x in (( proj (( {i} --> X),i)) .: ( product ( {i} --> Y))) iff x in Y

        proof

          let x be object;

          hereby

            assume x in (( proj (( {i} --> X),i)) .: ( product ( {i} --> Y)));

            then

            consider y be object such that

             A3: y in ( dom ( proj (( {i} --> X),i))) & y in ( product ( {i} --> Y)) and

             A4: x = (( proj (( {i} --> X),i)) . y) by FUNCT_1:def 6;

            consider z be Element of Y such that

             A5: y = ( {i} --> z) by A2, A3, Th16;

            reconsider y as Function by A5;

            x = (y . i) by A3, A4, CARD_3:def 16

            .= ((i .--> z) . i) by A5, FUNCOP_1:def 9

            .= z by FUNCOP_1: 72;

            hence x in Y by A2;

          end;

          assume x in Y;

          then

          reconsider z = x as Element of Y;

          ex y be object st y in ( dom ( proj (( {i} --> X),i))) & y in ( product ( {i} --> Y)) & x = (( proj (( {i} --> X),i)) . y)

          proof

            set y = ( {i} --> z);

            take y;

            y in ( product ( {i} --> Y)) by A2, Th13;

            then y in ( product ( {i} --> X)) by Th14, TARSKI:def 3;

            hence

             A7: y in ( dom ( proj (( {i} --> X),i))) & y in ( product ( {i} --> Y)) by A2, Th13, CARD_3:def 16;

            

            thus x = ((i .--> z) . i) by FUNCOP_1: 72

            .= (y . i) by FUNCOP_1:def 9

            .= (( proj (( {i} --> X),i)) . y) by A7, CARD_3:def 16;

          end;

          hence thesis by FUNCT_1:def 6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: TOPS_5:21

    

     Th21: for f,g be non-empty Function, i,x be object st x in (( product f) /\ ( product (f +* g))) holds (( proj (f,i)) . x) = (( proj ((f +* g),i)) . x)

    proof

      let f,g be non-empty Function, i,x be object;

      assume

       A1: x in (( product f) /\ ( product (f +* g)));

      then x in ( product f) by XBOOLE_0:def 4;

      then

      reconsider h = x as Function;

      x in ( product f) & x in ( product (f +* g)) by A1, XBOOLE_0:def 4;

      then

       A2: x in ( dom ( proj (f,i))) & x in ( dom ( proj ((f +* g),i))) by CARD_3:def 16;

      

      hence (( proj (f,i)) . x) = (h . i) by CARD_3:def 16

      .= (( proj ((f +* g),i)) . x) by A2, CARD_3:def 16;

    end;

    theorem :: TOPS_5:22

    

     Th22: for f,g be non-empty Function, i be object, A be set st A c= (( product f) /\ ( product (f +* g))) holds (( proj (f,i)) .: A) = (( proj ((f +* g),i)) .: A)

    proof

      let f,g be non-empty Function, i be object, A be set;

      assume

       A1: A c= (( product f) /\ ( product (f +* g)));

      for y be object holds y in (( proj (f,i)) .: A) iff y in (( proj ((f +* g),i)) .: A)

      proof

        let y be object;

        hereby

          assume y in (( proj (f,i)) .: A);

          then

          consider x be object such that

           A2: x in ( dom ( proj (f,i))) & x in A & y = (( proj (f,i)) . x) by FUNCT_1:def 6;

          x in ( product (f +* g)) by A1, A2, XBOOLE_0:def 4;

          then

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

          y = (( proj ((f +* g),i)) . x) by A2, A1, Th21;

          hence y in (( proj ((f +* g),i)) .: A) by A2, A4, FUNCT_1:def 6;

        end;

        assume y in (( proj ((f +* g),i)) .: A);

        then

        consider x be object such that

         A5: x in ( dom ( proj ((f +* g),i))) & x in A & y = (( proj ((f +* g),i)) . x) by FUNCT_1:def 6;

        x in ( product f) by A1, A5, XBOOLE_0:def 4;

        then

         A7: x in ( dom ( proj (f,i))) by CARD_3:def 16;

        y = (( proj (f,i)) . x) by A5, A1, Th21;

        hence y in (( proj (f,i)) .: A) by A5, A7, FUNCT_1:def 6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_5:23

    

     Th23: for f,g be non-empty Function st ( dom g) c= ( dom f) & for i be object st i in ( dom g) holds (g . i) c= (f . i) holds ( product (f +* g)) c= ( product f)

    proof

      let f,g be non-empty Function;

      assume that

       A1: ( dom g) c= ( dom f) and

       A2: for i be object st i in ( dom g) holds (g . i) c= (f . i);

      

       A3: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1

      .= ( dom f) by A1, XBOOLE_1: 12;

      now

        let x be object;

        assume x in ( dom (f +* g));

        thus ((f +* g) . x) c= (f . x)

        proof

          let i be object;

          assume

           A4: i in ((f +* g) . x);

          per cases ;

            suppose

             a5: x in ( dom g);

            then

             A5: i in (g . x) by A4, FUNCT_4: 13;

            (g . x) c= (f . x) by a5, A2;

            hence i in (f . x) by A5;

          end;

            suppose not x in ( dom g);

            hence i in (f . x) by A4, FUNCT_4: 11;

          end;

        end;

      end;

      hence ( product (f +* g)) c= ( product f) by A3, CARD_3: 27;

    end;

    theorem :: TOPS_5:24

    

     Th24: for f,g be non-empty Function st ( dom g) c= ( dom f) & for i be object st i in ( dom g) holds (g . i) c= (f . i) holds for i be object st i in (( dom f) \ ( dom g)) holds (( proj (f,i)) .: ( product (f +* g))) = (f . i)

    proof

      let f,g be non-empty Function;

      assume that

       A1: ( dom g) c= ( dom f) and

       A2: for i be object st i in ( dom g) holds (g . i) c= (f . i);

      

       A3: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1

      .= ( dom f) by A1, XBOOLE_1: 12;

      

       A4: ( product (f +* g)) = (( product f) /\ ( product (f +* g))) by A1, A2, Th23, XBOOLE_1: 28;

      let i be object;

      assume

       a5: i in (( dom f) \ ( dom g));

      then

       A5: i in ( dom f) & not i in ( dom g) by XBOOLE_0:def 5;

      

      thus (( proj (f,i)) .: ( product (f +* g))) = (( proj ((f +* g),i)) .: ( product (f +* g))) by A4, Th22

      .= (( proj ((f +* g),i)) .: ( dom ( proj ((f +* g),i)))) by CARD_3:def 16

      .= ( rng ( proj ((f +* g),i))) by RELAT_1: 113

      .= ((f +* g) . i) by A3, a5, YELLOW17: 3

      .= (f . i) by A5, FUNCT_4: 11;

    end;

    theorem :: TOPS_5:25

    

     Th25: for f,g be non-empty Function st ( dom g) c= ( dom f) & for i be object st i in ( dom g) holds (g . i) c= (f . i) holds for i be object st i in ( dom g) holds (( proj (f,i)) .: ( product (f +* g))) = (g . i)

    proof

      let f,g be non-empty Function;

      assume that

       A1: ( dom g) c= ( dom f) and

       A2: for i be object st i in ( dom g) holds (g . i) c= (f . i);

      

       A3: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1

      .= ( dom f) by A1, XBOOLE_1: 12;

      

       A4: ( product (f +* g)) = (( product f) /\ ( product (f +* g))) by A1, A2, Th23, XBOOLE_1: 28;

      let i be object;

      assume

       A5: i in ( dom g);

      

      thus (( proj (f,i)) .: ( product (f +* g))) = (( proj ((f +* g),i)) .: ( product (f +* g))) by A4, Th22

      .= (( proj ((f +* g),i)) .: ( dom ( proj ((f +* g),i)))) by CARD_3:def 16

      .= ( rng ( proj ((f +* g),i))) by RELAT_1: 113

      .= ((f +* g) . i) by A1, A3, A5, YELLOW17: 3

      .= (g . i) by A5, FUNCT_4: 13;

    end;

    theorem :: TOPS_5:26

    

     Th26: for f,g be non-empty Function st ( dom g) = ( dom f) & for i be object st i in ( dom g) holds (g . i) c= (f . i) holds for i be object st i in ( dom g) holds (( proj (f,i)) .: ( product g)) = (g . i)

    proof

      let f,g be non-empty Function;

      assume that

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

       A2: for i be object st i in ( dom g) holds (g . i) c= (f . i);

      let i be object;

      assume

       A3: i in ( dom g);

      

      thus (( proj (f,i)) .: ( product g)) = (( proj (f,i)) .: ( product (f +* g))) by A1, FUNCT_4: 19

      .= (g . i) by A1, A2, A3, Th25;

    end;

    theorem :: TOPS_5:27

    

     Th27: for f be Function, X,Y be set, i be object st X c= Y holds ( product (f +* (i .--> X))) c= ( product (f +* (i .--> Y)))

    proof

      let f be Function, X,Y be set, i be object;

      assume

       A1: X c= Y;

      ( dom (f +* (i .--> X))) = (( dom f) \/ ( dom (i .--> X))) by FUNCT_4:def 1

      .= (( dom f) \/ ( dom ( {i} --> X))) by FUNCOP_1:def 9

      .= (( dom f) \/ {i});

      

      then

       A3: ( dom (f +* (i .--> X))) = (( dom f) \/ ( dom ( {i} --> Y)))

      .= (( dom f) \/ ( dom (i .--> Y))) by FUNCOP_1:def 9

      .= ( dom (f +* (i .--> Y))) by FUNCT_4:def 1;

      now

        let x be object;

        assume x in ( dom (f +* (i .--> X)));

        per cases ;

          suppose

           A4: x = i;

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

          then x in ( dom ( {i} --> X)) & x in ( dom ( {i} --> Y));

          then

           A5: x in ( dom (i .--> X)) & x in ( dom (i .--> Y)) by FUNCOP_1:def 9;

          

          then

           A6: ((f +* (i .--> X)) . x) = ((i .--> X) . x) by FUNCT_4: 13

          .= X by A4, FUNCOP_1: 72;

          ((f +* (i .--> Y)) . x) = ((i .--> Y) . x) by A5, FUNCT_4: 13

          .= Y by A4, FUNCOP_1: 72;

          hence ((f +* (i .--> X)) . x) c= ((f +* (i .--> Y)) . x) by A1, A6;

        end;

          suppose x <> i;

          then not x in ( dom (i .--> X)) & not x in ( dom (i .--> Y)) by TARSKI:def 1;

          then ((f +* (i .--> X)) . x) = (f . x) & ((f +* (i .--> Y)) . x) = (f . x) by FUNCT_4: 11;

          hence ((f +* (i .--> X)) . x) c= ((f +* (i .--> Y)) . x);

        end;

      end;

      hence thesis by A3, CARD_3: 27;

    end;

    theorem :: TOPS_5:28

    

     Th28: for i,j be object, A,B,C,D be set st A c= C & B c= D holds ( product ((i,j) --> (A,B))) c= ( product ((i,j) --> (C,D)))

    proof

      let i,j be object, A,B,C,D be set;

      assume

       A1: A c= C & B c= D;

      per cases ;

        suppose

         A2: i <> j;

        let x be object;

        assume x in ( product ((i,j) --> (A,B)));

        then

        consider g be Function such that

         A3: g = x & ( dom g) = ( dom ((i,j) --> (A,B))) and

         A4: for y be object st y in ( dom ((i,j) --> (A,B))) holds (g . y) in (((i,j) --> (A,B)) . y) by CARD_3:def 5;

        

         A5: ( dom ((i,j) --> (A,B))) = {i, j} by FUNCT_4: 62

        .= ( dom ((i,j) --> (C,D))) by FUNCT_4: 62;

        for y be object st y in ( dom ((i,j) --> (C,D))) holds (g . y) in (((i,j) --> (C,D)) . y)

        proof

          let y be object;

          assume

           A6: y in ( dom ((i,j) --> (C,D)));

          then y in {i, j} by FUNCT_4: 62;

          per cases by TARSKI:def 2;

            suppose

             A7: y = i;

            then (g . y) in (((i,j) --> (A,B)) . i) by A4, A5, A6;

            then (g . y) in A by A2, FUNCT_4: 63;

            then (g . y) in C by A1;

            hence thesis by A2, A7, FUNCT_4: 63;

          end;

            suppose

             A8: y = j;

            then (g . y) in (((i,j) --> (A,B)) . j) by A4, A5, A6;

            then (g . y) in B by FUNCT_4: 63;

            then (g . y) in D by A1;

            hence thesis by A8, FUNCT_4: 63;

          end;

        end;

        hence thesis by A3, A5, CARD_3:def 5;

      end;

        suppose

         A9: i = j;

        

        then

         A10: ((i,j) --> (A,B)) = (i .--> B) by FUNCT_4: 81

        .= ( {i} --> B) by FUNCOP_1:def 9;

        ((i,j) --> (C,D)) = (i .--> D) by A9, FUNCT_4: 81

        .= ( {i} --> D) by FUNCOP_1:def 9;

        hence thesis by A1, A10, Th14;

      end;

    end;

    theorem :: TOPS_5:29

    

     Th29: for X,Y be set, f,i,j be object st i <> j holds f in ( product ((i,j) --> (X,Y))) iff ex x,y be object st x in X & y in Y & f = ((i,j) --> (x,y))

    proof

      let X,Y be set, f,i,j be object;

      assume

       A1: i <> j;

      thus f in ( product ((i,j) --> (X,Y))) implies ex x,y be object st x in X & y in Y & f = ((i,j) --> (x,y))

      proof

        assume f in ( product ((i,j) --> (X,Y)));

        then

        consider g be Function such that

         A2: g = f & ( dom g) = ( dom ((i,j) --> (X,Y))) and

         A3: for z be object st z in ( dom ((i,j) --> (X,Y))) holds (g . z) in (((i,j) --> (X,Y)) . z) by CARD_3:def 5;

        take (g . i), (g . j);

        

         A4: ( dom ((i,j) --> (X,Y))) = {i, j} by FUNCT_4: 62;

        then i in ( dom ((i,j) --> (X,Y))) by TARSKI:def 2;

        then (g . i) in (((i,j) --> (X,Y)) . i) by A3;

        hence (g . i) in X by A1, FUNCT_4: 63;

        j in ( dom ((i,j) --> (X,Y))) by A4, TARSKI:def 2;

        then (g . j) in (((i,j) --> (X,Y)) . j) by A3;

        hence thesis by A2, A4, FUNCT_4: 66, FUNCT_4: 63;

      end;

      given x,y be object such that

       A5: x in X & y in Y & f = ((i,j) --> (x,y));

      reconsider g = f as Function by A5;

      

       A6: ( dom g) = {i, j} by A5, FUNCT_4: 62

      .= ( dom ((i,j) --> (X,Y))) by FUNCT_4: 62;

      for z be object st z in ( dom ((i,j) --> (X,Y))) holds (g . z) in (((i,j) --> (X,Y)) . z)

      proof

        let z be object;

        assume z in ( dom ((i,j) --> (X,Y)));

        then z in {i, j} by FUNCT_4: 62;

        per cases by TARSKI:def 2;

          suppose

           A7: z = i;

          then (g . z) = x by A1, A5, FUNCT_4: 63;

          hence thesis by A1, A5, A7, FUNCT_4: 63;

        end;

          suppose

           A8: z = j;

          then (g . z) = y by A5, FUNCT_4: 63;

          hence thesis by A5, A8, FUNCT_4: 63;

        end;

      end;

      hence thesis by A6, CARD_3: 9;

    end;

    theorem :: TOPS_5:30

    

     Th30: for f be non-empty Function, X,Y be set, i,j,x,y be object holds for g be Function st x in X & y in Y & i <> j & g in ( product f) holds (g +* ((i,j) --> (x,y))) in ( product (f +* ((i,j) --> (X,Y))))

    proof

      let f be non-empty Function, X,Y be set;

      let i,j,x,y be object, g be Function;

      assume that

       A1: x in X & y in Y and

       A2: i <> j & g in ( product f);

      

       A3: ( dom (g +* ((i,j) --> (x,y)))) = (( dom g) \/ ( dom ((i,j) --> (x,y)))) by FUNCT_4:def 1

      .= (( dom g) \/ {i, j}) by FUNCT_4: 62

      .= (( dom f) \/ {i, j}) by A2, CARD_3: 9

      .= (( dom f) \/ ( dom ((i,j) --> (X,Y)))) by FUNCT_4: 62

      .= ( dom (f +* ((i,j) --> (X,Y)))) by FUNCT_4:def 1;

      for z be object st z in ( dom (f +* ((i,j) --> (X,Y)))) holds ((g +* ((i,j) --> (x,y))) . z) in ((f +* ((i,j) --> (X,Y))) . z)

      proof

        let z be object;

        assume

         A4: z in ( dom (f +* ((i,j) --> (X,Y))));

        per cases ;

          suppose

           A5: z in {i, j};

          then z in ( dom ((i,j) --> (x,y))) by FUNCT_4: 62;

          then

           A6: ((g +* ((i,j) --> (x,y))) . z) = (((i,j) --> (x,y)) . z) by FUNCT_4: 13;

          z in ( dom ((i,j) --> (X,Y))) by A5, FUNCT_4: 62;

          then

           A7: ((f +* ((i,j) --> (X,Y))) . z) = (((i,j) --> (X,Y)) . z) by FUNCT_4: 13;

          per cases by A5, TARSKI:def 2;

            suppose

             A8: z = i;

            then ((g +* ((i,j) --> (x,y))) . z) = x by A2, A6, FUNCT_4: 63;

            hence thesis by A1, A2, A7, A8, FUNCT_4: 63;

          end;

            suppose

             A9: z = j;

            then ((g +* ((i,j) --> (x,y))) . z) = y by A6, FUNCT_4: 63;

            hence thesis by A1, A7, A9, FUNCT_4: 63;

          end;

        end;

          suppose

           A10: not z in {i, j};

          then not z in ( dom ((i,j) --> (x,y))) by FUNCT_4: 62;

          then

           A11: ((g +* ((i,j) --> (x,y))) . z) = (g . z) by FUNCT_4: 11;

           not z in ( dom ((i,j) --> (X,Y))) by A10, FUNCT_4: 62;

          then

           A12: ((f +* ((i,j) --> (X,Y))) . z) = (f . z) by FUNCT_4: 11;

          z in (( dom f) \/ ( dom ((i,j) --> (X,Y)))) by A4, FUNCT_4:def 1;

          then z in (( dom f) \/ {i, j}) by FUNCT_4: 62;

          then z in ( dom f) by A10, XBOOLE_0:def 3;

          hence thesis by A2, A11, A12, CARD_3: 9;

        end;

      end;

      hence thesis by A3, CARD_3: 9;

    end;

    theorem :: TOPS_5:31

    

     Th31: for f be Function, A,B,C,D be set, i,j be object st A c= C & B c= D holds ( product (f +* ((i,j) --> (A,B)))) c= ( product (f +* ((i,j) --> (C,D))))

    proof

      let f be Function, A,B,C,D be set, i,j be object;

      assume

       A1: A c= C & B c= D;

      per cases ;

        suppose i = j;

        then ((i,j) --> (A,B)) = (i .--> B) & ((i,j) --> (C,D)) = (i .--> D) by FUNCT_4: 81;

        hence thesis by A1, Th27;

      end;

        suppose

         A2: i <> j;

        ( dom (f +* ((i,j) --> (A,B)))) = (( dom f) \/ ( dom ((i,j) --> (A,B)))) by FUNCT_4:def 1

        .= (( dom f) \/ {i, j}) by FUNCT_4: 62;

        

        then

         A3: ( dom (f +* ((i,j) --> (A,B)))) = (( dom f) \/ ( dom ((i,j) --> (C,D)))) by FUNCT_4: 62

        .= ( dom (f +* ((i,j) --> (C,D)))) by FUNCT_4:def 1;

        for x be object st x in ( dom (f +* ((i,j) --> (A,B)))) holds ((f +* ((i,j) --> (A,B))) . x) c= ((f +* ((i,j) --> (C,D))) . x)

        proof

          let x be object;

          assume x in ( dom (f +* ((i,j) --> (A,B))));

          per cases ;

            suppose

             A4: x in {i, j};

            then x in ( dom ((i,j) --> (A,B))) by FUNCT_4: 62;

            then

             A5: ((f +* ((i,j) --> (A,B))) . x) = (((i,j) --> (A,B)) . x) by FUNCT_4: 13;

            x in ( dom ((i,j) --> (C,D))) by A4, FUNCT_4: 62;

            then

             A6: ((f +* ((i,j) --> (C,D))) . x) = (((i,j) --> (C,D)) . x) by FUNCT_4: 13;

            per cases by A4, TARSKI:def 2;

              suppose

               A7: x = i;

              then ((f +* ((i,j) --> (A,B))) . x) = A by A2, A5, FUNCT_4: 63;

              hence thesis by A1, A2, A6, A7, FUNCT_4: 63;

            end;

              suppose

               A9: x = j;

              then ((f +* ((i,j) --> (A,B))) . x) = B by A5, FUNCT_4: 63;

              hence thesis by A1, A6, A9, FUNCT_4: 63;

            end;

          end;

            suppose

             A11: not x in {i, j};

            then not x in ( dom ((i,j) --> (A,B))) by FUNCT_4: 62;

            then

             A12: ((f +* ((i,j) --> (A,B))) . x) = (f . x) by FUNCT_4: 11;

             not x in ( dom ((i,j) --> (C,D))) by A11, FUNCT_4: 62;

            hence thesis by A12, FUNCT_4: 11;

          end;

        end;

        hence thesis by A3, CARD_3: 27;

      end;

    end;

    theorem :: TOPS_5:32

    for f be Function, A,B be set, i,j be object st i in ( dom f) & j in ( dom f) & A c= (f . i) & B c= (f . j) holds ( product (f +* ((i,j) --> (A,B)))) c= ( product f)

    proof

      let f be Function, A,B be set, i,j be object;

      assume

       A1: i in ( dom f) & j in ( dom f) & A c= (f . i) & B c= (f . j);

      then ( product f) = ( product (f +* ((i,j) --> ((f . i),(f . j))))) by Th11;

      hence thesis by A1, Th31;

    end;

    theorem :: TOPS_5:33

    

     Th33: for I be set, f,g be ManySortedSet of I holds (( product f) /\ ( product g)) = ( product (f (/\) g))

    proof

      let I be set, f,g be ManySortedSet of I;

      for x be object holds x in (( product f) /\ ( product g)) iff ex h be Function st h = x & ( dom h) = ( dom (f (/\) g)) & for y be object st y in ( dom (f (/\) g)) holds (h . y) in ((f (/\) g) . y)

      proof

        let x be object;

        hereby

          assume x in (( product f) /\ ( product g));

          then

           A1: x in ( product f) & x in ( product g) by XBOOLE_0:def 4;

          then

          consider h be Function such that

           A2: h = x & ( dom h) = ( dom f) and

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

          take h;

          thus h = x by A2;

          

          thus ( dom h) = I by A2, PARTFUN1:def 2

          .= ( dom (f (/\) g)) by PARTFUN1:def 2;

          let y be object;

          assume

           a4: y in ( dom (f (/\) g));

          then

           A4: y in I;

          

           A5: y in ( dom f) & y in ( dom g) by A4, PARTFUN1:def 2;

          then

           A6: (h . y) in (f . y) by A3;

          (h . y) in (g . y) by A1, A2, A5, CARD_3: 9;

          then (h . y) in ((f . y) /\ (g . y)) by A6, XBOOLE_0:def 4;

          hence (h . y) in ((f (/\) g) . y) by a4, PBOOLE:def 5;

        end;

        given h be Function such that

         A7: h = x & ( dom h) = ( dom (f (/\) g)) and

         A8: for y be object st y in ( dom (f (/\) g)) holds (h . y) in ((f (/\) g) . y);

        

         a9: ( dom h) = I by A7, PARTFUN1:def 2;

        then

         A9: ( dom h) = ( dom f) & ( dom h) = ( dom g) by PARTFUN1:def 2;

         A10:

        now

          let y be object;

          assume

           A11: (y in ( dom f) or y in ( dom g));

          (h . y) in ((f (/\) g) . y) by A7, A8, a9, A11;

          then (h . y) in ((f . y) /\ (g . y)) by A11, PBOOLE:def 5;

          hence (h . y) in (f . y) & (h . y) in (g . y) by XBOOLE_0:def 4;

        end;

        for y be object st y in ( dom f) holds (h . y) in (f . y) by A10;

        then

         A13: h in ( product f) by A9, CARD_3: 9;

        for y be object st y in ( dom g) holds (h . y) in (g . y) by A10;

        then h in ( product g) by A9, CARD_3: 9;

        hence x in (( product f) /\ ( product g)) by A7, A13, XBOOLE_0:def 4;

      end;

      hence thesis by CARD_3:def 5;

    end;

    

     Lm2: for I be 2 -element set, f be ManySortedSet of I holds for i,j be Element of I, x be object st i <> j holds (f +* (i,x)) = ((i,j) --> (x,(f . j)))

    proof

      let I be 2 -element set, f be ManySortedSet of I;

      let i,j be Element of I, x be object;

      assume

       A1: i <> j;

      then

       a2: I = {i, j} by Th8;

      then

       A2: ( dom f) = {i, j} by PARTFUN1:def 2;

      

       A3: ( dom (f +* (i,x))) = ( dom f) by FUNCT_7: 30

      .= ( dom ((i,j) --> (x,(f . j)))) by A2, FUNCT_4: 62;

      for z be object st z in ( dom (f +* (i,x))) holds ((f +* (i,x)) . z) = (((i,j) --> (x,(f . j))) . z)

      proof

        let z be object;

        assume z in ( dom (f +* (i,x)));

        per cases by a2, TARSKI:def 2;

          suppose

           A5: z = i;

          

          hence ((f +* (i,x)) . z) = x by A2, a2, FUNCT_7: 31

          .= (((i,j) --> (x,(f . j))) . z) by A1, A5, FUNCT_4: 63;

        end;

          suppose

           A6: z = j;

          

          hence ((f +* (i,x)) . z) = (f . j) by A1, FUNCT_7: 32

          .= (((i,j) --> (x,(f . j))) . z) by A6, FUNCT_4: 63;

        end;

      end;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: TOPS_5:34

    

     Th34: for I be 2 -element set, f be ManySortedSet of I holds for i,j be Element of I, x be object st i <> j holds (f +* (i,x)) = ((i,j) --> (x,(f . j))) & (f +* (j,x)) = ((i,j) --> ((f . i),x))

    proof

      let I be 2 -element set, f be ManySortedSet of I;

      let i,j be Element of I, x be object;

      assume

       A1: i <> j;

      thus (f +* (i,x)) = ((i,j) --> (x,(f . j))) by A1, Lm2;

      

      thus (f +* (j,x)) = ((j,i) --> (x,(f . i))) by A1, Lm2

      .= ((i,j) --> ((f . i),x)) by A1, Th10;

    end;

    theorem :: TOPS_5:35

    

     Th35: for f be non-empty Function, X be set, i be object st i in ( dom f) holds (f +* (i,X)) is non-empty iff X is non empty

    proof

      let f be non-empty Function, X be set, i be object;

      assume

       A1: i in ( dom f);

      hereby

        assume

         A2: (f +* (i,X)) is non-empty;

        i in ( dom (f +* (i,X))) by A1, FUNCT_7: 30;

        then ((f +* (i,X)) . i) <> {} by A2, FUNCT_1:def 9;

        hence X is non empty by A1, FUNCT_7: 31;

      end;

      assume

       A3: X is non empty;

      for x be object st x in ( dom (f +* (i,X))) holds ((f +* (i,X)) . x) is non empty

      proof

        let x be object;

        assume

         A4: x in ( dom (f +* (i,X)));

        

         A5: x in ( dom f) by A4, FUNCT_7: 30;

        x <> i implies ((f +* (i,X)) . x) = (f . x) by FUNCT_7: 32;

        hence thesis by A5, FUNCT_1:def 9, A3, FUNCT_7: 31;

      end;

      hence thesis by FUNCT_1:def 9;

    end;

    theorem :: TOPS_5:36

    

     Th36: for f be non-empty Function, X be set, i be object st i in ( dom f) holds ( product (f +* (i,X))) = {} iff X is empty

    proof

      let f be non-empty Function, X be set, i be object;

      assume

       A1: i in ( dom f);

      then

       A2: i in ( dom (f +* (i,X))) by FUNCT_7: 30;

      hereby

        assume ( product (f +* (i,X))) = {} ;

        then (f +* (i,X)) is non non-empty;

        hence X is empty by A1, Th35;

      end;

      assume X is empty;

      then ((f +* (i,X)) . i) = {} by A1, FUNCT_7: 31;

      then {} in ( rng (f +* (i,X))) by A2, FUNCT_1:def 3;

      hence thesis by CARD_3: 26;

    end;

    theorem :: TOPS_5:37

    

     Th37: for f be non-empty Function, X be set, i,x be object holds for g be Function st i in ( dom f) & x in X & g in ( product f) holds (g +* (i,x)) in ( product (f +* (i,X)))

    proof

      let f be non-empty Function, X be set, i,x be object;

      let g be Function;

      assume

       A1: i in ( dom f) & x in X & g in ( product f);

      

       A2: ( dom (g +* (i,x))) = ( dom g) by FUNCT_7: 30

      .= ( dom f) by A1, CARD_3: 9

      .= ( dom (f +* (i,X))) by FUNCT_7: 30;

      for y be object st y in ( dom (f +* (i,X))) holds ((g +* (i,x)) . y) in ((f +* (i,X)) . y)

      proof

        let y be object;

        assume

         A3: y in ( dom (f +* (i,X)));

        then

         A4: y in ( dom f) by FUNCT_7: 30;

        per cases ;

          suppose

           A5: i = y;

          y in ( dom f) by A3, FUNCT_7: 30;

          then y in ( dom g) by A1, CARD_3: 9;

          then ((g +* (i,x)) . y) = x by A5, FUNCT_7: 31;

          hence thesis by A1, A5, FUNCT_7: 31;

        end;

          suppose i <> y;

          then ((g +* (i,x)) . y) = (g . y) & ((f +* (i,X)) . y) = (f . y) by FUNCT_7: 32;

          hence thesis by A4, A1, CARD_3: 9;

        end;

      end;

      hence thesis by A2, CARD_3: 9;

    end;

    theorem :: TOPS_5:38

    

     Th38: for f be Function, X,Y be set, i be object st i in ( dom f) & X c= Y holds ( product (f +* (i,X))) c= ( product (f +* (i,Y)))

    proof

      let f be Function, X,Y be set, i be object;

      assume

       A1: i in ( dom f) & X c= Y;

      then (f +* (i,X)) = (f +* (i .--> X)) & (f +* (i,Y)) = (f +* (i .--> Y)) by FUNCT_7:def 3;

      hence thesis by A1, Th27;

    end;

    theorem :: TOPS_5:39

    

     Th39: for f be Function, X be set, i be object st i in ( dom f) & X c= (f . i) holds ( product (f +* (i,X))) c= ( product f)

    proof

      let f be Function, X be set, i be object;

      

       I: i is set by TARSKI: 1;

      assume i in ( dom f) & X c= (f . i);

      then ( product (f +* (i,X))) c= ( product (f +* (i,(f . i)))) by Th38;

      hence thesis by I, FUNCT_7: 35;

    end;

    theorem :: TOPS_5:40

    for f be non-empty Function, X,Y be non empty set, i,j be object st i in ( dom f) & j in ( dom f) & ( not X c= (f . i) or not (f . j) c= Y) & ( product (f +* (i,X))) c= ( product (f +* (j,Y))) holds i = j & X c= Y

    proof

      let f be non-empty Function, X,Y be non empty set, i,j be object;

      assume that

       A1: i in ( dom f) & j in ( dom f) and

       A2: not X c= (f . i) or not (f . j) c= Y and

       A3: ( product (f +* (i,X))) c= ( product (f +* (j,Y)));

      

       a4: (f +* (i,X)) is non-empty & (f +* (j,Y)) is non-empty by A1, Th35;

      thus

       A5: i = j

      proof

        assume

         A6: i <> j;

        

         A7: i in ( dom (f +* (i,X))) & j in ( dom (f +* (i,X))) by A1, FUNCT_7: 30;

        ((f +* (i,X)) . i) c= ((f +* (j,Y)) . i) by a4, A7, A3, PUA2MSS1: 1;

        then

         a8: X c= ((f +* (j,Y)) . i) by A1, FUNCT_7: 31;

        ((f +* (i,X)) . j) c= ((f +* (j,Y)) . j) by a4, A7, A3, PUA2MSS1: 1;

        then ((f +* (i,X)) . j) c= Y by A1, FUNCT_7: 31;

        hence contradiction by A2, a8, A6, FUNCT_7: 32;

      end;

      let x be object;

      assume

       A9: x in X;

      set g = the Element of ( product f);

      

       A10: (g +* (i,x)) in ( product (f +* (i,X))) by A1, A9, Th37;

      i in ( dom (f +* (j,Y))) by A1, FUNCT_7: 30;

      then ((g +* (i,x)) . i) in ((f +* (j,Y)) . i) by A3, A10, CARD_3: 9;

      then

       A11: ((g +* (i,x)) . i) in Y by A1, A5, FUNCT_7: 31;

      i in ( dom g) by A1, CARD_3: 9;

      hence thesis by A11, FUNCT_7: 31;

    end;

    theorem :: TOPS_5:41

    for f be non-empty Function, X be set, i be object st i in ( dom f) & ( product (f +* (i,X))) c= ( product f) holds X c= (f . i)

    proof

      let f be non-empty Function, X be set, i be object;

      assume

       A1: i in ( dom f) & ( product (f +* (i,X))) c= ( product f);

      let x be object;

      assume

       A2: x in X;

      set g = the Element of ( product f);

      

       a3: (g +* (i,x)) in ( product (f +* (i,X))) by A1, A2, Th37;

      i in ( dom g) by A1, CARD_3: 9;

      then ((g +* (i,x)) . i) = x by FUNCT_7: 31;

      hence thesis by A1, a3, CARD_3: 9;

    end;

    theorem :: TOPS_5:42

    

     Th42: for f be non-empty Function, X,Y be non empty set, i,j be object st i in ( dom f) & j in ( dom f) & (X <> (f . i) or Y <> (f . j)) & ( product (f +* (i,X))) = ( product (f +* (j,Y))) holds i = j & X = Y

    proof

      let f be non-empty Function, X,Y be non empty set, i,j be object;

      assume that

       A1: i in ( dom f) & j in ( dom f) and

       A2: X <> (f . i) or Y <> (f . j) and

       A3: ( product (f +* (i,X))) = ( product (f +* (j,Y)));

      (f +* (i,X)) is non-empty & (f +* (j,Y)) is non-empty by A1, Th35;

      then

       A4: (f +* (i,X)) = (f +* (j,Y)) by A3, PUA2MSS1: 2;

      thus

       A5: i = j

      proof

        assume

         A6: i <> j;

        

         A7: X = ((f +* (i,X)) . i) by A1, FUNCT_7: 31

        .= (f . i) by A4, A6, FUNCT_7: 32;

        Y = ((f +* (j,Y)) . j) by A1, FUNCT_7: 31

        .= (f . j) by A4, A6, FUNCT_7: 32;

        hence contradiction by A2, A7;

      end;

      

      thus X = ((f +* (j,Y)) . i) by A1, A4, FUNCT_7: 31

      .= Y by A1, A5, FUNCT_7: 31;

    end;

    theorem :: TOPS_5:43

    

     Th43: for f be non-empty Function, X be set, i be object st i in ( dom f) & X c= (f . i) holds (( proj (f,i)) .: ( product (f +* (i,X)))) = X

    proof

      let f be non-empty Function, X be set, i be object;

      assume

       A1: i in ( dom f) & X c= (f . i);

      

      then

       A2: (f +* (i,X)) = (f +* (i .--> X)) by FUNCT_7:def 3

      .= (f +* ( {i} --> X)) by FUNCOP_1:def 9;

      

       A3: i in ( dom (f +* (i,X))) by A1, FUNCT_7: 30;

      per cases ;

        suppose

         A4: X is non empty;

         {i} c= ( dom f) by A1, ZFMISC_1: 31;

        then

         A5: ( dom ( {i} --> X)) c= ( dom f);

        

         A6: for j be object st j in ( dom ( {i} --> X)) holds (( {i} --> X) . j) c= (f . j)

        proof

          let j be object;

          assume

           A7: j in ( dom ( {i} --> X));

          then i = j by TARSKI:def 1;

          hence thesis by A1, A7, FUNCOP_1: 7;

        end;

        

         A8: i in {i} by TARSKI:def 1;

        then i in ( dom ( {i} --> X));

        then (( proj (f,i)) .: ( product (f +* ( {i} --> X)))) = (( {i} --> X) . i) by A5, A6, A4, Th25;

        hence thesis by A2, A8, FUNCOP_1: 7;

      end;

        suppose

         A9: X is empty;

        then ((f +* (i,X)) . i) is empty by A1, FUNCT_7: 31;

        then {} in ( rng (f +* (i,X))) by A3, FUNCT_1: 3;

        then ( product (f +* (i,X))) = {} by CARD_3: 26;

        hence thesis by A9;

      end;

    end;

    theorem :: TOPS_5:44

    

     Th44: for x,y,z be object holds ((x .--> y) +* (x,z)) = (x .--> z)

    proof

      let x,y,z be object;

      ( dom (x .--> y)) = ( dom ( {x} --> y)) by FUNCOP_1:def 9

      .= {x};

      then x in ( dom (x .--> y)) by TARSKI:def 1;

      then ((x .--> y) +* (x,z)) = ((x .--> y) +* (x .--> z)) by FUNCT_7:def 3;

      hence thesis by Th12;

    end;

    registration

      let I be non empty set;

      let J be 1-sorted-yielding non-Empty ManySortedSet of I;

      cluster ( Carrier J) -> non-empty;

      coherence

      proof

        assume ( Carrier J) is non non-empty;

        then {} in ( rng ( Carrier J)) by RELAT_1:def 9;

        then

        consider i be object such that

         A1: i in ( dom ( Carrier J)) & (( Carrier J) . i) = {} by FUNCT_1:def 3;

        reconsider i as set by TARSKI: 1;

        consider R be 1-sorted such that

         A2: R = (J . i) & (( Carrier J) . i) = the carrier of R by A1, PRALG_1:def 15;

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

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

        then R is non empty by WAYBEL_3:def 7;

        hence contradiction by A1, A2;

      end;

    end

    begin

    theorem :: TOPS_5:45

    

     Th45: for T,S be TopSpace, f be Function of T, S holds f is open iff ex B be Basis of T st for V be Subset of T st V in B holds (f .: V) is open

    proof

      let T,S be TopSpace, f be Function of T, S;

      hereby

        assume

         A1: f is open;

        reconsider B = the Basis of T as Basis of T;

        take B;

        let V be Subset of T;

        assume V in B;

        hence (f .: V) is open by A1, TOPS_2:def 1, T_0TOPSP:def 2;

      end;

      given B be Basis of T such that

       A2: for V be Subset of T st V in B holds (f .: V) is open;

      now

        let A be Subset of T;

        set Y = { G where G be Subset of T : G in B & G c= A };

        Y c= ( bool the carrier of T)

        proof

          let g be object;

          assume g in Y;

          then ex G be Subset of T st g = G & G in B & G c= A;

          hence thesis;

        end;

        then

        reconsider Y as Subset-Family of T;

        set Z = { (f .: G) where G be Subset of T : G in Y };

        Z c= ( bool the carrier of S)

        proof

          let h be object;

          assume h in Z;

          then ex G be Subset of T st h = (f .: G) & G in Y;

          hence thesis;

        end;

        then

        reconsider Z as Subset-Family of S;

        

         A7: for P be Subset of S holds P in Z implies P is open

        proof

          let P be Subset of S;

          assume P in Z;

          then

          consider G1 be Subset of T such that

           A5: P = (f .: G1) & G1 in Y;

          ex G2 be Subset of T st G1 = G2 & G2 in B & G2 c= A by A5;

          hence thesis by A2, A5;

        end;

        assume A is open;

        then A = ( union Y) by YELLOW_8: 9;

        then (f .: A) = ( union Z) by RELSET_2: 14;

        hence (f .: A) is open by A7, TOPS_2: 19, TOPS_2:def 1;

      end;

      hence thesis by T_0TOPSP:def 2;

    end;

    theorem :: TOPS_5:46

    for T1,T2,S1,S2 be non empty TopSpace holds for f be Function of T1, S1, g be Function of T2, S2 st f is open & g is open holds [:f, g:] is open

    proof

      let T1,T2,S1,S2 be non empty TopSpace;

      let f be Function of T1, S1, g be Function of T2, S2;

      assume

       A1: f is open & g is open;

      ex B be Basis of [:T1, T2:] st for P be Subset of [:T1, T2:] st P in B holds ( [:f, g:] .: P) is open

      proof

        set B1 = the Basis of T1;

        set B2 = the Basis of T2;

        set B = { [:V, W:] where V be Subset of T1, W be Subset of T2 : V in B1 & W in B2 };

        reconsider B as Basis of [:T1, T2:] by YELLOW_9: 40;

        take B;

        let P be Subset of [:T1, T2:];

        assume P in B;

        then

        consider V be Subset of T1, W be Subset of T2 such that

         A2: P = [:V, W:] & V in B1 & W in B2;

        

         A3: (f .: V) is open & (g .: W) is open by A1, T_0TOPSP:def 2, A2, TOPS_2:def 1;

        ( [:f, g:] .: P) = [:(f .: V), (g .: W):] by A2, FUNCT_3: 72;

        hence thesis by A3, BORSUK_1: 6;

      end;

      hence thesis by Th45;

    end;

    theorem :: TOPS_5:47

    

     Th47: for S,T be non empty TopSpace, f be Function of S, T st f is bijective & ex K be Basis of S, L be Basis of T st (f .: K) = L holds f is being_homeomorphism

    proof

      let S,T be non empty TopSpace, f be Function of S, T;

      assume

       A1: f is bijective;

      given K be Basis of S, L be Basis of T such that

       A2: (f .: K) = L;

      for W be Subset of T st W in L holds (f " W) is open

      proof

        let W be Subset of T;

        assume W in L;

        then

        consider V be Subset of S such that

         A3: V in K & W = (f .: V) by A2, FUNCT_2:def 10;

        ( dom f) = the carrier of S by FUNCT_2:def 1;

        then V = (f " W) by A1, A3, FUNCT_1: 94;

        hence thesis by A3, TOPS_2:def 1;

      end;

      then

       A4: f is continuous by YELLOW_9: 34;

      for V be Subset of S st V in K holds (f .: V) is open

      proof

        let V be Subset of S;

        assume V in K;

        then (f .: V) in (f .: K) by FUNCT_2:def 10;

        hence thesis by A2, TOPS_2:def 1;

      end;

      then f is open by Th45;

      then

       A5: (f " ) is continuous by A1, TOPREALA: 14;

      

       A6: ( rng f) = the carrier of T by A1, FUNCT_2:def 3

      .= ( [#] T) by STRUCT_0:def 3;

      ( dom f) = the carrier of S by FUNCT_2:def 1

      .= ( [#] S) by STRUCT_0:def 3;

      hence thesis by A1, A5, A4, A6, TOPS_2:def 5;

    end;

    theorem :: TOPS_5:48

    

     Th48: for S,T be non empty TopSpace, f be Function of S, T st f is bijective & ex K be prebasis of S, L be prebasis of T st (f .: K) = L holds f is being_homeomorphism

    proof

      let S,T be non empty TopSpace, f be Function of S, T;

      assume

       A1: f is bijective;

      given K be prebasis of S, L be prebasis of T such that

       A2: (f .: K) = L;

      reconsider K0 = ( FinMeetCl K) as Basis of S by YELLOW_9: 23;

      reconsider L0 = ( FinMeetCl L) as Basis of T by YELLOW_9: 23;

      reconsider g = (f " ) as Function of T, S;

      reconsider f0 = f as one-to-one Function by A1;

      

       a3: (f0 " ) = g by A1, TOPS_2:def 4;

      for W be Subset of T holds W in L0 iff ex V be Subset of S st V in K0 & (f .: V) = W

      proof

        let W be Subset of T;

        thus W in L0 implies ex V be Subset of S st V in K0 & (f .: V) = W

        proof

          assume W in L0;

          then

          consider Y be Subset-Family of T such that

           A4: Y c= L & Y is finite & W = ( Intersect Y) by CANTOR_1:def 3;

          per cases ;

            suppose

             A5: Y <> {} ;

            then

             A6: W = ( meet Y) by A4, SETFAM_1:def 9;

            reconsider X = (g .: Y) as Subset-Family of S;

            reconsider V = ( meet X) as Subset of S;

            take V;

            ex Z be Subset-Family of S st Z c= K & Z is finite & V = ( Intersect Z)

            proof

              take X;

              for x be object st x in X holds x in K

              proof

                let x be object;

                assume x in X;

                then

                consider B be Subset of T such that

                 A7: B in Y & x = (g .: B) by FUNCT_2:def 10;

                consider A be Subset of S such that

                 A8: A in K & B = (f .: A) by A2, A4, A7, FUNCT_2:def 10;

                

                 A9: ( dom f) = the carrier of S by FUNCT_2:def 1;

                x = (f " (f .: A)) by a3, FUNCT_1: 85, A7, A8

                .= A by A1, A9, FUNCT_1: 94;

                hence thesis by A8;

              end;

              hence X c= K & X is finite by A4, TARSKI:def 3;

              consider B be object such that

               A10: B in Y by A5, XBOOLE_0:def 1;

              reconsider B as Subset of T by A10;

              (g .: B) in X by A10, FUNCT_2:def 10;

              hence thesis by SETFAM_1:def 9;

            end;

            hence V in K0 by CANTOR_1:def 3;

            set Z = { (f .: A) where A be Subset of S : A in X };

            for x be object holds x in Z iff x in Y

            proof

              let x be object;

              

               A11: ( rng f) = the carrier of T by A1, FUNCT_2:def 3;

              hereby

                assume x in Z;

                then

                consider A be Subset of S such that

                 A12: (f .: A) = x & A in X;

                consider B be Subset of T such that

                 A13: B in Y & A = (g .: B) by A12, FUNCT_2:def 10;

                x = (f .: (f " B)) by a3, FUNCT_1: 85, A12, A13

                .= B by A11, FUNCT_1: 77;

                hence x in Y by A13;

              end;

              assume

               A14: x in Y;

              then

              reconsider B = x as Subset of T;

              

               A15: (g .: B) in X by A14, FUNCT_2:def 10;

              (f .: (g .: B)) = (f .: (f " B)) by a3, FUNCT_1: 85

              .= B by A11, FUNCT_1: 77;

              hence thesis by A15;

            end;

            then Z = Y by TARSKI: 2;

            hence (f .: V) = W by A1, A6, Th4;

          end;

            suppose Y = {} ;

            then

             A16: W = the carrier of T by A4, SETFAM_1:def 9;

            set V = ( [#] S);

            take V;

            set Z = the empty Subset-Family of S;

            ( Intersect Z) = the carrier of S by SETFAM_1:def 9;

            then Z c= K & Z is finite & V = ( Intersect Z) by XBOOLE_1: 2, STRUCT_0:def 3;

            hence V in K0 by CANTOR_1:def 3;

            

            thus (f .: V) = (f .: the carrier of S) by STRUCT_0:def 3

            .= (f .: ( dom f)) by FUNCT_2:def 1

            .= ( rng f) by RELAT_1: 113

            .= W by A16, A1, FUNCT_2:def 3;

          end;

        end;

        given V be Subset of S such that

         A17: V in K0 & (f .: V) = W;

        consider X be Subset-Family of S such that

         A18: X c= K & X is finite & V = ( Intersect X) by A17, CANTOR_1:def 3;

        per cases ;

          suppose

           A19: X <> {} ;

          then

           A20: V = ( meet X) by A18, SETFAM_1:def 9;

          ex Y be Subset-Family of T st Y c= L & Y is finite & W = ( Intersect Y)

          proof

            reconsider Y = (f .: X) as Subset-Family of T;

            take Y;

            thus Y c= L

            proof

              let x be object;

              assume x in Y;

              then ex A be Subset of S st A in X & (f .: A) = x by FUNCT_2:def 10;

              hence thesis by A2, FUNCT_2:def 10, A18;

            end;

            thus Y is finite by A18;

            set Z = { (f .: A) where A be Subset of S : A in X };

            for x be object holds x in Y iff x in Z

            proof

              let x be object;

              hereby

                assume x in Y;

                then ex A be Subset of S st A in X & (f .: A) = x by FUNCT_2:def 10;

                hence x in Z;

              end;

              assume x in Z;

              then ex A be Subset of S st (f .: A) = x & A in X;

              hence thesis by FUNCT_2:def 10;

            end;

            then Y = Z by TARSKI: 2;

            then

             A24: ( meet Y) = W by A1, A17, A20, Th4;

            consider A be object such that

             A25: A in X by A19, XBOOLE_0:def 1;

            reconsider A as Subset of S by A25;

            (f .: A) in (f .: X) by A25, FUNCT_2:def 10;

            hence thesis by A24, SETFAM_1:def 9;

          end;

          hence thesis by CANTOR_1:def 3;

        end;

          suppose X = {} ;

          then

           A26: V = the carrier of S by A18, SETFAM_1:def 9;

          set Y = the empty Subset-Family of T;

          

           B1: Y c= L & Y is finite by XBOOLE_1: 2;

          W = (f .: ( dom f)) by A17, A26, FUNCT_2:def 1

          .= ( rng f) by RELAT_1: 113

          .= the carrier of T by A1, FUNCT_2:def 3

          .= ( Intersect Y) by SETFAM_1:def 9;

          hence W in L0 by B1, CANTOR_1:def 3;

        end;

      end;

      then (f .: K0) = L0 by FUNCT_2:def 10;

      hence thesis by A1, Th47;

    end;

    theorem :: TOPS_5:49

    

     Th49: for S,T be TopSpace st ex K be Basis of S, L be Basis of T st K = ( INTERSECTION (L, {( [#] S)})) holds S is SubSpace of T

    proof

      let S,T be TopSpace;

      given K be Basis of S, L be Basis of T such that

       A1: K = ( INTERSECTION (L, {( [#] S)}));

      

       A2: for A be Subset of S holds A in the topology of S iff ex B be Subset of T st B in the topology of T & A = (B /\ ( [#] S))

      proof

        let A be Subset of S;

        hereby

          assume A in the topology of S;

          then A in ( UniCl K) by CANTOR_1:def 2, TARSKI:def 3;

          then

          consider X be Subset-Family of S such that

           A3: X c= K & A = ( union X) by CANTOR_1:def 1;

          set Y = { D where D be Subset of T : D in L & ex C be Element of K st C in X & C = (D /\ ( [#] S)) };

          Y c= ( bool the carrier of T)

          proof

            let x be object;

            assume x in Y;

            then ex D be Subset of T st D = x & D in L & ex C be Element of K st C in X & C = (D /\ ( [#] S));

            hence thesis;

          end;

          then

          reconsider Y as Subset-Family of T;

          set B = ( union Y);

          take B;

          for x be Subset of T holds x in Y implies x is open

          proof

            let x be Subset of T;

            assume x in Y;

            then ex D be Subset of T st D = x & D in L & ex C be Element of K st C in X & C = (D /\ ( [#] S));

            hence thesis by TOPS_2:def 1;

          end;

          then Y is open by TOPS_2:def 1;

          hence B in the topology of T by TOPS_2: 19, PRE_TOPC:def 2;

          for x be object holds x in A iff x in (B /\ ( [#] S))

          proof

            let x be object;

            hereby

              assume x in A;

              then

              consider C be set such that

               A6: x in C & C in X by A3, TARSKI:def 4;

              reconsider C as Element of K by A3, A6;

              consider D,S0 be set such that

               A7: D in L & S0 in {( [#] S)} & C = (D /\ S0) by A1, A3, A6, SETFAM_1:def 5;

              reconsider D as Subset of T by A7;

              C in X & C = (D /\ ( [#] S)) by A6, A7, TARSKI:def 1;

              then

               A8: D in Y by A7;

              x in D by A6, A7, XBOOLE_0:def 4;

              then

               A9: x in B by A8, TARSKI:def 4;

              x in S0 by A6, A7, XBOOLE_0:def 4;

              then x in ( [#] S) by A7, TARSKI:def 1;

              hence x in (B /\ ( [#] S)) by A9, XBOOLE_0:def 4;

            end;

            assume

             A10: x in (B /\ ( [#] S));

            then x in B by XBOOLE_0:def 4;

            then

            consider D0 be set such that

             A11: x in D0 & D0 in Y by TARSKI:def 4;

            consider D be Subset of T such that

             A12: D = D0 & D in L and

             A13: ex C be Element of K st C in X & C = (D /\ ( [#] S)) by A11;

            consider C be Element of K such that

             A14: C in X & C = (D /\ ( [#] S)) by A13;

            x in ( [#] S) by A10, XBOOLE_0:def 4;

            then x in C by A11, A12, A14, XBOOLE_0:def 4;

            hence thesis by A3, A14, TARSKI:def 4;

          end;

          hence A = (B /\ ( [#] S)) by TARSKI: 2;

        end;

        given B be Subset of T such that

         A15: B in the topology of T & A = (B /\ ( [#] S));

        B in ( UniCl L) by A15, CANTOR_1:def 2, TARSKI:def 3;

        then

        consider Y be Subset-Family of T such that

         A16: Y c= L & B = ( union Y) by CANTOR_1:def 1;

        set X = ( INTERSECTION (Y, {( [#] S)}));

        X c= ( bool the carrier of S)

        proof

          let x be object;

          reconsider x0 = x as set by TARSKI: 1;

          assume x in X;

          then

          consider C,S0 be set such that

           A17: C in Y & S0 in {( [#] S)} & x0 = (C /\ S0) by SETFAM_1:def 5;

          x0 c= S0 by A17, XBOOLE_1: 17;

          then x0 c= ( [#] S) by A17, TARSKI:def 1;

          then x0 c= the carrier of S by STRUCT_0:def 3;

          hence thesis;

        end;

        then

        reconsider X as Subset-Family of S;

        for x be Subset of S holds x in X implies x is open

        proof

          let x be Subset of S;

          assume x in X;

          then

          consider C,S0 be set such that

           A18: C in Y & S0 in {( [#] S)} & x = (C /\ S0) by SETFAM_1:def 5;

          x in K by A1, A16, A18, SETFAM_1:def 5;

          hence thesis by TOPS_2:def 1;

        end;

        then

         A19: X is open by TOPS_2:def 1;

        A = ( union X) by A15, A16, SETFAM_1: 25;

        hence thesis by A19, TOPS_2: 19, PRE_TOPC:def 2;

      end;

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

      then

      consider B be Subset of T such that

       A20: B in the topology of T & the carrier of S = (B /\ ( [#] S)) by A2;

      ( [#] S) = (B /\ ( [#] S)) by A20, STRUCT_0:def 3;

      then ( [#] S) c= B by XBOOLE_1: 17;

      then ( [#] S) c= the carrier of T by XBOOLE_1: 1;

      then ( [#] S) c= ( [#] T) by STRUCT_0:def 3;

      hence thesis by A2, PRE_TOPC:def 4;

    end;

    theorem :: TOPS_5:50

    

     Th50: for S,T be TopSpace st ( [#] S) c= ( [#] T) & ex K be prebasis of S, L be prebasis of T st K = ( INTERSECTION (L, {( [#] S)})) holds S is SubSpace of T

    proof

      let S,T be TopSpace;

      assume

       A1: ( [#] S) c= ( [#] T);

      given K be prebasis of S, L be prebasis of T such that

       A2: K = ( INTERSECTION (L, {( [#] S)}));

      reconsider K0 = ( FinMeetCl K) as Basis of S by YELLOW_9: 23;

      reconsider L0 = ( FinMeetCl L) as Basis of T by YELLOW_9: 23;

      for x be object holds x in K0 iff x in ( INTERSECTION (L0, {( [#] S)}))

      proof

        let x be object;

        hereby

          assume

           A3: x in K0;

          then

          reconsider A = x as Subset of S;

          consider X be Subset-Family of S such that

           A4: X c= K & X is finite & A = ( Intersect X) by A3, CANTOR_1:def 3;

          per cases ;

            suppose

             A5: X <> {} ;

            then

             A6: A = ( meet X) by A4, SETFAM_1:def 9;

            defpred P[ object, object] means ex D be Subset of T st $1 = (D /\ ( [#] S)) & $2 = D;

            

             A7: for x be object st x in X holds ex y be object st y in L & P[x, y]

            proof

              let x be object;

              assume x in X;

              then

              consider D,S0 be set such that

               A8: D in L & S0 in {( [#] S)} & x = (D /\ S0) by A2, A4, SETFAM_1:def 5;

              take D;

              thus D in L by A8;

              reconsider D0 = D as Subset of T by A8;

              take D0;

              thus thesis by A8, TARSKI:def 1;

            end;

            consider f be Function such that

             A9: ( dom f) = X & ( rng f) c= L and

             A10: for x be object st x in X holds P[x, (f . x)] from FUNCT_1:sch 6( A7);

            reconsider Y = ( rng f) as Subset-Family of T by A9, XBOOLE_1: 1;

            set B = ( meet Y);

            

             A11: Y is finite by A4, A9, FINSET_1: 8;

            

             A12: f <> {} by A5, A9;

            then B = ( Intersect Y) by SETFAM_1:def 9;

            then

             A13: B in L0 by A9, A11, CANTOR_1:def 3;

            for y be object holds y in A iff y in (B /\ ( [#] S))

            proof

              let y be object;

              hereby

                assume

                 A14: y in A;

                for D be set st D in Y holds y in D

                proof

                  let D be set;

                  assume D in Y;

                  then

                  consider C be object such that

                   A15: C in ( dom f) & (f . C) = D by FUNCT_1:def 3;

                  reconsider C as set by TARSKI: 1;

                  

                   A16: ex D0 be Subset of T st C = (D0 /\ ( [#] S)) & D = D0 by A9, A10, A15;

                  y in C by A6, A9, A14, A15, SETFAM_1:def 1;

                  hence thesis by A16, TARSKI:def 3, XBOOLE_1: 17;

                end;

                then

                 A17: y in B by A12, SETFAM_1:def 1;

                the carrier of S = ( [#] S) by STRUCT_0:def 3;

                hence y in (B /\ ( [#] S)) by A14, A17, XBOOLE_0:def 4;

              end;

              assume y in (B /\ ( [#] S));

              then

               A18: y in B & y in ( [#] S) by XBOOLE_0:def 4;

              for C be set st C in X holds y in C

              proof

                let C be set;

                assume

                 A19: C in X;

                then

                consider D be Subset of T such that

                 A20: C = (D /\ ( [#] S)) & (f . C) = D by A10;

                D in Y by A9, A19, A20, FUNCT_1:def 3;

                then y in D by A18, SETFAM_1:def 1;

                hence thesis by A18, A20, XBOOLE_0:def 4;

              end;

              hence thesis by A5, A6, SETFAM_1:def 1;

            end;

            then

             A21: A = (B /\ ( [#] S)) by TARSKI: 2;

            ( [#] S) in {( [#] S)} by TARSKI:def 1;

            hence x in ( INTERSECTION (L0, {( [#] S)})) by A13, A21, SETFAM_1:def 5;

          end;

            suppose X = {} ;

            

            then

             A22: A = the carrier of S by A4, SETFAM_1:def 9

            .= ( [#] S) by STRUCT_0:def 3;

            ex B,S0 be set st B in L0 & S0 in {( [#] S)} & A = (B /\ S0)

            proof

              take ( [#] T), ( [#] S);

              set Y = the empty Subset-Family of T;

              

               A23: Y c= L & Y is finite by XBOOLE_1: 2;

              ( Intersect Y) = the carrier of T by SETFAM_1:def 9

              .= ( [#] T) by STRUCT_0:def 3;

              hence thesis by A1, A22, XBOOLE_1: 28, TARSKI:def 1, A23, CANTOR_1:def 3;

            end;

            hence x in ( INTERSECTION (L0, {( [#] S)})) by SETFAM_1:def 5;

          end;

        end;

        assume x in ( INTERSECTION (L0, {( [#] S)}));

        then

        consider B,S0 be set such that

         A24: B in L0 & S0 in {( [#] S)} & x = (B /\ S0) by SETFAM_1:def 5;

        consider Y be Subset-Family of T such that

         A25: Y c= L & Y is finite & B = ( Intersect Y) by A24, CANTOR_1:def 3;

        per cases ;

          suppose

           A26: Y <> {} ;

          defpred P[ object, object] means ex D be Subset of T st $2 = (D /\ ( [#] S)) & $1 = D;

          

           A27: for x be object st x in Y holds ex y be object st y in K & P[x, y]

          proof

            let x be object;

            assume

             A28: x in Y;

            then

            reconsider D = x as Subset of T;

            take (D /\ ( [#] S));

            ( [#] S) in {( [#] S)} by TARSKI:def 1;

            hence (D /\ ( [#] S)) in K by A2, A25, A28, SETFAM_1:def 5;

            take D;

            thus thesis;

          end;

          consider f be Function such that

           A29: ( dom f) = Y & ( rng f) c= K and

           A30: for x be object st x in Y holds P[x, (f . x)] from FUNCT_1:sch 6( A27);

          reconsider X = ( rng f) as Subset-Family of S by A29, XBOOLE_1: 1;

          

           A31: X is finite by A25, A29, FINSET_1: 8;

          

           a32: f <> {} by A26, A29;

          reconsider A = x as set by TARSKI: 1;

          for y be object holds y in A iff for M be set st M in X holds y in M

          proof

            let y be object;

            hereby

              assume

               A33: y in A;

              let M be set;

              assume M in X;

              then

              consider D be object such that

               A34: D in ( dom f) & (f . D) = M by FUNCT_1:def 3;

              consider D0 be Subset of T such that

               A35: M = (D0 /\ ( [#] S)) & D = D0 by A29, A30, A34;

              y in B by A24, A33, XBOOLE_0:def 4;

              then y in ( meet Y) by A25, A26, SETFAM_1:def 9;

              then

               A36: y in D0 by A29, A34, A35, SETFAM_1:def 1;

              y in S0 by A24, A33, XBOOLE_0:def 4;

              then y in ( [#] S) by A24, TARSKI:def 1;

              hence y in M by A36, A35, XBOOLE_0:def 4;

            end;

            assume

             A37: for M be set st M in X holds y in M;

            for M be set st M in Y holds y in M

            proof

              let M be set;

              assume

               A38: M in Y;

              then

              consider D be Subset of T such that

               A39: (f . M) = (D /\ ( [#] S)) & M = D by A30;

              (M /\ ( [#] S)) in X by A29, A38, A39, FUNCT_1: 3;

              then y in (M /\ ( [#] S)) by A37;

              hence thesis by XBOOLE_1: 17, TARSKI:def 3;

            end;

            then y in ( meet Y) by A26, SETFAM_1:def 1;

            then

             A40: y in B by A25, A26, SETFAM_1:def 9;

            set M0 = the Element of Y;

            consider D0 be Subset of T such that

             A41: (f . M0) = (D0 /\ ( [#] S)) & M0 = D0 by A26, A30;

            (M0 /\ ( [#] S)) in X by A29, A26, A41, FUNCT_1: 3;

            then y in (M0 /\ ( [#] S)) by A37;

            then y in ( [#] S) by XBOOLE_1: 17, TARSKI:def 3;

            then y in S0 by A24, TARSKI:def 1;

            hence thesis by A24, A40, XBOOLE_0:def 4;

          end;

          then A = ( meet X) by a32, SETFAM_1:def 1;

          then x = ( Intersect X) by a32, SETFAM_1:def 9;

          hence thesis by A29, A31, CANTOR_1:def 3;

        end;

          suppose Y = {} ;

          

          then

           A42: B = the carrier of T by A25, SETFAM_1:def 9

          .= ( [#] T) by STRUCT_0:def 3;

          set X = the empty Subset-Family of S;

          ( [#] S) = the carrier of S by STRUCT_0:def 3;

          then

           a43: X c= K & X is finite & ( [#] S) = ( Intersect X) by XBOOLE_1: 2, SETFAM_1:def 9;

          x = (B /\ ( [#] S)) by A24, TARSKI:def 1

          .= ( [#] S) by A1, A42, XBOOLE_1: 28;

          hence thesis by a43, CANTOR_1:def 3;

        end;

      end;

      hence thesis by TARSKI: 2, Th49;

    end;

    theorem :: TOPS_5:51

    

     Th51: for S,T be TopSpace st ex K be prebasis of S, L be prebasis of T st ( [#] S) in K & K = ( INTERSECTION (L, {( [#] S)})) holds S is SubSpace of T

    proof

      let S,T be TopSpace;

      given K be prebasis of S, L be prebasis of T such that

       A1: ( [#] S) in K & K = ( INTERSECTION (L, {( [#] S)}));

      consider B,S0 be set such that

       A2: B in L & S0 in {( [#] S)} & ( [#] S) = (B /\ S0) by A1, SETFAM_1:def 5;

      B c= the carrier of T by A2;

      then

       A3: B c= ( [#] T) by STRUCT_0:def 3;

      ( [#] S) c= B by A2, XBOOLE_1: 17;

      hence thesis by A1, A3, Th50, XBOOLE_1: 1;

    end;

    theorem :: TOPS_5:52

    

     Th52: for I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for i be Element of I holds ( rng ( proj (J,i))) = the carrier of (J . i)

    proof

      let I be non empty set;

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

      let i be Element of I;

      

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

      

      thus ( rng ( proj (J,i))) = ( rng ( proj (( Carrier J),i))) by WAYBEL18:def 4

      .= (( Carrier J) . i) by A1, YELLOW17: 3

      .= ( [#] (J . i)) by PENCIL_3: 7

      .= the carrier of (J . i) by STRUCT_0:def 3;

    end;

    registration

      let X be set, T be TopStruct;

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

      coherence ;

    end

    definition

      let F be Relation;

      :: TOPS_5:def1

      attr F is TopSpace-yielding means

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

    end

    registration

      cluster TopSpace-yielding -> TopStruct-yielding for Relation;

      coherence

      proof

        let F be Relation;

        assume F is TopSpace-yielding;

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

        hence thesis by WAYBEL18:def 1;

      end;

    end

    registration

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

      coherence ;

    end

    registration

      let X be set, T be TopSpace;

      cluster (X --> T) -> TopSpace-yielding;

      coherence

      proof

        for x be set st x in ( rng (X --> T)) holds x is TopSpace by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      let I be set;

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

      existence

      proof

        take J = (I --> the non empty TopSpace);

        thus thesis;

      end;

    end

    definition

      let I be non empty set;

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

      let i be Element of I;

      :: original: .

      redefine

      func J . i -> non empty TopSpace ;

      coherence

      proof

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

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

        hence thesis by Def1;

      end;

    end

    definition

      let f be Function;

      :: TOPS_5:def2

      func ProjMap f -> ManySortedFunction of ( dom f) means

      : Def2: for x be object st x in ( dom f) holds (it . x) = ( proj (f,x));

      existence

      proof

        deffunc F( object) = ( proj (f,$1));

        consider g be ManySortedSet of ( dom f) such that

         A1: for x be object st x in ( dom f) holds (g . x) = F(x) from PBOOLE:sch 4;

        now

          let x be object;

          assume x in ( dom g);

          then (g . x) = ( proj (f,x)) by A1;

          hence (g . x) is Function;

        end;

        then

        reconsider g as ManySortedFunction of ( dom f) by FUNCOP_1:def 6;

        take g;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let g1,g2 be ManySortedFunction of ( dom f);

        assume that

         A2: for x be object st x in ( dom f) holds (g1 . x) = ( proj (f,x)) and

         A3: for x be object st x in ( dom f) holds (g2 . x) = ( proj (f,x));

        now

          let x be object;

          assume

           A4: x in ( dom f);

          

          hence (g1 . x) = ( proj (f,x)) by A2

          .= (g2 . x) by A3, A4;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    registration

      let f be empty Function;

      cluster ( ProjMap f) -> empty;

      coherence ;

    end

    registration

      let f be non-empty Function;

      cluster ( ProjMap f) -> non-empty;

      coherence

      proof

        now

          let x be object;

          assume x in ( dom ( ProjMap f));

          then (( ProjMap f) . x) = ( proj (f,x)) by Def2;

          hence (( ProjMap f) . x) is non empty;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

    end

    registration

      let f be non non-empty Function;

      cluster ( ProjMap f) -> empty-yielding;

      coherence

      proof

         {} in ( rng f) by RELAT_1:def 9;

        then

         A1: ( product f) = {} by CARD_3: 26;

        now

          let x be object;

          assume x in ( dom ( ProjMap f));

          then (( ProjMap f) . x) = ( proj (f,x)) by Def2;

          hence (( ProjMap f) . x) is empty by A1;

        end;

        hence thesis by FUNCT_1:def 8;

      end;

    end

    definition

      let I be non empty set;

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

      :: TOPS_5:def3

      func ProjMap J -> ManySortedSet of I equals ( ProjMap ( Carrier J));

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

      let I be non empty set;

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

      cluster ( ProjMap J) -> Function-yielding non empty non-empty;

      coherence ;

    end

    theorem :: TOPS_5:53

    

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

    proof

      let I be non empty set;

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

      let i be Element of I;

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

      

      hence (( ProjMap J) . i) = ( proj (( Carrier J),i)) by Def2

      .= ( proj (J,i)) by WAYBEL18:def 4;

    end;

    definition

      let I be non empty set;

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

      let f be one-to-oneI -valued Function;

      :: TOPS_5:def4

      func product_basis_selector (J,f) -> ManySortedSet of ( rng f) equals ((( ProjMap J) .:.: (I -indexing (f " ))) | ( rng f));

      coherence

      proof

        ( dom ((( ProjMap J) .:.: (I -indexing (f " ))) | ( rng f))) = (( dom (( ProjMap J) .:.: (I -indexing (f " )))) /\ ( rng f)) by RELAT_1: 61

        .= (I /\ ( rng f)) by PARTFUN1:def 2

        .= ( rng f) by XBOOLE_1: 28;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let I be non empty set;

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

      let f be empty one-to-oneI -valued Function;

      cluster ( product_basis_selector (J,f)) -> empty;

      coherence ;

    end

    theorem :: TOPS_5:54

    

     Th54: for I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for f be one-to-oneI -valued Function holds for i be Element of I st i in ( rng f) holds (( product_basis_selector (J,f)) . i) = (( proj (J,i)) .: ((f " ) . i))

    proof

      let I be non empty set;

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

      let f be one-to-oneI -valued Function;

      let i be Element of I;

      assume

       A1: i in ( rng f);

      then

       A2: i in ( dom (f " )) by FUNCT_1: 33;

      

      thus (( product_basis_selector (J,f)) . i) = ((( ProjMap J) .:.: (I -indexing (f " ))) . i) by A1, FUNCT_1: 49

      .= ((( ProjMap J) . i) .: ((I -indexing (f " )) . i)) by PBOOLE:def 20

      .= (( proj (J,i)) .: ((I -indexing (f " )) . i)) by Th53

      .= (( proj (J,i)) .: ((f " ) . i)) by A2, ALGSPEC1: 9;

    end;

    theorem :: TOPS_5:55

    

     Th55: for I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for f be one-to-oneI -valued Function st (f " ) is non-empty & ( dom f) c= ( bool ( product ( Carrier J))) holds ( product_basis_selector (J,f)) is non-empty

    proof

      let I be non empty set;

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

      let f be one-to-oneI -valued Function;

      assume

       A1: (f " ) is non-empty & ( dom f) c= ( bool ( product ( Carrier J)));

      assume ( product_basis_selector (J,f)) is non non-empty;

      then

      consider x be object such that

       A2: x in ( dom ( product_basis_selector (J,f))) and

       A3: (( product_basis_selector (J,f)) . x) is empty by FUNCT_1:def 9;

      

       A4: x in ( rng f) by A2;

      then

      reconsider i = x as Element of I;

      (( proj (J,i)) .: ((f " ) . i)) is empty by A3, A2, Th54;

      then ( dom ( proj (J,i))) misses ((f " ) . i) by RELAT_1: 118;

      then ( dom ( proj (( Carrier J),i))) misses ((f " ) . i) by WAYBEL18:def 4;

      then

       A5: ( product ( Carrier J)) misses ((f " ) . i) by CARD_3:def 16;

      

       A6: ( rng (f " )) c= ( bool ( product ( Carrier J))) by A1, FUNCT_1: 33;

      i in ( dom (f " )) by A4, FUNCT_1: 33;

      then ((f " ) . i) in ( rng (f " )) by FUNCT_1: 3;

      hence contradiction by A1, A5, A6, XBOOLE_1: 67;

    end;

    theorem :: TOPS_5:56

    

     Th56: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds {} in ( product_prebasis J)

    proof

      let I be non empty set;

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

      set P = the empty 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) & P = ( product (( Carrier J) +* (i,V)))

      proof

        set i = the Element of I;

        set V = the empty Subset of (J . i);

        take i, (J . i), V;

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

        hence thesis by Th36;

      end;

      hence thesis by WAYBEL18:def 2;

    end;

    theorem :: TOPS_5:57

    

     Th57: for I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for P be non empty Subset of ( product ( Carrier J)) st P in ( product_prebasis J) holds ex i be Element of I st (( proj (J,i)) .: P) is open & for j be Element of I st j <> i holds (( proj (J,j)) .: P) = ( [#] (J . j))

    proof

      let I be non empty set;

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

      let P be non empty Subset of ( product ( Carrier J));

      assume P in ( product_prebasis J);

      then

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

       A1: i in I & V is open & T = (J . i) and

       A2: P = ( product (( Carrier J) +* (i,V))) by WAYBEL18:def 2;

      reconsider i as Element of I by A1;

      reconsider V as Subset of (J . i) by A1;

      take i;

      

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

      

       a4: ( rng ( proj (J,i))) = the carrier of (J . i) by Th52;

      (( proj (J,i)) .: P) = (( proj (J,i)) .: (( proj (J,i)) " V)) by A2, WAYBEL18: 4;

      hence (( proj (J,i)) .: P) is open by A1, a4, FUNCT_1: 77;

      let j be Element of I;

      assume

       A5: j <> i;

      for x be object holds x in (( proj (J,j)) .: P) iff x in ( [#] (J . j))

      proof

        let x be object;

        hereby

          assume x in (( proj (J,j)) .: P);

          then

          consider y be object such that

           A6: y in ( dom ( proj (J,j))) & y in P & x = (( proj (J,j)) . y) by FUNCT_1:def 6;

          consider g be Function such that

           A7: y = g & ( dom g) = ( dom (( Carrier J) +* (i,V))) and

           A8: for z be object st z in ( dom (( Carrier J) +* (i,V))) holds (g . z) in ((( Carrier J) +* (i,V)) . z) by A2, A6, CARD_3:def 5;

          j in ( dom ( Carrier J)) by A3;

          then

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

          x = (g . j) by A6, A7, YELLOW17: 8;

          then x in ((( Carrier J) +* (i,V)) . j) by A8, A9;

          then x in (( Carrier J) . j) by A5, FUNCT_7: 32;

          hence x in ( [#] (J . j)) by PENCIL_3: 7;

        end;

        assume x in ( [#] (J . j));

        then x in (( Carrier J) . j) by PENCIL_3: 7;

        then

         A10: x in ((( Carrier J) +* (i,V)) . j) by A5, FUNCT_7: 32;

        set g0 = the Element of ( product (( Carrier J) +* (i,V)));

        set g = (g0 +* (j,x));

        

         a11: (( Carrier J) . i) = ( [#] (J . i)) by PENCIL_3: 7

        .= the carrier of (J . i) by STRUCT_0:def 3;

        consider g00 be Function such that

         A12: g0 = g00 & ( dom g00) = ( dom (( Carrier J) +* (i,V))) and

         A13: for z be object st z in ( dom (( Carrier J) +* (i,V))) holds (g00 . z) in ((( Carrier J) +* (i,V)) . z) by A2, CARD_3:def 5;

        ex f be Function st g = f & ( dom f) = ( dom (( Carrier J) +* (i,V))) & for z be object st z in ( dom (( Carrier J) +* (i,V))) holds (f . z) in ((( Carrier J) +* (i,V)) . z)

        proof

          take g;

          thus g = g & ( dom g) = ( dom (( Carrier J) +* (i,V))) by A12, FUNCT_7: 30;

          let z be object;

          assume

           A15: z in ( dom (( Carrier J) +* (i,V)));

          z <> j implies (g . z) = (g0 . z) by FUNCT_7: 32;

          hence thesis by A10, A12, A13, A15, FUNCT_7: 31;

        end;

        then

         A16: g in ( product (( Carrier J) +* (i,V))) by CARD_3:def 5;

        

         a17: ( product (( Carrier J) +* (i,V))) c= ( product ( Carrier J)) by A3, a11, Th39;

        then g in ( product ( Carrier J)) by A16;

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

        then

         A18: g in ( dom ( proj (J,j))) by WAYBEL18:def 4;

        

         A19: j in ( dom ( Carrier J)) by A3;

        

         A20: g is Element of ( product J) by a17, A16, WAYBEL18:def 3;

        j in ( dom g0) by A12, A19, FUNCT_7: 30;

        

        then x = (g . j) by FUNCT_7: 31

        .= (( proj (J,j)) . g) by A20, YELLOW17: 8;

        hence thesis by A2, A16, A18, FUNCT_1:def 6;

      end;

      hence (( proj (J,j)) .: P) = ( [#] (J . j)) by TARSKI: 2;

    end;

    theorem :: TOPS_5:58

    

     Th58: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be non empty Subset of ( product ( Carrier J)) st P in ( product_prebasis J) holds (for j be Element of I holds (( proj (J,j)) .: P) is open) & ex i be Element of I st for j be Element of I st j <> i holds (( proj (J,j)) .: P) = ( [#] (J . j))

    proof

      let I be non empty set;

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

      let P be non empty Subset of ( product ( Carrier J));

      assume P in ( product_prebasis J);

      then

      consider i be Element of I such that

       A1: (( proj (J,i)) .: P) is open and

       A2: for j be Element of I st j <> i holds (( proj (J,j)) .: P) = ( [#] (J . j)) by Th57;

      hereby

        let j be Element of I;

        j <> i implies (( proj (J,j)) .: P) = ( [#] (J . j)) by A2;

        hence (( proj (J,j)) .: P) is open by A1;

      end;

      take i;

      thus thesis by A2;

    end;

    theorem :: TOPS_5:59

    

     Th59: for I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for f be one-to-oneI -valued Function holds for X be Subset-Family of ( product ( Carrier J)) st X c= ( product_prebasis J) & ( dom f) = X & (f " ) is non-empty & for A be Subset of ( product ( Carrier J)) st A in X holds (( proj (J,(f /. A))) .: A) is open holds for i be Element of I holds ( not i in ( rng f) implies (( proj (J,i)) .: ( product (( Carrier J) +* ( product_basis_selector (J,f))))) = ( [#] (J . i))) & (i in ( rng f) implies (( proj (J,i)) .: ( product (( Carrier J) +* ( product_basis_selector (J,f))))) is open)

    proof

      let I be non empty set;

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

      let f be one-to-oneI -valued Function;

      let X be Subset-Family of ( product ( Carrier J));

      set g = ( product_basis_selector (J,f));

      set P = ( product (( Carrier J) +* g));

      assume that

       A1: X c= ( product_prebasis J) & ( dom f) = X & (f " ) is non-empty and

       A2: for A be Subset of ( product ( Carrier J)) st A in X holds (( proj (J,(f /. A))) .: A) is open;

      let i be Element of I;

      

       A3: ( dom ( Carrier J)) = I & ( dom g) = ( rng f) by PARTFUN1:def 2;

      

       A4: g is non-empty by A1, Th55;

       A6:

      now

        let j be object;

        assume

         a7: j in ( dom g);

        then j in ( rng f);

        then

        reconsider k = j as Element of I;

        (g . j) = (( proj (J,k)) .: ((f " ) . k)) by a7, Th54;

        then (g . j) c= the carrier of (J . k);

        then (g . j) c= ( [#] (J . k)) by STRUCT_0:def 3;

        hence (g . j) c= (( Carrier J) . j) by PENCIL_3: 7;

      end;

      thus not i in ( rng f) implies (( proj (J,i)) .: P) = ( [#] (J . i))

      proof

        assume not i in ( rng f);

        then

         A8: i in (( dom ( Carrier J)) \ ( dom g)) by A3, XBOOLE_0:def 5;

        

        thus (( proj (J,i)) .: P) = (( proj (( Carrier J),i)) .: P) by WAYBEL18:def 4

        .= (( Carrier J) . i) by A3, A4, A6, A8, Th24

        .= ( [#] (J . i)) by PENCIL_3: 7;

      end;

      assume

       A9: i in ( rng f);

      

       A11: (( proj (J,i)) .: P) = (( proj (( Carrier J),i)) .: P) by WAYBEL18:def 4

      .= (g . i) by A4, A3, A6, A9, Th25

      .= (( proj (J,i)) .: ((f " ) . i)) by A9, Th54;

      

       A12: (f . ((f " ) . i)) = i by A9, FUNCT_1: 35;

      i in ( dom (f " )) by A9, FUNCT_1: 33;

      then

       a13: ((f " ) . i) in ( rng (f " )) by FUNCT_1: 3;

      then

       A13: ((f " ) . i) in ( dom f) by FUNCT_1: 33;

      ((f " ) . i) in X by A1, a13, FUNCT_1: 33;

      then

      reconsider A = ((f " ) . i) as Subset of ( product ( Carrier J));

      (f /. A) = i by A12, A13, PARTFUN1:def 6;

      hence thesis by A2, A11, A13, A1;

    end;

    theorem :: TOPS_5:60

    

     Th60: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for f be one-to-oneI -valued Function holds for X be Subset-Family of ( product ( Carrier J)) st X c= ( product_prebasis J) & ( dom f) = X & (f " ) is non-empty & for A be Subset of ( product ( Carrier J)) st A in X holds (( proj (J,(f /. A))) .: A) is open holds for i be Element of I holds (( proj (J,i)) .: ( product (( Carrier J) +* ( product_basis_selector (J,f))))) is open & ( not i in ( rng f) implies (( proj (J,i)) .: ( product (( Carrier J) +* ( product_basis_selector (J,f))))) = ( [#] (J . i)))

    proof

      let I be non empty set;

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

      let f be one-to-oneI -valued Function;

      let X be Subset-Family of ( product ( Carrier J));

      set g = ( product_basis_selector (J,f));

      set P = ( product (( Carrier J) +* g));

      assume that

       A1: X c= ( product_prebasis J) & ( dom f) = X & (f " ) is non-empty and

       A2: for A be Subset of ( product ( Carrier J)) st A in X holds (( proj (J,(f /. A))) .: A) is open;

      let i be Element of I;

       not i in ( rng f) implies (( proj (J,i)) .: P) = ( [#] (J . i)) by A1, A2, Th59;

      hence thesis by A1, A2, Th59;

    end;

    

     Lm3: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) implies ex X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function st X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X & P = ( product (( Carrier J) +* ( product_basis_selector (J,f))))

    proof

      let I be non empty set;

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

      let P be Subset of ( product ( Carrier J));

      assume

       A1: P in ( FinMeetCl ( product_prebasis J));

      consider Y be Subset-Family of ( product ( Carrier J)) such that

       A2: Y c= ( product_prebasis J) & Y is finite & P = ( Intersect Y) by A1, CANTOR_1:def 3;

      per cases ;

        suppose

         A3: Y is non empty & ( meet Y) <> {} ;

        then

         A4: P = ( meet Y) by A2, SETFAM_1:def 9;

        defpred P[ object, object] means ex i be Element of I, B be Subset of (J . i) st $2 = i & B is open & $1 = ( product (( Carrier J) +* (i,B)));

        

         A5: for x be object st x in Y holds ex i be object st i in I & P[x, i]

        proof

          let x be object;

          assume x in Y;

          then

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

           A6: i in I & V is open & T = (J . i) & x = ( product (( Carrier J) +* (i,V))) by A2, WAYBEL18:def 2;

          take i;

          thus i in I by A6;

          reconsider j = i as Element of I by A6;

          reconsider V as Subset of (J . j) by A6;

          take j, V;

          thus thesis by A6;

        end;

        consider g be Function of Y, I such that

         A7: for x be object st x in Y holds P[x, (g . x)] from FUNCT_2:sch 1( A5);

        set X = { ( meet (g " {i})) where i be Element of I : (g " {i}) <> {} };

        X c= ( bool ( product ( Carrier J)))

        proof

          let x be object;

          assume x in X;

          then

          consider i be Element of I such that

           A8: x = ( meet (g " {i})) & (g " {i}) <> {} ;

          reconsider Z = (g " {i}) as Subset-Family of ( product ( Carrier J)) by XBOOLE_1: 1;

          ( meet Z) is Subset of ( product ( Carrier J));

          hence thesis by A8;

        end;

        then

        reconsider X as Subset-Family of ( product ( Carrier J));

        take X;

        defpred Q[ object, object] means ex i be Element of I st $2 = i & $1 = ( meet (g " {i})) & (g " {i}) <> {} ;

        

         A9: for x be object st x in X holds ex i be object st i in I & Q[x, i]

        proof

          let x be object;

          assume x in X;

          then

          consider i be Element of I such that

           A10: x = ( meet (g " {i})) & (g " {i}) <> {} ;

          take i;

          thus i in I;

          take i;

          thus thesis by A10;

        end;

        consider f be Function of X, I such that

         A11: for x be object st x in X holds Q[x, (f . x)] from FUNCT_2:sch 1( A9);

        

         A12: ( dom f) = X & ( rng f) c= I by FUNCT_2:def 1;

        for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A13: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          then

          consider i1 be Element of I such that

           A14: (f . x1) = i1 & x1 = ( meet (g " {i1})) & (g " {i1}) <> {} by A11;

          ex i2 be Element of I st (f . x2) = i2 & x2 = ( meet (g " {i2})) & (g " {i2}) <> {} by A11, A13;

          hence thesis by A13, A14;

        end;

        then

        reconsider f as one-to-oneI -valued Function by FUNCT_1:def 4;

        take f;

        

         A16: for i be Element of I, S be non empty set st (g " {i}) <> {} & S in (g " {i}) holds ex V be non empty open Subset of (J . i) st S = ( product (( Carrier J) +* (i,V)))

        proof

          let i be Element of I;

          let S be non empty set;

          assume

           a17: (g " {i}) <> {} & S in (g " {i});

          then

           A17: S in Y & (g . S) in {i} by FUNCT_2: 38;

          then

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

           A18: j in I & V is open & T = (J . j) and

           A19: S = ( product (( Carrier J) +* (j,V))) by A2, WAYBEL18:def 2;

          

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

          per cases ;

            suppose

             A21: V <> (( Carrier J) . j);

            

             A22: V is non empty by A19, a20, Th36, A18;

            

             A23: i = j

            proof

              (g . S) = i by A17, TARSKI:def 1;

              then

              consider k be Element of I, B be Subset of (J . k) such that

               A24: i = k & B is open and

               A25: S = ( product (( Carrier J) +* (k,B))) by A7, a17;

              B is non empty by a20, A25, Th36;

              hence thesis by A19, A18, a20, A21, A22, A24, A25, Th42;

            end;

            then

            reconsider V as non empty open Subset of (J . i) by A19, a20, Th36, A18;

            take V;

            thus thesis by A19, A23;

          end;

            suppose V = (( Carrier J) . j);

            

            then

             A26: S = ( product ( Carrier J)) by A19, FUNCT_7: 35

            .= ( product (( Carrier J) +* (i,(( Carrier J) . i)))) by FUNCT_7: 35;

            take ( [#] (J . i));

            thus thesis by A26, PENCIL_3: 7;

          end;

        end;

        

         A27: X is non empty

        proof

          

           A28: ex i be Element of I st (g " {i}) <> {}

          proof

            set A = the Element of Y;

            consider i be Element of I, B be Subset of (J . i) such that

             A29: (g . A) = i & B is open & A = ( product (( Carrier J) +* (i,B))) by A3, A7;

            take i;

            (g . A) in {i} by A29, TARSKI:def 1;

            hence (g " {i}) <> {} by A3, FUNCT_2: 38;

          end;

          ex x be object st x in X

          proof

            consider i be Element of I such that

             A30: (g " {i}) <> {} by A28;

            ( meet (g " {i})) in X by A30;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A31: for x be Element of X st x = ( meet (g " {(f . x)})) & (g " {(f . x)}) <> {} & x <> {} holds ex Z be Subset-Family of (J . ( In ((f . x),I))) st Z = { (( proj (J,( In ((f . x),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . x)}) } & Z is open & Z is finite & Z is non empty & x = ( product (( Carrier J) +* ((f . x),( meet Z))))

        proof

          let x be Element of X;

          set i = ( In ((f . x),I));

          

           a32: (f . x) in ( rng f) by A12, A27, FUNCT_1: 3;

          then

           A32: i = (f . x) by SUBSET_1:def 8;

          assume

           A33: x = ( meet (g " {(f . x)})) & (g " {(f . x)}) <> {} & x <> {} ;

          set Z = { (( proj (J,( In ((f . x),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . x)}) };

          Z c= ( bool the carrier of (J . i))

          proof

            let y be object;

            assume y in Z;

            then ex V be Subset of ( product ( Carrier J)) st y = (( proj (J,i)) .: V) & V in (g " {(f . x)});

            hence thesis;

          end;

          then

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

          take Z;

          thus Z = { (( proj (J,( In ((f . x),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . x)}) };

          for A be Subset of (J . i) holds A in Z implies A is open

          proof

            let A be Subset of (J . i);

            assume A in Z;

            then

            consider V be Subset of ( product ( Carrier J)) such that

             A35: A = (( proj (J,i)) .: V) & V in (g " {(f . x)});

            V in Y & (V is empty or V is non empty) by A35;

            hence thesis by A2, A35, Th58;

          end;

          hence Z is open by TOPS_2:def 1;

          defpred R[ object, object] means ex V be Subset of ( product ( Carrier J)) st $1 = V & $2 = (( proj (J,i)) .: V);

          

           A37: for y,z1,z2 be object st y in (g " {i}) & R[y, z1] & R[y, z2] holds z1 = z2;

          

           A38: for y be object st y in (g " {i}) holds ex z be object st R[y, z]

          proof

            let y be object;

            assume y in (g " {i});

            then y in Y;

            then

            reconsider V = y as Subset of ( product ( Carrier J));

            take (( proj (J,i)) .: V), V;

            thus thesis;

          end;

          consider h be Function such that

           A39: ( dom h) = (g " {i}) & for y be object st y in (g " {i}) holds R[y, (h . y)] from FUNCT_1:sch 2( A37, A38);

          

           a45: for y be object holds y in ( rng h) iff y in Z

          proof

            let y be object;

            hereby

              assume y in ( rng h);

              then

              consider z be object such that

               A40: z in ( dom h) & y = (h . z) by FUNCT_1:def 3;

              ex V be Subset of ( product ( Carrier J)) st z = V & (h . z) = (( proj (J,i)) .: V) by A39, A40;

              hence y in Z by A32, A39, A40;

            end;

            assume y in Z;

            then

            consider V be Subset of ( product ( Carrier J)) such that

             A42: y = (( proj (J,i)) .: V) & V in (g " {(f . x)});

            

             A43: V in ( dom h) by a32, SUBSET_1:def 8, A39, A42;

            ex V0 be Subset of ( product ( Carrier J)) st V = V0 & (h . V) = (( proj (J,i)) .: V0) by A32, A39, A42;

            hence thesis by A42, A43, FUNCT_1:def 3;

          end;

          then ( rng h) = Z by TARSKI: 2;

          hence Z is finite by A2, A39, FINSET_1: 8;

          (h . the Element of (g " {(f . x)})) in ( rng h) by A32, A33, A39, FUNCT_1: 3;

          hence

           A46: Z is non empty by a45;

          

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

          then

           A47: i in ( dom ( Carrier J));

          for y be object holds y in ( meet (g " {i})) iff y in ( product (( Carrier J) +* (i,( meet Z))))

          proof

            let y be object;

            hereby

              assume

               A49: y in ( meet (g " {i}));

              set S0 = the Element of (g " {i});

              S0 is non empty by A32, A33, A49, SETFAM_1:def 1;

              then

              consider V0 be non empty open Subset of (J . i) such that

               A50: S0 = ( product (( Carrier J) +* (i,V0))) by A16, A32, A33;

              y in ( product (( Carrier J) +* (i,V0))) by A32, A33, A49, A50, SETFAM_1:def 1;

              then

              consider f0 be Function such that

               A51: y = f0 & ( dom f0) = ( dom (( Carrier J) +* (i,V0))) and

               A52: for z be object st z in ( dom (( Carrier J) +* (i,V0))) holds (f0 . z) in ((( Carrier J) +* (i,V0)) . z) by CARD_3:def 5;

              now

                take f0;

                thus y = f0 by A51;

                

                thus ( dom f0) = ( dom ( Carrier J)) by A51, FUNCT_7: 30

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

                let z be object;

                assume z in ( dom (( Carrier J) +* (i,( meet Z))));

                then

                 A53: z in ( dom ( Carrier J)) by FUNCT_7: 30;

                per cases ;

                  suppose

                   A54: z <> i;

                  

                  then

                   A55: ((( Carrier J) +* (i,( meet Z))) . z) = (( Carrier J) . z) by FUNCT_7: 32

                  .= ((( Carrier J) +* (i,V0)) . z) by A54, FUNCT_7: 32;

                  z in ( dom (( Carrier J) +* (i,V0))) by A53, FUNCT_7: 30;

                  hence (f0 . z) in ((( Carrier J) +* (i,( meet Z))) . z) by A52, A55;

                end;

                  suppose

                   A56: z = i;

                  then

                   A57: ((( Carrier J) +* (i,( meet Z))) . z) = ( meet Z) by A53, FUNCT_7: 31;

                  for S be set st S in Z holds (f0 . z) in S

                  proof

                    let S be set;

                    assume S in Z;

                    then

                    consider S1 be Subset of ( product ( Carrier J)) such that

                     A58: S = (( proj (J,i)) .: S1) & S1 in (g " {(f . x)});

                    S1 is non empty by A32, A49, A58, SETFAM_1:def 1;

                    then

                    consider V1 be non empty open Subset of (J . i) such that

                     A59: S1 = ( product (( Carrier J) +* (i,V1))) by A16, A32, A58;

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

                    then V1 c= ( [#] (J . i)) by STRUCT_0:def 3;

                    then

                     A60: V1 c= (( Carrier J) . i) by PENCIL_3: 7;

                    ( proj (J,i)) = ( proj (( Carrier J),i)) by WAYBEL18:def 4;

                    then

                     A61: S = V1 by A58, A59, A60, a47, Th43;

                    y in S1 by A32, A49, A58, SETFAM_1:def 1;

                    then

                    consider f1 be Function such that

                     A62: y = f1 & ( dom f1) = ( dom (( Carrier J) +* (i,V1))) and

                     A63: for a be object st a in ( dom (( Carrier J) +* (i,V1))) holds (f1 . a) in ((( Carrier J) +* (i,V1)) . a) by A59, CARD_3:def 5;

                    i in ( dom (( Carrier J) +* (i,V1))) by A47, FUNCT_7: 30;

                    then (f1 . i) in ((( Carrier J) +* (i,V1)) . i) by A63;

                    hence (f0 . z) in S by A51, A56, A61, A62, a47, FUNCT_7: 31;

                  end;

                  hence (f0 . z) in ((( Carrier J) +* (i,( meet Z))) . z) by A57, A46, SETFAM_1:def 1;

                end;

              end;

              hence y in ( product (( Carrier J) +* (i,( meet Z)))) by CARD_3:def 5;

            end;

            assume

             A64: y in ( product (( Carrier J) +* (i,( meet Z))));

            for S be set st S in (g " {i}) holds y in S

            proof

              let S be set;

              assume

               A65: S in (g " {i});

              S is non empty by A32, A33, A65, SETFAM_1: 4;

              then

              consider V be non empty open Subset of (J . i) such that

               A66: S = ( product (( Carrier J) +* (i,V))) by A16, A65;

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

              then V c= ( [#] (J . i)) by STRUCT_0:def 3;

              then

               A67: V c= (( Carrier J) . i) by PENCIL_3: 7;

              ( proj (J,i)) = ( proj (( Carrier J),i)) by WAYBEL18:def 4;

              then

               A68: (( proj (J,i)) .: S) = V by a47, A66, A67, Th43;

              S in Y by A65;

              then V in Z by A32, A65, A68;

              then ( product (( Carrier J) +* (i,( meet Z)))) c= ( product (( Carrier J) +* (i,V))) by a47, Th38, SETFAM_1: 3;

              hence y in S by A64, A66;

            end;

            hence y in ( meet (g " {i})) by A32, A33, SETFAM_1:def 1;

          end;

          hence x = ( product (( Carrier J) +* ((f . x),( meet Z)))) by A32, A33, TARSKI: 2;

        end;

        for x be object holds x in X implies x in ( product_prebasis J)

        proof

          let x be object;

          assume

           A69: x in X;

          per cases ;

            suppose

             A70: x <> {} ;

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

            proof

              consider i be Element of I such that

               A71: (f . x) = i & x = ( meet (g " {i})) & (g " {i}) <> {} by A11, A69;

              consider Z be Subset-Family of (J . ( In ((f . x),I))) such that Z = { (( proj (J,( In ((f . x),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . x)}) } and

               A72: Z is open & Z is finite & Z is non empty and

               A73: x = ( product (( Carrier J) +* ((f . x),( meet Z)))) by A31, A69, A70, A71;

              set W = ( meet Z);

              take i, (J . ( In ((f . x),I))), W;

              thus thesis by A71, A73, A72, TOPS_2: 20;

            end;

            hence thesis by A69, WAYBEL18:def 2;

          end;

            suppose x = {} ;

            hence thesis by Th56;

          end;

        end;

        hence X c= ( product_prebasis J) by TARSKI:def 3;

        for x be object holds x in ( meet X) iff x in ( meet Y)

        proof

          let x be object;

          hereby

            assume

             A74: x in ( meet X);

            for Sy be set st Sy in Y holds x in Sy

            proof

              let Sy be set;

              assume

               A75: Sy in Y;

              then

              consider i be Element of I, B be Subset of (J . i) such that

               A76: (g . Sy) = i & B is open & Sy = ( product (( Carrier J) +* (i,B))) by A7;

              (g . Sy) in {i} by A76, TARSKI:def 1;

              then

               A77: Sy in (g " {i}) by A75, FUNCT_2: 38;

              then ( meet (g " {i})) in X;

              then

               A78: x in ( meet (g " {i})) by A74, SETFAM_1:def 1;

              ( meet (g " {i})) c= Sy by A77, SETFAM_1: 3;

              hence x in Sy by A78;

            end;

            hence x in ( meet Y) by A3, SETFAM_1:def 1;

          end;

          assume

           A79: x in ( meet Y);

          for Sx be set st Sx in X holds x in Sx

          proof

            let Sx be set;

            assume Sx in X;

            then

            consider i be Element of I such that

             A80: Sx = ( meet (g " {i})) & (g " {i}) <> {} ;

            for A be set st A in (g " {i}) holds x in A by A79, SETFAM_1:def 1;

            hence x in Sx by A80, SETFAM_1:def 1;

          end;

          hence x in ( meet X) by A27, SETFAM_1:def 1;

        end;

        then

         A81: ( meet X) = ( meet Y) by TARSKI: 2;

        thus X is finite

        proof

          set S = { (g " {i}) where i be Element of I : i in ( rng g) };

          

           a82: S is a_partition of Y by Th5;

          defpred R[ object, object] means ex M be set st $1 = M & $2 = ( meet M);

          

           A83: for A be object st A in S holds ex B be object st B in X & R[A, B]

          proof

            let A be object;

            assume A in S;

            then

            consider i be Element of I such that

             A84: A = (g " {i}) & i in ( rng g);

            take ( meet (g " {i}));

            consider x be object such that

             A85: x in Y & (g . x) = i by A84, FUNCT_2: 11;

            i in {i} by TARSKI:def 1;

            then x in (g " {i}) by A85, FUNCT_2: 38;

            hence ( meet (g " {i})) in X;

            take (g " {i});

            thus thesis by A84;

          end;

          consider h be Function of S, X such that

           A86: for A be object st A in S holds R[A, (h . A)] from FUNCT_2:sch 1( A83);

          for B be object st B in X holds ex A be object st A in S & B = (h . A)

          proof

            let B be object;

            assume B in X;

            then

            consider i be Element of I such that

             A87: B = ( meet (g " {i})) & (g " {i}) <> {} ;

            take (g " {i});

            consider x be object such that

             A88: x in (g " {i}) by A87, XBOOLE_0:def 1;

            x in Y & (g . x) in {i} by A88, FUNCT_2: 38;

            then

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

            ( dom g) = Y by FUNCT_2:def 1;

            then i in ( rng g) by A88, A90, FUNCT_1:def 3;

            hence (g " {i}) in S;

            then ex M be set st (g " {i}) = M & (h . (g " {i})) = ( meet M) by A86;

            hence thesis by A87;

          end;

          then ( rng h) = X by FUNCT_2: 10;

          hence X is finite by a82, A2;

        end;

        thus P = ( Intersect X) by A4, A27, A81, SETFAM_1:def 9;

        thus ( dom f) = X by FUNCT_2:def 1;

        set F = (( Carrier J) +* ( product_basis_selector (J,f)));

        for x be object holds x in ( meet X) iff x in ( product F)

        proof

          let x be object;

          

           A92: I = (I \/ ( rng f)) by XBOOLE_1: 12

          .= (( dom ( Carrier J)) \/ ( rng f)) by PARTFUN1:def 2

          .= (( dom ( Carrier J)) \/ ( dom ( product_basis_selector (J,f)))) by PARTFUN1:def 2

          .= ( dom F) by FUNCT_4:def 1;

          hereby

            assume

             A93: x in ( meet X);

            consider A0 be object such that

             A94: A0 in X by A27, XBOOLE_0:def 1;

            reconsider A0 as set by TARSKI: 1;

            consider i0 be Element of I such that

             A95: (f . A0) = i0 & A0 = ( meet (g " {i0})) & (g " {i0}) <> {} by A11, A94;

            A0 <> {} by A3, A81, A94, SETFAM_1: 4;

            then

            consider Z0 be Subset-Family of (J . ( In ((f . A0),I))) such that Z0 = { (( proj (J,( In ((f . A0),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . A0)}) } and Z0 is open & Z0 is finite & Z0 is non empty and

             A96: A0 = ( product (( Carrier J) +* ((f . A0),( meet Z0)))) by A31, A94, A95;

            x in A0 by A93, A94, SETFAM_1:def 1;

            then

            consider h be Function such that

             A97: x = h & ( dom h) = ( dom (( Carrier J) +* ((f . A0),( meet Z0)))) and

             A98: for y be object st y in ( dom (( Carrier J) +* ((f . A0),( meet Z0)))) holds (h . y) in ((( Carrier J) +* ((f . A0),( meet Z0))) . y) by A96, CARD_3:def 5;

            

             A99: ( dom h) = I by A97, PARTFUN1:def 2;

            

             A100: ( dom h) = ( dom F) by A92, A97, PARTFUN1:def 2;

            for y be object st y in ( dom F) holds (h . y) in (F . y)

            proof

              let y be object;

              assume y in ( dom F);

              then

              reconsider i = y as Element of I by A92;

              i in ( dom h) by A99;

              then

               A101: i in ( dom ( Carrier J)) by A97, FUNCT_7: 30;

              per cases ;

                suppose

                 A102: y in ( rng f);

                then y in ( dom ( product_basis_selector (J,f))) by PARTFUN1:def 2;

                then (F . y) = (( product_basis_selector (J,f)) . i) by FUNCT_4: 13;

                then

                 A103: (F . y) = (( proj (J,i)) .: ((f " ) . i)) by A102, Th54;

                consider A be object such that

                 A104: A in X & (f . A) = i by A102, FUNCT_2: 11;

                reconsider A as set by TARSKI: 1;

                consider j be Element of I such that

                 A105: (f . A) = j & A = ( meet (g " {j})) & (g " {j}) <> {} by A11, A104;

                A <> {} by A3, A81, A104, SETFAM_1: 4;

                then

                consider Z be Subset-Family of (J . ( In ((f . A),I))) such that Z = { (( proj (J,( In ((f . A),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . A)}) } and Z is open & Z is finite & Z is non empty and

                 A106: A = ( product (( Carrier J) +* ((f . A),( meet Z)))) by A31, A104, A105;

                reconsider Z as Subset-Family of (J . i) by A104;

                

                 a107: h in A by A93, A97, A104, SETFAM_1:def 1;

                ( dom (( Carrier J) +* ((f . A),( meet Z)))) = I by PARTFUN1:def 2;

                then (h . i) in ((( Carrier J) +* ((f . A),( meet Z))) . i) by a107, A106, CARD_3: 9;

                then

                 A108: (h . i) in ( meet Z) by A104, A101, FUNCT_7: 31;

                ex z be object st z in ( dom ( proj (J,i))) & z in ( meet (g " {i})) & (( proj (J,i)) . z) = (h . i)

                proof

                  set z0 = the Element of ( product ( Carrier J));

                  set z = (z0 +* (i,(h . i)));

                  take z;

                  ( meet Z) c= the carrier of (J . i);

                  then ( meet Z) c= ( [#] (J . i)) by STRUCT_0:def 3;

                  then

                   A109: ( meet Z) c= (( Carrier J) . i) by PENCIL_3: 7;

                  

                   A110: z in ( product (( Carrier J) +* (i,( meet Z)))) by A101, A108, Th37;

                  ( product (( Carrier J) +* (i,( meet Z)))) c= ( product ( Carrier J)) by A101, A109, Th39;

                  then z in ( product ( Carrier J)) by A110;

                  then

                   A111: z in ( dom ( proj (( Carrier J),i))) by CARD_3:def 16;

                  hence z in ( dom ( proj (J,i))) & z in ( meet (g " {i})) by A104, A105, A106, A101, A108, Th37, WAYBEL18:def 4;

                  

                   A112: i in ( dom z0) by A101, CARD_3: 9;

                  

                  thus (( proj (J,i)) . z) = (( proj (( Carrier J),i)) . z) by WAYBEL18:def 4

                  .= (z . i) by A111, CARD_3:def 16

                  .= (h . i) by A112, FUNCT_7: 31;

                end;

                then (h . i) in (( proj (J,i)) .: ( meet (g " {i}))) by FUNCT_1:def 6;

                hence (h . y) in (F . y) by A103, A105, A12, A104, FUNCT_1: 34;

              end;

                suppose not y in ( rng f);

                then not y in ( dom ( product_basis_selector (J,f)));

                then

                 A114: (F . y) = (( Carrier J) . y) by FUNCT_4: 11;

                reconsider Z0 as Subset-Family of (J . i0) by A95;

                ( meet Z0) c= the carrier of (J . i0);

                then ( meet Z0) c= ( [#] (J . i0)) by STRUCT_0:def 3;

                then

                 A115: ( meet Z0) c= (( Carrier J) . i0) by PENCIL_3: 7;

                i0 in I;

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

                then

                 A116: ( product (( Carrier J) +* (i0,( meet Z0)))) c= ( product ( Carrier J)) by A115, Th39;

                h in ( product (( Carrier J) +* (i0,( meet Z0)))) by A95, A97, A98, CARD_3: 9;

                hence (h . y) in (F . y) by A114, A101, A116, CARD_3: 9;

              end;

            end;

            hence x in ( product F) by A97, A100, CARD_3:def 5;

          end;

          assume x in ( product F);

          then

          consider h be Function such that

           A117: h = x & ( dom h) = ( dom F) and

           A118: for y be object st y in ( dom F) holds (h . y) in (F . y) by CARD_3:def 5;

          for A be set st A in X holds h in A

          proof

            let A be set;

            assume

             A119: A in X;

            then

            consider i be Element of I such that

             A120: (f . A) = i & A = ( meet (g " {i})) & (g " {i}) <> {} by A11;

            

             A121: ((f " ) . i) = A by A12, A119, A120, FUNCT_1: 34;

            A <> {} by A3, A81, A119, SETFAM_1: 4;

            then

            consider Z be Subset-Family of (J . ( In ((f . A),I))) such that

             A122: Z = { (( proj (J,( In ((f . A),I)))) .: V) where V be Subset of ( product ( Carrier J)) : V in (g " {(f . A)}) } and Z is open & Z is finite & Z is non empty and

             A124: A = ( product (( Carrier J) +* ((f . A),( meet Z)))) by A31, A119, A120;

            

             A125: ( dom h) = ( dom (( Carrier J) +* ((f . A),( meet Z)))) by A92, A117, PARTFUN1:def 2;

            for y be object st y in ( dom (( Carrier J) +* ((f . A),( meet Z)))) holds (h . y) in ((( Carrier J) +* ((f . A),( meet Z))) . y)

            proof

              let y be object;

              assume

               A126: y in ( dom (( Carrier J) +* ((f . A),( meet Z))));

              per cases ;

                suppose y <> i;

                then

                 A127: ((( Carrier J) +* ((f . A),( meet Z))) . y) = (( Carrier J) . y) by A120, FUNCT_7: 32;

                

                 A128: y in ( dom ( Carrier J)) by A126, FUNCT_7: 30;

                

                 A129: (h . y) in (F . y) by A92, A118, A126;

                per cases ;

                  suppose

                   A130: y in ( rng f);

                  then

                  reconsider i0 = y as Element of I;

                  y in ( dom ( product_basis_selector (J,f))) by A130, PARTFUN1:def 2;

                  

                  then (F . y) = (( product_basis_selector (J,f)) . i0) by FUNCT_4: 13

                  .= (( proj (J,i0)) .: ((f " ) . i0)) by A130, Th54;

                  then (F . y) c= ( rng ( proj (J,i0))) by RELAT_1: 111;

                  then (F . y) c= ( rng ( proj (( Carrier J),i0))) by WAYBEL18:def 4;

                  then (F . y) c= (( Carrier J) . i0) by A128, YELLOW17: 3;

                  hence thesis by A127, A129;

                end;

                  suppose not y in ( rng f);

                  then not y in ( dom ( product_basis_selector (J,f)));

                  hence thesis by A127, A129, FUNCT_4: 11;

                end;

              end;

                suppose

                 A131: y = i;

                i in I;

                then

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

                

                 A133: i in ( rng f) by A12, A119, A120, FUNCT_1:def 3;

                then i in ( dom ( product_basis_selector (J,f))) by PARTFUN1:def 2;

                

                then

                 A134: (F . i) = (( product_basis_selector (J,f)) . i) by FUNCT_4: 13

                .= (( proj (J,i)) .: ( meet (g " {i}))) by A120, A121, A133, Th54;

                reconsider G = (g " {i}) as Subset-Family of ( product ( Carrier J)) by XBOOLE_1: 1;

                (h . i) in (( proj (J,i)) .: ( meet (g " {i}))) by A92, A118, A134;

                then (h . i) in ( meet { (( proj (J,i)) .: B) where B be Subset of ( product ( Carrier J)) : B in G }) by Th3, TARSKI:def 3;

                hence thesis by A131, a132, FUNCT_7: 31, A120, A122;

              end;

            end;

            hence h in A by A124, A125, CARD_3: 9;

          end;

          hence thesis by A27, A117, SETFAM_1:def 1;

        end;

        hence thesis by A4, A81, TARSKI: 2;

      end;

        suppose

         A136: Y is empty;

        reconsider f = the empty Function as one-to-oneI -valued Function by XBOOLE_1: 2, RELAT_1: 38, RELAT_1:def 19;

        take Y, f;

        thus Y c= ( product_prebasis J) & Y is finite & P = ( Intersect Y) by A2;

        thus ( dom f) = Y by A136;

        ( product_basis_selector (J,f)) is empty;

        hence thesis by A2, A136, SETFAM_1:def 9;

      end;

        suppose Y is non empty & ( meet Y) = {} ;

        then

         A138: P = {} by A2, SETFAM_1:def 9;

        set i = the Element of I;

        set V = the empty Subset of (J . i);

        

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

        then

         A140: ( product (( Carrier J) +* (i,V))) = {} by Th36;

        then ( product (( Carrier J) +* (i,V))) in ( product_prebasis J) by Th56;

        then

        reconsider A = ( product (( Carrier J) +* (i,V))) as Subset of ( product ( Carrier J));

        set X = {A};

        set f = (A .--> i);

        take X, f;

        thus X c= ( product_prebasis J) & X is finite by A140, Th56, ZFMISC_1: 31;

         {} in X by A140, TARSKI:def 1;

        then ( meet X) = {} by SETFAM_1: 4;

        hence P = ( Intersect X) by A138, SETFAM_1:def 9;

        

        thus ( dom f) = ( dom ( {A} --> i)) by FUNCOP_1:def 9

        .= X;

        set F = (( Carrier J) +* ( product_basis_selector (J,f)));

        ex j be object st j in ( dom F) & (F . j) = {}

        proof

          take i;

          i in (( dom ( Carrier J)) \/ ( dom ( product_basis_selector (J,f)))) by a139, XBOOLE_1: 7, TARSKI:def 3;

          hence i in ( dom F) by FUNCT_4:def 1;

          i in {i} by TARSKI:def 1;

          then i in ( rng ( {A} --> i)) by FUNCOP_1: 8;

          then

           A142: i in ( rng f) by FUNCOP_1:def 9;

          then i in ( dom ( product_basis_selector (J,f))) by PARTFUN1:def 2;

          

          hence (F . i) = (( product_basis_selector (J,f)) . i) by FUNCT_4: 13

          .= (( proj (J,i)) .: ((f " ) . i)) by A142, Th54

          .= (( proj (J,i)) .: ((i .--> A) . i)) by NECKLACE: 9

          .= (( proj (J,i)) .: A) by FUNCOP_1: 72

          .= {} by A140;

        end;

        then {} in ( rng F) by FUNCT_1:def 3;

        hence thesis by A138, CARD_3: 26;

      end;

    end;

    theorem :: TOPS_5:61

    for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) iff ex X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function st X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X & P = ( product (( Carrier J) +* ( product_basis_selector (J,f)))) by Lm3, CANTOR_1:def 3;

    theorem :: TOPS_5:62

    

     Th62: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be non empty Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) implies ex X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function st X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X & for i be Element of I holds (( proj (J,i)) .: P) is open & ( not i in ( rng f) implies (( proj (J,i)) .: P) = ( [#] (J . i)))

    proof

      let I be non empty set;

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

      let P be non empty Subset of ( product ( Carrier J));

      assume

       A1: P in ( FinMeetCl ( product_prebasis J));

      consider X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function such that

       A2: X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X and

       A3: P = ( product (( Carrier J) +* ( product_basis_selector (J,f)))) by A1, Lm3;

      take X, f;

      thus X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X by A2;

       A4:

      now

        let A be Subset of ( product ( Carrier J));

        assume

         A5: A in X;

        A is empty implies (( proj (J,(f /. A))) .: A) = ( {} (J . (f /. A)));

        hence (( proj (J,(f /. A))) .: A) is open by A2, A5, Th58;

      end;

      (f " ) is non-empty

      proof

        assume (f " ) is non non-empty;

        then {} in ( rng (f " )) by RELAT_1:def 9;

        then {} in X by A2, FUNCT_1: 33;

        then X is non empty & ( meet X) = {} by SETFAM_1: 4;

        hence contradiction by A2, SETFAM_1:def 9;

      end;

      hence thesis by A2, A3, A4, Th60;

    end;

    theorem :: TOPS_5:63

    

     Th63: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be non empty Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) implies ex I0 be finite Subset of I st for i be Element of I holds (( proj (J,i)) .: P) is open & ( not i in I0 implies (( proj (J,i)) .: P) = ( [#] (J . i)))

    proof

      let I be non empty set;

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

      let P be non empty Subset of ( product ( Carrier J));

      assume P in ( FinMeetCl ( product_prebasis J));

      then

      consider X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function such that

       A1: X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X and

       A2: for i be Element of I holds (( proj (J,i)) .: P) is open & ( not i in ( rng f) implies (( proj (J,i)) .: P) = ( [#] (J . i))) by Th62;

      reconsider I0 = ( rng f) as finite Subset of I by A1, FINSET_1: 8;

      take I0;

      thus thesis by A2;

    end;

    theorem :: TOPS_5:64

    

     Th64: for I be 1 -element set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for i be Element of I, P be Subset of ( product ( Carrier J)) holds P in ( product_prebasis J) iff ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V))

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      ( card I) = 1 by CARD_1:def 7;

      then

       A1: I = {i} by ORDERS_5: 2;

      the carrier of (J . i) = ( [#] (J . i)) by STRUCT_0:def 3

      .= (( Carrier J) . i) by PENCIL_3: 7;

      then

       A2: ( Carrier J) = ( {i} --> the carrier of (J . i)) by A1, Th7;

      let P be Subset of ( product ( Carrier J));

      hereby

        assume P in ( product_prebasis J);

        then

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

         A3: j in I & V is open & T = (J . j) and

         A4: P = ( product (( Carrier J) +* (j,V))) by WAYBEL18:def 2;

        

         A5: i = j by A1, A3, TARSKI:def 1;

        reconsider W = V as Subset of (J . i) by A1, A3, TARSKI:def 1;

        take W;

        thus W is open by A3, A5;

        

        thus P = ( product ((i .--> the carrier of (J . i)) +* (i,W))) by A2, A4, A5, FUNCOP_1:def 9

        .= ( product (i .--> W)) by Th44

        .= ( product ( {i} --> W)) by FUNCOP_1:def 9;

      end;

      given V be Subset of (J . i) such that

       A6: V is open & P = ( product ( {i} --> V));

      P = ( product (i .--> V)) by A6, FUNCOP_1:def 9

      .= ( product ((i .--> the carrier of (J . i)) +* (i,V))) by Th44

      .= ( product (( Carrier J) +* (i,V))) by A2, FUNCOP_1:def 9;

      hence thesis by A6, WAYBEL18:def 2;

    end;

    

     Lm4: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I, P be Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) implies ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V))

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      ( card I) = 1 by CARD_1:def 7;

      then

       A1: I = {i} by ORDERS_5: 2;

      the carrier of (J . i) = ( [#] (J . i)) by STRUCT_0:def 3

      .= (( Carrier J) . i) by PENCIL_3: 7;

      then

       A2: ( Carrier J) = ( {i} --> the carrier of (J . i)) by A1, Th7;

      let P be Subset of ( product ( Carrier J));

      assume P in ( FinMeetCl ( product_prebasis J));

      then

      consider X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function such that

       A3: X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X and

       A4: P = ( product (( Carrier J) +* ( product_basis_selector (J,f)))) by Lm3;

      set F = (( Carrier J) +* ( product_basis_selector (J,f)));

      per cases by A1, ZFMISC_1: 33;

        suppose ( rng f) = {} ;

        then

         a5: ( product_basis_selector (J,f)) = {} ;

        take ( [#] (J . i));

        thus thesis by a5, A2, A4, STRUCT_0:def 3;

      end;

        suppose

         A6: ( rng f) = {i};

        then

         A7: ( dom f) = {((f " ) . i)} by Th1;

        

         A8: i in ( rng f) by A6, TARSKI:def 1;

        

         A9: ((f " ) . i) in X by A3, A7, TARSKI:def 1;

        then

        reconsider V0 = ((f " ) . i) as Subset of ( product ( Carrier J));

        reconsider V = (( proj (J,i)) .: V0) as Subset of (J . i);

        take V;

        V0 is empty or V0 is non empty;

        hence V is open by A3, A9, Th58;

        

         A10: ( product_basis_selector (J,f)) = ( {i} --> (( product_basis_selector (J,f)) . i)) by A6, Th7

        .= ( {i} --> (( proj (J,i)) .: V0)) by A8, Th54;

        ( dom ( Carrier J)) = {i} by A1, PARTFUN1:def 2;

        then ( dom ( Carrier J)) = ( dom ( product_basis_selector (J,f))) by A6, PARTFUN1:def 2;

        hence thesis by A4, A10, FUNCT_4: 19;

      end;

    end;

    

     Lm5: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I, P be Subset of ( product ( Carrier J)) holds P in ( FinMeetCl ( product_prebasis J)) iff ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V))

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      let P be Subset of ( product ( Carrier J));

      thus P in ( FinMeetCl ( product_prebasis J)) implies ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V)) by Lm4;

      given V be Subset of (J . i) such that

       A2: V is open & P = ( product ( {i} --> V));

      P in ( product_prebasis J) by A2, Th64;

      hence thesis by TARSKI:def 3, CANTOR_1: 4;

    end;

    

     Lm6: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I, P be Subset of ( product ( Carrier J)) holds P in ( UniCl ( FinMeetCl ( product_prebasis J))) iff ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V))

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      ( card I) = 1 by CARD_1:def 7;

      then

       A1: I = {i} by ORDERS_5: 2;

      the carrier of (J . i) = ( [#] (J . i)) by STRUCT_0:def 3

      .= (( Carrier J) . i) by PENCIL_3: 7;

      then

       A2: ( Carrier J) = ( {i} --> the carrier of (J . i)) by A1, Th7;

      let P be Subset of ( product ( Carrier J));

      hereby

        assume P in ( UniCl ( FinMeetCl ( product_prebasis J)));

        then

        consider Y be Subset-Family of ( product ( Carrier J)) such that

         A3: Y c= ( FinMeetCl ( product_prebasis J)) & P = ( union Y) by CANTOR_1:def 1;

        defpred P[ object] means ex W be open Subset of (J . i) st W = $1 & ( product ( {i} --> W)) in Y;

        consider Z be Subset of ( bool the carrier of (J . i)) such that

         A4: for x be set holds x in Z iff x in ( bool the carrier of (J . i)) & P[x] from SUBSET_1:sch 1;

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

        set V = ( union Z);

        take V;

        

         A5: for W be Subset of (J . i) holds W in Z iff W is open & ( product ( {i} --> W)) in Y

        proof

          let W be Subset of (J . i);

          hereby

            assume W in Z;

            then ex W2 be open Subset of (J . i) st W2 = W & ( product ( {i} --> W2)) in Y by A4;

            hence W is open & ( product ( {i} --> W)) in Y;

          end;

          assume W is open & ( product ( {i} --> W)) in Y;

          hence thesis by A4;

        end;

        then for W be Subset of (J . i) holds W in Z implies W is open;

        hence V is open by TOPS_2:def 1, TOPS_2: 19;

        for x be object holds x in ( union Y) iff x in ( product ( {i} --> V))

        proof

          let x be object;

          hereby

            assume x in ( union Y);

            then

            consider K be set such that

             A7: x in K & K in Y by TARSKI:def 4;

            reconsider K as Subset of ( product ( Carrier J)) by A7;

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

             A8: L is open & K = ( product ( {i} --> L)) by A3, A7, Lm5;

            

             A9: L in Z by A5, A7, A8;

            

             A10: L is non empty

            proof

              assume L is empty;

              then ( dom ( {i} --> L)) = {i} & ( rng ( {i} --> L)) = { {} } by FUNCOP_1: 8;

              hence contradiction by A7, A8, Lm1;

            end;

            then

            consider y be Element of L such that

             A11: x = ( {i} --> y) by A7, A8, Th16;

            y in V by A9, A10, TARSKI:def 4;

            hence x in ( product ( {i} --> V)) by A11, Th16;

          end;

          assume

           A12: x in ( product ( {i} --> V));

          

           A13: V is non empty

          proof

            assume V is empty;

            then ( rng ( {i} --> V)) = { {} } by FUNCOP_1: 8;

            hence contradiction by A12, Lm1;

          end;

          then

          consider y be Element of V such that

           A14: x = ( {i} --> y) by A12, Th16;

          consider L be set such that

           A15: y in L & L in Z by A13, TARSKI:def 4;

          reconsider L as Subset of (J . i) by A15;

          reconsider K = ( product ( {i} --> L)) as Subset of ( product ( Carrier J)) by A2, Th14;

          

           A16: K in Y by A5, A15;

          x in K by A14, A15, Th16;

          hence thesis by A16, TARSKI:def 4;

        end;

        hence P = ( product ( {i} --> V)) by A3, TARSKI: 2;

      end;

      assume ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V));

      then P in ( FinMeetCl ( product_prebasis J)) by Lm5;

      hence thesis by CANTOR_1: 1, TARSKI:def 3;

    end;

    

     Lm7: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds ( UniCl ( FinMeetCl ( product_prebasis J))) = ( product_prebasis J)

    proof

      let I be 1 -element set;

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

      for x be object holds x in ( UniCl ( FinMeetCl ( product_prebasis J))) iff x in ( product_prebasis J)

      proof

        let x be object;

        set i = the Element of I;

        hereby

          assume

           A1: x in ( UniCl ( FinMeetCl ( product_prebasis J)));

          then

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

          ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V)) by A1, Lm6;

          hence x in ( product_prebasis J) by Th64;

        end;

        assume

         A2: x in ( product_prebasis J);

        then

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

        ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V)) by A2, Th64;

        hence thesis by Lm6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_5:65

    

     Th65: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds the topology of ( product J) = ( product_prebasis J)

    proof

      let I be 1 -element set;

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

      reconsider T = ( product J) as TopSpace;

      reconsider K = ( product_prebasis J) as Subset-Family of T by WAYBEL18:def 3;

      K is prebasis of T by WAYBEL18:def 3;

      then

       A1: ( UniCl ( FinMeetCl K)) = the topology of T by YELLOW_9: 22, YELLOW_9: 23;

      ( FinMeetCl K) = ( FinMeetCl ( product_prebasis J)) by WAYBEL18:def 3;

      then ( UniCl ( FinMeetCl K)) = ( UniCl ( FinMeetCl ( product_prebasis J))) by WAYBEL18:def 3;

      hence thesis by A1, Lm7;

    end;

    theorem :: TOPS_5:66

    for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I, P be Subset of ( product J) holds P is open iff ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V))

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      let P be Subset of ( product J);

      hereby

        assume P is open;

        then P in the topology of ( product J) by PRE_TOPC:def 2;

        then P in ( product_prebasis J) by Th65;

        hence ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V)) by Th64;

      end;

      

       A1: P is Subset of ( product ( Carrier J)) by WAYBEL18:def 3;

      assume ex V be Subset of (J . i) st V is open & P = ( product ( {i} --> V));

      then P in ( product_prebasis J) by A1, Th64;

      then P in the topology of ( product J) by Th65;

      hence P is open by PRE_TOPC:def 2;

    end;

    registration

      let I be non empty set;

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

      let i be Element of I;

      cluster ( proj (J,i)) -> continuous onto;

      coherence

      proof

        ( rng ( proj (J,i))) = the carrier of (J . i) by Th52;

        hence thesis by WAYBEL18: 5, FUNCT_2:def 3;

      end;

    end

    registration

      let I be non empty set;

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

      let i be Element of I;

      cluster ( proj (J,i)) -> open;

      coherence

      proof

        

         A1: ex B be Basis of ( product J) st for P be Subset of ( product J) st P in B holds (( proj (J,i)) .: P) is open

        proof

          set B = ( FinMeetCl ( product_prebasis J));

          set T = ( product J);

          reconsider K = ( product_prebasis J) as Subset-Family of T by WAYBEL18:def 3;

          ( FinMeetCl K) is Basis of T by WAYBEL18:def 3, YELLOW_9: 23;

          then

          reconsider B as Basis of ( product J) by WAYBEL18:def 3;

          take B;

          let P be Subset of ( product J);

          assume

           A2: P in B;

          per cases ;

            suppose P <> {} ;

            then ex I0 be finite Subset of I st for j be Element of I holds (( proj (J,j)) .: P) is open & ( not j in I0 implies (( proj (J,j)) .: P) = ( [#] (J . j))) by A2, Th63;

            hence thesis;

          end;

            suppose P = {} ;

            then (( proj (J,i)) .: P) is empty & (( proj (J,i)) .: P) is Subset of (J . i);

            hence thesis;

          end;

        end;

        ( product J) is TopSpace & (J . i) is TopSpace;

        hence thesis by A1, Th45;

      end;

    end

    theorem :: TOPS_5:67

    

     Th67: for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I holds ( proj (J,i)) is being_homeomorphism

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      ( card I) = 1 by CARD_1:def 7;

      then

       A1: I = {i} by ORDERS_5: 2;

      set f = ( proj (J,i));

      

       A2: ( dom f) = the carrier of ( product J) by FUNCT_2:def 1

      .= ( [#] ( product J)) by STRUCT_0:def 3;

      the carrier of (J . i) = ( [#] (J . i)) by STRUCT_0:def 3

      .= (( Carrier J) . i) by PENCIL_3: 7;

      then

       A3: ( Carrier J) = ( {i} --> the carrier of (J . i)) by A1, Th7;

      

       A4: ( rng f) = the carrier of (J . i) by FUNCT_2:def 3

      .= ( [#] (J . i)) by STRUCT_0:def 3;

      

       a5: f = ( proj (( Carrier J),i)) by WAYBEL18:def 4

      .= ( proj ((i .--> the carrier of (J . i)),i)) by A3, FUNCOP_1:def 9;

      (f " ) is continuous by a5, TOPREALA: 14;

      hence f is being_homeomorphism by A2, A4, a5, TOPS_2:def 5;

    end;

    theorem :: TOPS_5:68

    for I be 1 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i be Element of I holds (( product J),(J . i)) are_homeomorphic

    proof

      let I be 1 -element set;

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

      let i be Element of I;

      ( proj (J,i)) is being_homeomorphism by Th67;

      hence thesis by T_0TOPSP:def 1;

    end;

    

     Lm8: for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, P be Subset of ( product ( Carrier J)) st i <> j holds P in ( product_prebasis J) implies (ex V be Subset of (J . i) st V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))))) or (ex W be Subset of (J . j) st W is open & P = ( product ((i,j) --> (( [#] (J . i)),W))))

    proof

      let I be 2 -element set;

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

      let i,j be Element of I, P be Subset of ( product ( Carrier J));

      assume

       A1: i <> j & P in ( product_prebasis J);

      then

      consider k be set, T be TopStruct, U be Subset of T such that

       A2: k in I & U is open & T = (J . k) & P = ( product (( Carrier J) +* (k,U))) by WAYBEL18:def 2;

      k in {i, j} by A1, A2, Th8;

      per cases by TARSKI:def 2;

        suppose

         A3: k = i;

        then

        reconsider V = U as Subset of (J . i) by A2;

        now

          take V;

          thus V is open by A2, A3;

          (( Carrier J) . j) = ( [#] (J . j)) by PENCIL_3: 7;

          hence P = ( product ((i,j) --> (V,( [#] (J . j))))) by A2, A1, A3, Th34;

        end;

        hence thesis;

      end;

        suppose

         A4: k = j;

        then

        reconsider W = U as Subset of (J . j) by A2;

        now

          take W;

          thus W is open by A2, A4;

          (( Carrier J) . i) = ( [#] (J . i)) by PENCIL_3: 7;

          hence P = ( product ((i,j) --> (( [#] (J . i)),W))) by A2, A1, A4, Th34;

        end;

        hence thesis;

      end;

    end;

    theorem :: TOPS_5:69

    

     Th69: for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, P be Subset of ( product ( Carrier J)) st i <> j holds P in ( product_prebasis J) iff (ex V be Subset of (J . i) st V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))))) or (ex W be Subset of (J . j) st W is open & P = ( product ((i,j) --> (( [#] (J . i)),W))))

    proof

      let I be 2 -element set;

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

      let i,j be Element of I, P be Subset of ( product ( Carrier J));

      assume

       A1: i <> j;

      hence P in ( product_prebasis J) implies (ex V be Subset of (J . i) st V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))))) or (ex W be Subset of (J . j) st W is open & P = ( product ((i,j) --> (( [#] (J . i)),W)))) by Lm8;

      assume (ex V be Subset of (J . i) st V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))))) or (ex W be Subset of (J . j) st W is open & P = ( product ((i,j) --> (( [#] (J . i)),W))));

      per cases ;

        suppose ex V be Subset of (J . i) st V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))));

        then

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

         A2: V is open & P = ( product ((i,j) --> (V,( [#] (J . j)))));

        (( Carrier J) . j) = ( [#] (J . j)) by PENCIL_3: 7;

        then P = ( product (( Carrier J) +* (i,V))) by A1, A2, Th34;

        hence P in ( product_prebasis J) by A2, WAYBEL18:def 2;

      end;

        suppose ex W be Subset of (J . j) st W is open & P = ( product ((i,j) --> (( [#] (J . i)),W)));

        then

        consider W be Subset of (J . j) such that

         A3: W is open & P = ( product ((i,j) --> (( [#] (J . i)),W)));

        (( Carrier J) . i) = ( [#] (J . i)) by PENCIL_3: 7;

        then P = ( product (( Carrier J) +* (j,W))) by A1, A3, Th34;

        hence P in ( product_prebasis J) by A3, WAYBEL18:def 2;

      end;

    end;

    

     Lm9: for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, P be Subset of ( product ( Carrier J)) st i <> j holds P in ( FinMeetCl ( product_prebasis J)) implies ex V be Subset of (J . i), W be Subset of (J . j) st V is open & W is open & P = ( product ((i,j) --> (V,W)))

    proof

      let I be 2 -element set;

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

      let i,j be Element of I, P be Subset of ( product ( Carrier J));

      assume

       A1: i <> j & P in ( FinMeetCl ( product_prebasis J));

      then

      consider X be Subset-Family of ( product ( Carrier J)), f be one-to-oneI -valued Function such that

       A2: X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom f) = X and

       A3: P = ( product (( Carrier J) +* ( product_basis_selector (J,f)))) by Lm3;

      set F = (( Carrier J) +* ( product_basis_selector (J,f)));

      i in I & j in I;

      then

       A4: i in ( dom ( Carrier J)) & j in ( dom ( Carrier J)) by PARTFUN1:def 2;

      ( rng f) c= I;

      then ( rng f) c= {i, j} by A1, Th8;

      per cases by ZFMISC_1: 36;

        suppose ( rng f) = {} ;

        then ( product_basis_selector (J,f)) = {} ;

        

        then

         A5: P = ( product ((i,j) --> ((( Carrier J) . i),(( Carrier J) . j)))) by A1, A3, Th9

        .= ( product ((i,j) --> (( [#] (J . i)),(( Carrier J) . j)))) by PENCIL_3: 7

        .= ( product ((i,j) --> (( [#] (J . i)),( [#] (J . j))))) by PENCIL_3: 7;

        thus thesis by A5;

      end;

        suppose

         A6: ( rng f) = {i};

        then

         A7: ( dom f) = {((f " ) . i)} by Th1;

        

         A8: i in ( rng f) by A6, TARSKI:def 1;

        

         A9: ((f " ) . i) in X by A2, A7, TARSKI:def 1;

        then

        reconsider V0 = ((f " ) . i) as Subset of ( product ( Carrier J));

        reconsider V = (( proj (J,i)) .: V0) as Subset of (J . i);

        take V, ( [#] (J . j));

        V0 is empty or V0 is non empty;

        hence V is open & ( [#] (J . j)) is open by A2, A9, Th58;

        ( product_basis_selector (J,f)) = ( {i} --> (( product_basis_selector (J,f)) . i)) by A6, Th7

        .= ( {i} --> (( proj (J,i)) .: ((f " ) . i))) by A8, Th54

        .= (i .--> V) by FUNCOP_1:def 9;

        

        then F = (( Carrier J) +* (i,V)) by A4, FUNCT_7:def 3

        .= ((i,j) --> (V,(( Carrier J) . j))) by A1, Th34

        .= ((i,j) --> (V,( [#] (J . j)))) by PENCIL_3: 7;

        hence thesis by A3;

      end;

        suppose

         A10: ( rng f) = {j};

        then

         A11: ( dom f) = {((f " ) . j)} by Th1;

        

         A12: j in ( rng f) by A10, TARSKI:def 1;

        

         A13: ((f " ) . j) in X by A2, A11, TARSKI:def 1;

        then

        reconsider W0 = ((f " ) . j) as Subset of ( product ( Carrier J));

        reconsider W = (( proj (J,j)) .: W0) as Subset of (J . j);

        take ( [#] (J . i)), W;

        thus ( [#] (J . i)) is open;

        W0 is empty or W0 is non empty;

        hence W is open by A2, A13, Th58;

        ( product_basis_selector (J,f)) = ( {j} --> (( product_basis_selector (J,f)) . j)) by A10, Th7

        .= ( {j} --> (( proj (J,j)) .: ((f " ) . j))) by A12, Th54

        .= (j .--> W) by FUNCOP_1:def 9;

        

        then F = (( Carrier J) +* (j,W)) by A4, FUNCT_7:def 3

        .= ((i,j) --> ((( Carrier J) . i),W)) by A1, Th34

        .= ((i,j) --> (( [#] (J . i)),W)) by PENCIL_3: 7;

        hence thesis by A3;

      end;

        suppose

         A14: ( rng f) = {i, j};

        then

         A15: ( dom f) = {((f " ) . i), ((f " ) . j)} by Th2;

        

         A16: i in ( rng f) & j in ( rng f) by A14, TARSKI:def 2;

        

         A17: ((f " ) . i) in X & ((f " ) . j) in X by A2, A15, TARSKI:def 2;

        then

        reconsider V0 = ((f " ) . i) as Subset of ( product ( Carrier J));

        reconsider V = (( proj (J,i)) .: V0) as Subset of (J . i);

        reconsider W0 = ((f " ) . j) as Subset of ( product ( Carrier J)) by A17;

        reconsider W = (( proj (J,j)) .: W0) as Subset of (J . j);

        take V, W;

        V0 is empty or V0 is non empty;

        hence V is open by A2, A17, Th58;

        W0 is empty or W0 is non empty;

        hence W is open by A2, A17, Th58;

        ( rng f) = I by A1, A14, Th8;

        

        then

         A18: ( product_basis_selector (J,f)) = ((i,j) --> ((( product_basis_selector (J,f)) . i),(( product_basis_selector (J,f)) . j))) by A1, Th9

        .= ((i,j) --> ((( product_basis_selector (J,f)) . i),(( proj (J,j)) .: ((f " ) . j)))) by A16, Th54

        .= ((i,j) --> (V,W)) by A16, Th54;

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

        .= {i, j} by A1, Th8;

        then ( dom ( Carrier J)) = ( dom ( product_basis_selector (J,f))) by A14, PARTFUN1:def 2;

        hence thesis by A3, A18, FUNCT_4: 19;

      end;

    end;

    theorem :: TOPS_5:70

    for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, P be Subset of ( product ( Carrier J)) st i <> j holds P in ( FinMeetCl ( product_prebasis J)) iff ex V be Subset of (J . i), W be Subset of (J . j) st V is open & W is open & P = ( product ((i,j) --> (V,W)))

    proof

      let I be 2 -element set;

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

      let i,j be Element of I, P be Subset of ( product ( Carrier J));

      assume

       A1: i <> j;

      hence P in ( FinMeetCl ( product_prebasis J)) implies ex V be Subset of (J . i), W be Subset of (J . j) st V is open & W is open & P = ( product ((i,j) --> (V,W))) by Lm9;

      given V be Subset of (J . i), W be Subset of (J . j) such that

       A2: V is open & W is open & P = ( product ((i,j) --> (V,W)));

      ex Y be Subset-Family of ( product ( Carrier J)) st Y c= ( product_prebasis J) & Y is finite & P = ( Intersect Y)

      proof

        set V0 = ( product (( Carrier J) +* (i,V)));

        set W0 = ( product (( Carrier J) +* (j,W)));

        set Y = {V0, W0};

        

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

        (( Carrier J) . i) = ( [#] (J . i)) & (( Carrier J) . j) = ( [#] (J . j)) by PENCIL_3: 7;

        then

         a4: (( Carrier J) . i) = the carrier of (J . i) & (( Carrier J) . j) = the carrier of (J . j) by STRUCT_0:def 3;

        

         A5: V0 c= ( product ( Carrier J)) & W0 c= ( product ( Carrier J)) by a4, A3, Th39;

        then

        reconsider Y as Subset-Family of ( product ( Carrier J)) by ZFMISC_1: 32;

        take Y;

        

         A6: V0 = ( product ((i,j) --> (V,(( Carrier J) . j)))) & W0 = ( product ((i,j) --> ((( Carrier J) . i),W))) by A1, Th34;

        then V0 = ( product ((i,j) --> (V,( [#] (J . j))))) & W0 = ( product ((i,j) --> (( [#] (J . i)),W))) by PENCIL_3: 7;

        then V0 in ( product_prebasis J) & W0 in ( product_prebasis J) by A1, A2, A5, Th69;

        hence Y c= ( product_prebasis J) & Y is finite by ZFMISC_1: 32;

        P c= V0 & P c= W0 by A2, a4, A6, Th28;

        then

         A7: P c= (V0 /\ W0) by XBOOLE_1: 19;

        (V0 /\ W0) c= P

        proof

          let x be object;

          assume x in (V0 /\ W0);

          then

           A8: x in V0 & x in W0 by XBOOLE_0:def 4;

          then

          consider g be Function such that

           A9: g = x & ( dom g) = ( dom ((i,j) --> (V,(( Carrier J) . j)))) and

           A10: for y be object st y in ( dom ((i,j) --> (V,(( Carrier J) . j)))) holds (g . y) in (((i,j) --> (V,(( Carrier J) . j))) . y) by A6, CARD_3:def 5;

          

           A12: ( dom g) = {i, j} by A9, FUNCT_4: 62

          .= ( dom ((i,j) --> (V,W))) by FUNCT_4: 62;

          for y be object st y in ( dom ((i,j) --> (V,W))) holds (g . y) in (((i,j) --> (V,W)) . y)

          proof

            let y be object;

            assume y in ( dom ((i,j) --> (V,W)));

            then

             A13: y in {i, j} by FUNCT_4: 62;

            per cases by TARSKI:def 2;

              suppose

               A14: y = i;

              

              then

               A15: (((i,j) --> (V,(( Carrier J) . j))) . y) = V by A1, FUNCT_4: 63

              .= (((i,j) --> (V,W)) . y) by A1, A14, FUNCT_4: 63;

              y in ( dom ((i,j) --> (V,(( Carrier J) . j)))) by A13, FUNCT_4: 62;

              hence thesis by A10, A15;

            end;

              suppose

               A16: y = j;

              

              then

               A17: (((i,j) --> ((( Carrier J) . i),W)) . y) = W by FUNCT_4: 63

              .= (((i,j) --> (V,W)) . y) by A16, FUNCT_4: 63;

              y in ( dom ((i,j) --> ((( Carrier J) . i),W))) by A13, FUNCT_4: 62;

              hence thesis by A6, A8, A9, CARD_3: 9, A17;

            end;

          end;

          hence x in P by A2, A9, A12, CARD_3: 9;

        end;

        then P = (V0 /\ W0) by A7, XBOOLE_0:def 10;

        then P = ( meet Y) by SETFAM_1: 11;

        hence P = ( Intersect Y) by SETFAM_1:def 9;

      end;

      hence P in ( FinMeetCl ( product_prebasis J)) by CANTOR_1:def 3;

    end;

    theorem :: TOPS_5:71

    for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I holds <:( proj (J,i)), ( proj (J,j)):> is Function of ( product J), [:(J . i), (J . j):] by BORSUK_1:def 2;

    theorem :: TOPS_5:72

    

     Th72: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for P be Subset of ( product ( Carrier J)) holds for i,j be Element of I st i <> j & (ex F be ManySortedSet of I st P = ( product F) & for k be Element of I holds (F . k) c= (( Carrier J) . k)) holds ( <:( proj (J,i)), ( proj (J,j)):> .: P) = [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):]

    proof

      let I be non empty set;

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

      let P be Subset of ( product ( Carrier J));

      let i,j be Element of I;

      assume that

       A1: i <> j and

       A2: ex F be ManySortedSet of I st P = ( product F) & for k be Element of I holds (F . k) c= (( Carrier J) . k);

      consider F be ManySortedSet of I such that

       A3: P = ( product F) and

       A4: for k be Element of I holds (F . k) c= (( Carrier J) . k) by A2;

      per cases ;

        suppose

         A5: F is non-empty;

        for y be object holds y in [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):] implies y in ( <:( proj (J,i)), ( proj (J,j)):> .: P)

        proof

          let y be object;

          assume y in [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):];

          then

          consider y1,y2 be object such that

           A6: y1 in (( proj (J,i)) .: P) & y2 in (( proj (J,j)) .: P) & y = [y1, y2] by ZFMISC_1:def 2;

          

           A7: ( dom F) = I by PARTFUN1:def 2

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

          i in I & j in I;

          then

           A8: i in ( dom F) & j in ( dom F) by PARTFUN1:def 2;

          for k be object st k in ( dom F) holds (F . k) c= (( Carrier J) . k) by A4;

          then (( proj (( Carrier J),i)) .: P) = (F . i) & (( proj (( Carrier J),j)) .: P) = (F . j) by A3, A5, A7, A8, Th26;

          then

           A9: (( proj (J,i)) .: P) = (F . i) & (( proj (J,j)) .: P) = (F . j) by WAYBEL18:def 4;

          set p0 = the Element of ( product F);

          set p = (p0 +* ((i,j) --> (y1,y2)));

          

           A10: ( dom <:( proj (J,i)), ( proj (J,j)):>) = (( dom ( proj (J,i))) /\ ( dom ( proj (J,j)))) by FUNCT_3:def 7

          .= (( dom ( proj (( Carrier J),i))) /\ ( dom ( proj (J,j)))) by WAYBEL18:def 4

          .= (( dom ( proj (( Carrier J),i))) /\ ( dom ( proj (( Carrier J),j)))) by WAYBEL18:def 4;

          

          then

           A11: ( dom <:( proj (J,i)), ( proj (J,j)):>) = (( dom ( proj (( Carrier J),i))) /\ ( product ( Carrier J))) by CARD_3:def 16

          .= (( product ( Carrier J)) /\ ( product ( Carrier J))) by CARD_3:def 16

          .= ( product ( Carrier J));

          p in ( product (F +* ((i,j) --> ((F . i),(F . j))))) by A1, A6, A5, A9, Th30;

          then

           A12: p in P by A3, A8, Th11;

          then

           A14: p in ( dom ( proj (( Carrier J),i))) & p in ( dom ( proj (( Carrier J),j))) by A11, A10, XBOOLE_0:def 4;

          

           A15: (( proj (J,i)) . p) = (( proj (( Carrier J),i)) . p) by WAYBEL18:def 4

          .= (p . i) by A14, CARD_3:def 16

          .= y1 by A1, FUNCT_4: 84;

          

           A16: (( proj (J,j)) . p) = (( proj (( Carrier J),j)) . p) by WAYBEL18:def 4

          .= (p . j) by A14, CARD_3:def 16

          .= y2 by A1, FUNCT_4: 84;

          ( <:( proj (J,i)), ( proj (J,j)):> . p) = [y1, y2] by A11, A12, A15, A16, FUNCT_3:def 7;

          hence thesis by A6, A12, A11, FUNCT_1:def 6;

        end;

        then

         A17: [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):] c= ( <:( proj (J,i)), ( proj (J,j)):> .: P) by TARSKI:def 3;

        ( <:( proj (J,i)), ( proj (J,j)):> .: P) c= [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):] by FUNCT_3: 56;

        hence thesis by A17, XBOOLE_0:def 10;

      end;

        suppose not F is non-empty;

        then {} in ( rng F) by RELAT_1:def 9;

        then P = {} by A3, CARD_3: 26;

        then ( <:( proj (J,i)), ( proj (J,j)):> .: P) = {} & (( proj (J,i)) .: P) = {} ;

        hence thesis by ZFMISC_1: 90;

      end;

    end;

    theorem :: TOPS_5:73

    

     Th73: for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, f be Function of ( product J), [:(J . i), (J . j):] st i <> j & f = <:( proj (J,i)), ( proj (J,j)):> holds f is onto open

    proof

      let I be non empty set;

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

      let i,j be Element of I, f be Function of ( product J), [:(J . i), (J . j):];

      assume

       A1: i <> j & f = <:( proj (J,i)), ( proj (J,j)):>;

      

       a2: for k be Element of I holds (( Carrier J) . k) c= (( Carrier J) . k);

      

       A3: for k be Element of I holds (( proj (J,k)) .: ( [#] ( product ( Carrier J)))) = the carrier of (J . k)

      proof

        let k be Element of I;

        

        thus (( proj (J,k)) .: ( [#] ( product ( Carrier J)))) = (( proj (J,k)) .: ( product ( Carrier J))) by SUBSET_1:def 3

        .= (( proj (J,k)) .: ( dom ( proj (( Carrier J),k)))) by CARD_3:def 16

        .= (( proj (J,k)) .: ( dom ( proj (J,k)))) by WAYBEL18:def 4

        .= ( rng ( proj (J,k))) by RELAT_1: 113

        .= the carrier of (J . k) by Th52;

      end;

      ( rng f) = ( <:( proj (J,i)), ( proj (J,j)):> .: ( dom f)) by A1, RELAT_1: 113

      .= ( <:( proj (J,i)), ( proj (J,j)):> .: the carrier of ( product J)) by FUNCT_2:def 1

      .= ( <:( proj (J,i)), ( proj (J,j)):> .: ( product ( Carrier J))) by WAYBEL18:def 3

      .= ( <:( proj (J,i)), ( proj (J,j)):> .: ( [#] ( product ( Carrier J)))) by SUBSET_1:def 3

      .= [:(( proj (J,i)) .: ( [#] ( product ( Carrier J)))), (( proj (J,j)) .: ( [#] ( product ( Carrier J)))):] by A1, SUBSET_1:def 3, a2, Th72

      .= [:the carrier of (J . i), (( proj (J,j)) .: ( [#] ( product ( Carrier J)))):] by A3

      .= [:the carrier of (J . i), the carrier of (J . j):] by A3

      .= the carrier of [:(J . i), (J . j):] by BORSUK_1:def 2;

      hence f is onto by FUNCT_2:def 3;

      ex B be Basis of ( product J) st for P be Subset of ( product J) st P in B holds (f .: P) is open

      proof

        set B = ( FinMeetCl ( product_prebasis J));

        set T = ( product J);

        reconsider K = ( product_prebasis J) as Subset-Family of T by WAYBEL18:def 3;

        ( FinMeetCl K) is Basis of T by WAYBEL18:def 3, YELLOW_9: 23;

        then

        reconsider B as Basis of ( product J) by WAYBEL18:def 3;

        take B;

        let P be Subset of ( product J);

        assume

         A4: P in B;

        

         A5: (( proj (J,i)) .: P) is open & (( proj (J,j)) .: P) is open

        proof

          per cases ;

            suppose P <> {} ;

            then ex I0 be finite Subset of I st for j be Element of I holds (( proj (J,j)) .: P) is open & ( not j in I0 implies (( proj (J,j)) .: P) = ( [#] (J . j))) by A4, Th63;

            hence thesis;

          end;

            suppose P = {} ;

            then (( proj (J,i)) .: P) is empty & (( proj (J,i)) .: P) is Subset of (J . i) & (( proj (J,j)) .: P) is empty & (( proj (J,j)) .: P) is Subset of (J . j);

            hence thesis;

          end;

        end;

        

         A7: ex F be ManySortedSet of I st P = ( product F) & for k be Element of I holds (F . k) c= (( Carrier J) . k)

        proof

          consider X be Subset-Family of ( product ( Carrier J)), g be one-to-oneI -valued Function such that X c= ( product_prebasis J) & X is finite & P = ( Intersect X) & ( dom g) = X and

           A8: P = ( product (( Carrier J) +* ( product_basis_selector (J,g)))) by A4, Lm3;

          set F = (( Carrier J) +* ( product_basis_selector (J,g)));

          reconsider F as ManySortedSet of I;

          take F;

          thus P = ( product F) by A8;

          let k be Element of I;

          per cases ;

            suppose

             A9: k in ( rng g);

            then k in ( dom ( product_basis_selector (J,g))) by PARTFUN1:def 2;

            

            then

             a10: (F . k) = (( product_basis_selector (J,g)) . k) by FUNCT_4: 13

            .= (( proj (J,k)) .: ((g " ) . k)) by A9, Th54;

            ( rng ( proj (J,k))) = the carrier of (J . k) by Th52

            .= ( [#] (J . k)) by STRUCT_0:def 3

            .= (( Carrier J) . k) by PENCIL_3: 7;

            hence thesis by a10, RELAT_1: 111;

          end;

            suppose not k in ( rng g);

            then not k in ( dom ( product_basis_selector (J,g)));

            hence thesis by FUNCT_4: 11;

          end;

        end;

        P is Subset of ( product ( Carrier J)) by WAYBEL18:def 3;

        then (f .: P) = [:(( proj (J,i)) .: P), (( proj (J,j)) .: P):] by A1, A7, Th72;

        hence (f .: P) is open by A5, BORSUK_1: 6;

      end;

      hence f is open by Th45;

    end;

    theorem :: TOPS_5:74

    

     Th74: for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I, f be Function of ( product J), [:(J . i), (J . j):] st i <> j & f = <:( proj (J,i)), ( proj (J,j)):> holds f is being_homeomorphism

    proof

      let I be 2 -element set;

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

      let i,j be Element of I, f be Function of ( product J), [:(J . i), (J . j):];

      assume

       A1: i <> j & f = <:( proj (J,i)), ( proj (J,j)):>;

      

       A2: ( dom f) = the carrier of ( product J) by FUNCT_2:def 1

      .= ( [#] ( product J)) by STRUCT_0:def 3;

      

       A3: f is onto open by A1, Th73;

      then ( rng f) = the carrier of [:(J . i), (J . j):] by FUNCT_2:def 3;

      then

       A4: ( rng f) = ( [#] [:(J . i), (J . j):]) by STRUCT_0:def 3;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A5: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        then

         a6: (f . x1) = [(( proj (J,i)) . x1), (( proj (J,j)) . x1)] & (f . x2) = [(( proj (J,i)) . x2), (( proj (J,j)) . x2)] by A1, FUNCT_3:def 7;

        x1 in (( dom ( proj (J,i))) /\ ( dom ( proj (J,j)))) & x2 in (( dom ( proj (J,i))) /\ ( dom ( proj (J,j)))) by A1, A5, FUNCT_3:def 7;

        then x1 in ( dom ( proj (J,i))) & x2 in ( dom ( proj (J,j))) by XBOOLE_0:def 4;

        then

         a7: x1 in ( dom ( proj (( Carrier J),i))) & x2 in ( dom ( proj (( Carrier J),j))) by WAYBEL18:def 4;

        reconsider g1 = x1, g2 = x2 as Element of ( product J) by A5;

        (( proj (J,i)) . x1) = (g1 . i) & (( proj (J,i)) . x2) = (g2 . i) & (( proj (J,j)) . x1) = (g1 . j) & (( proj (J,j)) . x2) = (g2 . j) by YELLOW17: 8;

        then

         A8: (g1 . i) = (g2 . i) & (g1 . j) = (g2 . j) by a6, A5, XTUPLE_0: 1;

        

         A9: ( Carrier J) = ((i,j) --> ((( Carrier J) . i),(( Carrier J) . j))) by A1, Th9;

        then

        consider a1,b1 be object such that a1 in (( Carrier J) . i) & b1 in (( Carrier J) . j) and

         A10: g1 = ((i,j) --> (a1,b1)) by A1, a7, Th29;

        consider a2,b2 be object such that a2 in (( Carrier J) . i) & b2 in (( Carrier J) . j) and

         A11: g2 = ((i,j) --> (a2,b2)) by A1, a7, A9, Th29;

        (g1 . i) = a1 & (g2 . i) = a2 & (g1 . j) = b1 & (g2 . j) = b2 by A1, A10, A11, FUNCT_4: 63;

        hence thesis by A8, A10, A11;

      end;

      then

       A12: f is one-to-one by FUNCT_1:def 4;

      

       A13: f is continuous by A1, YELLOW12: 41;

      (f " ) is continuous by A3, A12, TOPREALA: 14;

      hence f is being_homeomorphism by A2, A4, A12, A13, TOPS_2:def 5;

    end;

    theorem :: TOPS_5:75

    for I be 2 -element set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for i,j be Element of I st i <> j holds (( product J), [:(J . i), (J . j):]) are_homeomorphic

    proof

      let I be 2 -element set;

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

      let i,j be Element of I;

      assume

       A1: i <> j;

      reconsider f = <:( proj (J,i)), ( proj (J,j)):> as Function of ( product J), [:(J . i), (J . j):] by BORSUK_1:def 2;

      f is being_homeomorphism by A1, Th74;

      hence thesis by T_0TOPSP:def 1;

    end;

    registration

      let I1,I2 be non empty set;

      let J be TopSpace-yielding non-Empty ManySortedSet of I2;

      let f be Function of I1, I2;

      cluster (J * f) -> TopSpace-yielding non-Empty;

      coherence

      proof

        hereby

          let y be object;

          assume y in ( rng (J * f));

          then y in ( rng J) by RELAT_1: 26, TARSKI:def 3;

          hence y is TopSpace by Def1;

        end;

        for S be 1-sorted st S in ( rng (J * f)) holds S is non empty

        proof

          let S be 1-sorted;

          assume S in ( rng (J * f));

          then S in ( rng J) by RELAT_1: 26, TARSKI:def 3;

          hence thesis by WAYBEL_3:def 7;

        end;

        hence thesis by WAYBEL_3:def 7;

      end;

    end

    definition

      let I1,I2 be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;

      let p be Function of I1, I2;

      assume that

       A1: p is bijective and

       A2: for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic ;

      :: TOPS_5:def5

      mode ProductHomeo of J1,J2,p -> Function of ( product J1), ( product J2) means

      : Def5: ex F be ManySortedFunction of I1 st (for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism) & for g be Element of ( product J1), i be Element of I1 holds ((it . g) . (p . i)) = ((F . i) . (g . i));

      existence

      proof

        defpred P[ object, object] means ex i be Element of I1, f be Function of (J1 . i), ((J2 * p) . i) st $1 = i & $2 = f & f is being_homeomorphism;

        

         A3: for x be object st x in I1 holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in I1;

          then

          reconsider i = x as Element of I1;

          consider f be Function of (J1 . i), ((J2 * p) . i) such that

           A4: f is being_homeomorphism by A2, T_0TOPSP:def 1;

          take f, i, f;

          thus thesis by A4;

        end;

        consider F be ManySortedSet of I1 such that

         A5: for x be object st x in I1 holds P[x, (F . x)] from PBOOLE:sch 3( A3);

        

         A6: for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism

        proof

          let i be Element of I1;

          consider j be Element of I1, f be Function of (J1 . j), ((J2 * p) . j) such that

           A7: i = j & (F . i) = f & f is being_homeomorphism by A5;

          reconsider f as Function of (J1 . i), ((J2 * p) . i) by A7;

          take f;

          thus thesis by A7;

        end;

        for x be object st x in ( dom F) holds (F . x) is Function

        proof

          let x be object;

          assume x in ( dom F);

          then

          reconsider i = x as Element of I1;

          ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism by A6;

          hence thesis;

        end;

        then

        reconsider F as ManySortedFunction of I1 by FUNCOP_1:def 6;

        defpred Q[ object, object] means ex g be Element of ( product J1), h be Element of ( product J2) st $1 = g & $2 = h & for i be Element of I1 holds (h . (p . i)) = ((F . i) . (g . i));

        

         A9: for x be object st x in the carrier of ( product J1) holds ex y be object st y in the carrier of ( product J2) & Q[x, y]

        proof

          let x be object;

          assume x in the carrier of ( product J1);

          then

          reconsider g = x as Element of ( product J1);

          deffunc H( object) = ((F . $1) . (g . $1));

          consider h0 be ManySortedSet of I1 such that

           A10: for i be Element of I1 holds (h0 . i) = H(i) from PBOOLE:sch 5;

          reconsider p9 = p as one-to-one Function by A1;

          ( rng (p9 " )) = ( dom p9) by FUNCT_1: 33

          .= I1 by FUNCT_2:def 1

          .= ( dom h0) by PARTFUN1:def 2;

          

          then ( dom (h0 * (p9 " ))) = ( dom (p9 " )) by RELAT_1: 27

          .= ( rng p9) by FUNCT_1: 33

          .= I2 by A1, FUNCT_2:def 3;

          then

          reconsider h = (h0 * (p9 " )) as ManySortedSet of I2 by PARTFUN1:def 2, RELAT_1:def 18;

          take h;

          

           A11: ( dom h) = I2 by PARTFUN1:def 2

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

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

          proof

            let x be object;

            assume x in ( dom ( Carrier J2));

            then

            reconsider j = x as Element of I2;

            j in I2;

            then

             A12: j in ( rng p9) by A1, FUNCT_2:def 3;

            then

             A13: j in ( dom (p9 " )) by FUNCT_1: 33;

            then ((p9 " ) . j) in ( rng (p9 " )) by FUNCT_1: 3;

            then ((p9 " ) . j) in ( dom p9) by FUNCT_1: 33;

            then

            reconsider i = ((p9 " ) . j) as Element of I1 by FUNCT_2:def 1;

            

             A14: ((F . i) . (g . i)) = (h0 . i) by A10

            .= (h . j) by A13, FUNCT_1: 13;

            consider f be Function of (J1 . i), ((J2 * p) . i) such that

             A15: (F . i) = f & f is being_homeomorphism by A6;

            

             A16: (f . (g . i)) in the carrier of ((J2 * p) . i);

            i in I1;

            then i in ( dom p) by FUNCT_2:def 1;

            

            then ((J2 * p) . i) = (J2 . (p . i)) by FUNCT_1: 13

            .= (J2 . j) by A12, FUNCT_1: 35;

            then (h . j) in ( [#] (J2 . j)) by A14, A15, A16, STRUCT_0:def 3;

            hence thesis by PENCIL_3: 7;

          end;

          then

           H: h in ( product ( Carrier J2)) by A11, CARD_3: 9;

          hence h in the carrier of ( product J2) by WAYBEL18:def 3;

          reconsider h as Element of ( product J2) by H, WAYBEL18:def 3;

          take g, h;

          now

            let i be Element of I1;

            i in I1;

            then

             A17: i in ( dom p) by PARTFUN1:def 2;

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

            then

             A18: (p9 . i) in ( dom (p9 " )) by FUNCT_1: 33;

            

            thus (h . (p . i)) = (h0 . ((p9 " ) . (p9 . i))) by A18, FUNCT_1: 13

            .= (h0 . i) by A17, FUNCT_1: 34

            .= ((F . i) . (g . i)) by A10;

          end;

          hence thesis;

        end;

        consider IT be Function of the carrier of ( product J1), the carrier of ( product J2) such that

         A19: for x be object st x in the carrier of ( product J1) holds Q[x, (IT . x)] from FUNCT_2:sch 1( A9);

        reconsider IT as Function of ( product J1), ( product J2);

        take IT, F;

        now

          let g be Element of ( product J1);

          

           A20: ex g0 be Element of ( product J1), h be Element of ( product J2) st g = g0 & (IT . g) = h & for i be Element of I1 holds (h . (p . i)) = ((F . i) . (g0 . i)) by A19;

          let i be Element of I1;

          thus ((IT . g) . (p . i)) = ((F . i) . (g . i)) by A20;

        end;

        hence thesis by A6;

      end;

    end

    theorem :: TOPS_5:76

    

     Th76: for I1,I2 be non empty set holds for J1 be TopSpace-yielding non-Empty ManySortedSet of I1 holds for J2 be TopSpace-yielding non-Empty ManySortedSet of I2 holds for p be Function of I1, I2, H be ProductHomeo of J1, J2, p holds for F be ManySortedFunction of I1 st p is bijective & (for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism) & (for g be Element of ( product J1), i be Element of I1 holds ((H . g) . (p . i)) = ((F . i) . (g . i))) holds for i be Element of I1, U be Subset of (J1 . i) holds (H .: ( product (( Carrier J1) +* (i,U)))) = ( product (( Carrier J2) +* ((p . i),((F . i) .: U))))

    proof

      let I1,I2 be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;

      let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;

      let F be ManySortedFunction of I1;

      assume that

       A1: p is bijective and

       A2: for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism and

       A3: for g be Element of ( product J1), i be Element of I1 holds ((H . g) . (p . i)) = ((F . i) . (g . i));

      let i be Element of I1, U be Subset of (J1 . i);

      reconsider j = (p . i) as Element of I2;

      i in I1;

      then

       A4: i in ( dom p) by FUNCT_2:def 1;

      consider f be Function of (J1 . i), ((J2 * p) . i) such that

       A5: (F . i) = f & f is being_homeomorphism by A2;

      

       A6: ( rng f) = ( [#] ((J2 * p) . i)) by A5, TOPS_2:def 5

      .= ( [#] (J2 . j)) by A4, FUNCT_1: 13

      .= the carrier of (J2 . j) by STRUCT_0:def 3;

      for y be object holds y in (H .: ( product (( Carrier J1) +* (i,U)))) iff y in ( product (( Carrier J2) +* (j,((F . i) .: U))))

      proof

        let y be object;

        thus y in (H .: ( product (( Carrier J1) +* (i,U)))) implies y in ( product (( Carrier J2) +* (j,((F . i) .: U))))

        proof

          assume y in (H .: ( product (( Carrier J1) +* (i,U))));

          then

          consider x be object such that

           A8: x in ( dom H) & x in ( product (( Carrier J1) +* (i,U))) & y = (H . x) by FUNCT_1:def 6;

          reconsider g = x as Element of ( product J1) by A8;

          y in ( rng H) by A8, FUNCT_1: 3;

          then

          reconsider h = y as Element of ( product J2);

          h in the carrier of ( product J2);

          then

           A9: h in ( product ( Carrier J2)) by WAYBEL18:def 3;

          

          then

           A10: ( dom h) = ( dom ( Carrier J2)) by CARD_3: 9

          .= ( dom (( Carrier J2) +* (j,((F . i) .: U)))) by FUNCT_7: 30;

          for z be object st z in ( dom (( Carrier J2) +* (j,((F . i) .: U)))) holds (h . z) in ((( Carrier J2) +* (j,((F . i) .: U))) . z)

          proof

            let z be object;

            assume

             a11: z in ( dom (( Carrier J2) +* (j,((F . i) .: U))));

            then

             A11: z in ( dom ( Carrier J2)) by FUNCT_7: 30;

            reconsider j0 = z as Element of I2 by a11;

            I2 = ( rng p) by A1, FUNCT_2:def 3;

            then

            consider i0 be object such that

             A12: i0 in I1 & (p . i0) = j0 by FUNCT_2: 11;

            reconsider i0 as Element of I1 by A12;

            consider f0 be Function of (J1 . i0), ((J2 * p) . i0) such that

             A13: (F . i0) = f0 & f0 is being_homeomorphism by A2;

            

             A14: (h . j0) = (f0 . (g . i0)) by A3, A8, A12, A13;

            per cases ;

              suppose

               A15: j0 = j;

              then

               A16: ((( Carrier J2) +* (j,((F . i) .: U))) . z) = ((F . i) .: U) by A11, FUNCT_7: 31;

              

               A17: i0 = i by A1, A12, A15, FUNCT_2: 19;

              

               a18: I1 = ( dom ( Carrier J1)) by PARTFUN1:def 2;

              then i in ( dom ( Carrier J1));

              then i in ( dom (( Carrier J1) +* (i,U))) by FUNCT_7: 30;

              then (g . i) in ((( Carrier J1) +* (i,U)) . i) by A8, CARD_3: 9;

              then (g . i) in U by a18, FUNCT_7: 31;

              hence thesis by A14, A16, A17, A13, FUNCT_2: 35;

            end;

              suppose j0 <> j;

              then ((( Carrier J2) +* (j,((F . i) .: U))) . z) = (( Carrier J2) . z) by FUNCT_7: 32;

              hence thesis by A9, A11, CARD_3: 9;

            end;

          end;

          hence y in ( product (( Carrier J2) +* (j,((F . i) .: U)))) by A10, CARD_3: 9;

        end;

        assume

         A20: y in ( product (( Carrier J2) +* (j,((F . i) .: U))));

        then

        reconsider h = y as Element of ( product (( Carrier J2) +* (j,((F . i) .: U))));

        

         A21: the carrier of (J1 . i) = ( [#] (J1 . i)) by STRUCT_0:def 3

        .= (( Carrier J1) . i) by PENCIL_3: 7;

        i in I1;

        then

         A22: i in ( dom ( Carrier J1)) by PARTFUN1:def 2;

        then

         A23: ( product (( Carrier J1) +* (i,U))) c= ( product ( Carrier J1)) by A21, Th39;

        

         A24: (( Carrier J2) . j) = ( [#] (J2 . j)) by PENCIL_3: 7

        .= the carrier of (J2 . j) by STRUCT_0:def 3;

        

         a25: j in I2 & ((F . i) .: U) c= the carrier of (J2 . j) by A6, A5, RELAT_1: 111;

        then

         A25: j in ( dom ( Carrier J2)) & ((F . i) .: U) c= (( Carrier J2) . j) by A24, PARTFUN1:def 2;

        then

         A26: ( product (( Carrier J2) +* (j,((F . i) .: U)))) c= ( product ( Carrier J2)) by Th39;

        ex x be object st x in ( dom H) & x in ( product (( Carrier J1) +* (i,U))) & (H . x) = y

        proof

          defpred P[ object, object] means ex f be one-to-one Function st (F . $1) = f & $2 = ((f " ) . (h . (p . $1)));

          

           A28: for i0 be Element of I1 holds ex y be object st P[i0, y]

          proof

            let i0 be Element of I1;

            consider f0 be Function of (J1 . i0), ((J2 * p) . i0) such that

             A29: (F . i0) = f0 & f0 is being_homeomorphism by A2;

            reconsider f0 as one-to-one Function by A29;

            take ((f0 " ) . (h . (p . i0))), f0;

            thus thesis by A29;

          end;

          consider g be ManySortedSet of I1 such that

           A30: for i be Element of I1 holds P[i, (g . i)] from PBOOLE:sch 6( A28);

          take g;

          

           A31: ( dom g) = I1 by PARTFUN1:def 2

          .= ( dom (( Carrier J1) +* (i,U))) by PARTFUN1:def 2;

          

           a36: for z be object st z in ( dom (( Carrier J1) +* (i,U))) holds (g . z) in ((( Carrier J1) +* (i,U)) . z)

          proof

            let z be object;

            assume z in ( dom (( Carrier J1) +* (i,U)));

            then

            reconsider i0 = z as Element of I1;

            consider f0 be one-to-one Function such that

             A32: (F . i0) = f0 & (g . i0) = ((f0 " ) . (h . (p . i0))) by A30;

            (p . i0) in I2;

            then (p . i0) in ( dom ( Carrier J2)) by PARTFUN1:def 2;

            then (h . (p . i0)) in (( Carrier J2) . (p . i0)) by A20, A26, CARD_3: 9;

            then (h . (p . i0)) in ( [#] (J2 . (p . i0))) by PENCIL_3: 7;

            then

             A33: (h . (p . i0)) in ( [#] ((J2 * p) . i0)) by FUNCT_2: 15;

            per cases ;

              suppose

               A35: i = i0;

              then

               A36: ((( Carrier J1) +* (i,U)) . z) = U by A22, FUNCT_7: 31;

              j in ( dom (( Carrier J2) +* (j,((F . i) .: U)))) by a25, PARTFUN1:def 2;

              then (h . j) in ((( Carrier J2) +* (j,((F . i) .: U))) . j) by A20, CARD_3: 9;

              then

               A37: (h . j) in ((F . i) .: U) by A25, FUNCT_7: 31;

              

               A38: (f " ) = (f0 " ) by A5, A32, A35, TOPS_2:def 4;

              ( [#] ((J2 * p) . i0)) = ( rng f) by A5, A35, TOPS_2:def 5

              .= ( dom (f0 " )) by A5, A32, A35, FUNCT_1: 33;

              then (g . i0) in ( rng (f0 " )) by A32, A33, FUNCT_1: 3;

              then

               A39: (g . i0) in ( dom f) by A5, A32, A35, FUNCT_1: 33;

              (h . j) in (( Carrier J2) . j) by A20, A26, A25, CARD_3: 9;

              then (h . j) in ( [#] (J2 . j)) by PENCIL_3: 7;

              then

               a40: (h . j) in ( [#] ((J2 * p) . i)) by A4, FUNCT_1: 13;

              

               a41: ( dom f) = the carrier of (J1 . i) by FUNCT_2:def 1;

              reconsider f1 = f as one-to-one Function by A5;

              

               A43: (h . j) in ( rng f1) by a40, A5, TOPS_2:def 5;

              (f . ((f " ) . (h . j))) = (f1 . ((f1 " ) . (h . j))) by A5, TOPS_2:def 4

              .= (h . j) by A43, FUNCT_1: 35;

              then (g . i0) in (f0 " (f0 .: U)) by A5, A32, A35, A38, A39, A37, FUNCT_1:def 7;

              hence thesis by A36, a41, A5, A32, A35, FUNCT_1: 94;

            end;

              suppose i <> i0;

              then

               A44: ((( Carrier J1) +* (i,U)) . z) = (( Carrier J1) . z) by FUNCT_7: 32;

              consider f9 be Function of (J1 . i0), ((J2 * p) . i0) such that

               A45: (F . i0) = f9 & f9 is being_homeomorphism by A2;

              ( dom (f0 " )) = ( rng f0) by FUNCT_1: 33

              .= ( [#] ((J2 * p) . i0)) by A32, A45, TOPS_2:def 5

              .= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3;

              then ((f0 " ) . (h . (p . i0))) in ( rng (f0 " )) by A33, FUNCT_1: 3;

              then (g . i0) in ( dom f0) by A32, FUNCT_1: 33;

              then (g . i0) in ( [#] (J1 . i0)) by A32, A45, TOPS_2:def 5;

              hence thesis by A44, PENCIL_3: 7;

            end;

          end;

          then g in ( product (( Carrier J1) +* (i,U))) by A31, CARD_3: 9;

          then g in ( product ( Carrier J1)) by A23;

          then

           A47: g in the carrier of ( product J1) by WAYBEL18:def 3;

          hence g in ( dom H) & g in ( product (( Carrier J1) +* (i,U))) by a36, A31, CARD_3: 9, FUNCT_2:def 1;

          reconsider h0 = (H . g) as Element of ( product J2) by A47, FUNCT_2: 5;

          h0 in the carrier of ( product J2);

          then h0 in ( product ( Carrier J2)) by WAYBEL18:def 3;

          

          then

           A48: ( dom h0) = ( dom ( Carrier J2)) by CARD_3: 9

          .= ( dom h) by A20, A26, CARD_3: 9;

          for z be object st z in ( dom h) holds (h . z) = (h0 . z)

          proof

            let z be object;

            assume z in ( dom h);

            then z in ( dom ( Carrier J2)) by A20, A26, CARD_3: 9;

            then

            reconsider j0 = z as Element of I2;

            reconsider p9 = p as one-to-one Function by A1;

            j0 in I2;

            then

             A49: j0 in ( rng p9) by A1, FUNCT_2:def 3;

            then j0 in ( dom (p9 " )) by FUNCT_1: 33;

            then ((p9 " ) . j0) in ( rng (p9 " )) by FUNCT_1: 3;

            then

             A50: ((p9 " ) . j0) in ( dom p9) by FUNCT_1: 33;

            then

            reconsider i0 = ((p9 " ) . j0) as Element of I1 by FUNCT_2:def 1;

            consider f9 be one-to-one Function such that

             A51: (F . i0) = f9 & (g . i0) = ((f9 " ) . (h . (p . i0))) by A30;

            consider f0 be Function of (J1 . i0), ((J2 * p) . i0) such that

             A52: (F . i0) = f0 & f0 is being_homeomorphism by A2;

            

             A53: ( rng f9) = ( [#] ((J2 * p) . i0)) by A51, A52, TOPS_2:def 5

            .= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3;

            

             A54: (p . i0) = j0 by A49, FUNCT_1: 35;

            

             A55: (( Carrier J2) . (p . i0)) = ( [#] (J2 . (p . i0))) by PENCIL_3: 7

            .= ( [#] ((J2 * p) . i0)) by A50, FUNCT_1: 13

            .= the carrier of ((J2 * p) . i0) by STRUCT_0:def 3;

            (p . i0) in I2;

            then (p . i0) in ( dom ( Carrier J2)) by PARTFUN1:def 2;

            then

             A56: (h . (p . i0)) in (( Carrier J2) . (p . i0)) by A20, A26, CARD_3: 9;

            (h . j0) = (f9 . ((f9 " ) . (h . (p . i0)))) by A53, A54, A55, A56, FUNCT_1: 35

            .= (h0 . j0) by A3, A47, A51, A54;

            hence thesis;

          end;

          hence (H . g) = y by A48, FUNCT_1: 2;

        end;

        hence thesis by FUNCT_1:def 6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPS_5:77

    

     Th77: for I1,I2 be non empty set holds for J1 be TopSpace-yielding non-Empty ManySortedSet of I1 holds for J2 be TopSpace-yielding non-Empty ManySortedSet of I2 holds for p be Function of I1, I2, H be ProductHomeo of J1, J2, p st p is bijective & for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic holds H is bijective

    proof

      let I1,I2 be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;

      let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;

      assume that

       A1: p is bijective and

       A2: for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic ;

      consider F be ManySortedFunction of I1 such that

       A3: for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism and

       A4: for g be Element of ( product J1), i be Element of I1 holds ((H . g) . (p . i)) = ((F . i) . (g . i)) by A1, A2, Def5;

      for x1,x2 be object st x1 in ( dom H) & x2 in ( dom H) & (H . x1) = (H . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A5: x1 in ( dom H) & x2 in ( dom H) & (H . x1) = (H . x2);

        then

        reconsider g1 = x1, g2 = x2 as Element of ( product J1);

        

         A6: g1 is Element of ( product ( Carrier J1)) & g2 is Element of ( product ( Carrier J1)) by WAYBEL18:def 3;

        

         A7: ( dom g1) = ( dom ( Carrier J1)) by A6, CARD_3: 9

        .= ( dom g2) by A6, CARD_3: 9;

        for z be object st z in ( dom g1) holds (g1 . z) = (g2 . z)

        proof

          let z be object;

          assume z in ( dom g1);

          then z in ( dom ( Carrier J1)) by A6, CARD_3: 9;

          then

          reconsider i = z as Element of I1;

          

           a8: ((H . g1) . (p . i)) = ((F . i) . (g1 . i)) & ((H . g2) . (p . i)) = ((F . i) . (g2 . i)) by A4;

          consider f be Function of (J1 . i), ((J2 * p) . i) such that

           A9: (F . i) = f & f is being_homeomorphism by A3;

          

           A12: (( Carrier J1) . i) = ( [#] (J1 . i)) by PENCIL_3: 7

          .= the carrier of (J1 . i) by STRUCT_0:def 3

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

          i in I1;

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

          then (g1 . i) in (( Carrier J1) . i) & (g2 . i) in (( Carrier J1) . i) by A6, CARD_3: 9;

          hence thesis by a8, A5, A9, A12, FUNCT_1:def 4;

        end;

        hence thesis by A7, FUNCT_1: 2;

      end;

      then

       A13: H is one-to-one by FUNCT_1:def 4;

      set i0 = the Element of I1;

      consider f0 be Function of (J1 . i0), ((J2 * p) . i0) such that

       A14: (F . i0) = f0 & f0 is being_homeomorphism by A3;

      i0 in I1;

      then

       A15: i0 in ( dom p) by FUNCT_2:def 1;

      ( rng H) = (H .: ( dom H)) by RELAT_1: 113

      .= (H .: the carrier of ( product J1)) by FUNCT_2:def 1

      .= (H .: ( product ( Carrier J1))) by WAYBEL18:def 3

      .= (H .: ( product (( Carrier J1) +* (i0,(( Carrier J1) . i0))))) by FUNCT_7: 35

      .= (H .: ( product (( Carrier J1) +* (i0,( [#] (J1 . i0)))))) by PENCIL_3: 7

      .= ( product (( Carrier J2) +* ((p . i0),((F . i0) .: ( [#] (J1 . i0)))))) by A1, A3, A4, Th76

      .= ( product (( Carrier J2) +* ((p . i0),(f0 .: ( dom f0))))) by A14, TOPS_2:def 5

      .= ( product (( Carrier J2) +* ((p . i0),( rng f0)))) by RELAT_1: 113

      .= ( product (( Carrier J2) +* ((p . i0),( [#] ((J2 * p) . i0))))) by A14, TOPS_2:def 5

      .= ( product (( Carrier J2) +* ((p . i0),( [#] (J2 . (p . i0)))))) by A15, FUNCT_1: 13

      .= ( product (( Carrier J2) +* ((p . i0),(( Carrier J2) . (p . i0))))) by PENCIL_3: 7

      .= ( product ( Carrier J2)) by FUNCT_7: 35

      .= the carrier of ( product J2) by WAYBEL18:def 3;

      then H is onto by FUNCT_2:def 3;

      hence thesis by A13;

    end;

    theorem :: TOPS_5:78

    

     Th78: for I1,I2 be non empty set holds for J1 be TopSpace-yielding non-Empty ManySortedSet of I1 holds for J2 be TopSpace-yielding non-Empty ManySortedSet of I2 holds for p be Function of I1, I2, H be ProductHomeo of J1, J2, p st p is bijective & for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic holds H is being_homeomorphism

    proof

      let I1,I2 be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;

      let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;

      assume that

       A1: p is bijective and

       A2: for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic ;

      consider F be ManySortedFunction of I1 such that

       A3: for i be Element of I1 holds ex f be Function of (J1 . i), ((J2 * p) . i) st (F . i) = f & f is being_homeomorphism and

       A4: for g be Element of ( product J1), i be Element of I1 holds ((H . g) . (p . i)) = ((F . i) . (g . i)) by A1, A2, Def5;

      

       A5: H is bijective by A1, A2, Th77;

      ex K be prebasis of ( product J1), L be prebasis of ( product J2) st (H .: K) = L

      proof

        reconsider K = ( product_prebasis J1) as prebasis of ( product J1) by WAYBEL18:def 3;

        reconsider L = ( product_prebasis J2) as prebasis of ( product J2) by WAYBEL18:def 3;

        take K, L;

        for W be Subset of ( product J2) holds W in L iff ex V be Subset of ( product J1) st V in K & (H .: V) = W

        proof

          let W be Subset of ( product J2);

          thus W in L implies ex V be Subset of ( product J1) st V in K & (H .: V) = W

          proof

            assume W in L;

            then

            consider j be set, T be TopStruct, W0j be Subset of T such that

             A6: j in I2 & W0j is open & T = (J2 . j) and

             A7: W = ( product (( Carrier J2) +* (j,W0j))) by WAYBEL18:def 2;

            reconsider j as Element of I2 by A6;

            reconsider Wj = W0j as Subset of (J2 . j) by A6;

            j in I2;

            then j in ( rng p) by A1, FUNCT_2:def 3;

            then

            consider i be object such that

             A8: i in I1 & (p . i) = j by FUNCT_2: 11;

            

             A9: i in ( dom p) by A8, FUNCT_2:def 1;

            reconsider i as Element of I1 by A8;

            consider f be Function of (J1 . i), ((J2 * p) . i) such that

             A10: (F . i) = f & f is being_homeomorphism by A3;

            reconsider Vi = (f " Wj) as Subset of (J1 . i);

            

             A11: the carrier of (J1 . i) = ( [#] (J1 . i)) by STRUCT_0:def 3

            .= (( Carrier J1) . i) by PENCIL_3: 7;

            i in ( dom ( Carrier J1)) by A8, PARTFUN1:def 2;

            then ( product (( Carrier J1) +* (i,Vi))) c= ( product ( Carrier J1)) by A11, Th39;

            then

            reconsider V = ( product (( Carrier J1) +* (i,Vi))) as Subset of ( product J1) by WAYBEL18:def 3;

            take V;

            

             A12: V is Subset of ( product ( Carrier J1)) by WAYBEL18:def 3;

            ex k be set, S be TopStruct, U be Subset of S st k in I1 & U is open & S = (J1 . k) & V = ( product (( Carrier J1) +* (k,U)))

            proof

              take i, (J1 . i), Vi;

              reconsider W1j = Wj as Subset of ((J2 * p) . i) by A8, A9, FUNCT_1: 13;

              W0j in the topology of (J2 . j) by A6, PRE_TOPC:def 2;

              then W1j in the topology of ((J2 * p) . i) by A8, A9, FUNCT_1: 13;

              then

               A14: W1j is open by PRE_TOPC:def 2;

              ( [#] ((J2 * p) . i)) = {} implies ( [#] (J1 . i)) = {} ;

              hence thesis by A10, A14, TOPS_2: 43;

            end;

            hence V in K by A12, WAYBEL18:def 2;

            reconsider f0 = f as one-to-one Function by A10;

            ( rng f0) = ( [#] ((J2 * p) . i)) by A10, TOPS_2:def 5

            .= ( [#] (J2 . j)) by A9, A8, FUNCT_1: 13

            .= the carrier of (J2 . j) by STRUCT_0:def 3;

            then (f .: (f " Wj)) = Wj by FUNCT_1: 77;

            hence (H .: V) = W by A1, A3, A4, A7, A8, Th76, A10;

          end;

          given V be Subset of ( product J1) such that

           A16: V in K & (H .: V) = W;

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

           A17: i in I1 & Vi is open & S = (J1 . i) and

           A18: V = ( product (( Carrier J1) +* (i,Vi))) by A16, WAYBEL18:def 2;

          reconsider i as Element of I1 by A17;

          reconsider Vi as Subset of (J1 . i) by A17;

          

           A19: W is Subset of ( product ( Carrier J2)) by WAYBEL18:def 3;

          ex j be set, T be TopStruct, U be Subset of T st j in I2 & U is open & T = (J2 . j) & W = ( product (( Carrier J2) +* (j,U)))

          proof

            reconsider j = (p . i) as Element of I2;

            consider f be Function of (J1 . i), ((J2 * p) . i) such that

             A20: (F . i) = f & f is being_homeomorphism by A3;

            

             a21: i in ( dom p) by A17, FUNCT_2:def 1;

            then

             A21: ((J2 * p) . i) = (J2 . j) by FUNCT_1: 13;

            reconsider Wj = (f .: Vi) as Subset of (J2 . j) by a21, FUNCT_1: 13;

            take j, (J2 . j), Wj;

            thus j in I2 & Wj is open & (J2 . j) = (J2 . j) by A21, A17, A20, T_0TOPSP:def 2;

            thus W = ( product (( Carrier J2) +* (j,Wj))) by A16, A1, A3, A4, A18, A20, Th76;

          end;

          hence W in L by A19, WAYBEL18:def 2;

        end;

        hence (H .: K) = L by FUNCT_2:def 10;

      end;

      hence thesis by A5, Th48;

    end;

    theorem :: TOPS_5:79

    

     Th79: for I1,I2 be non empty set holds for J1 be TopSpace-yielding non-Empty ManySortedSet of I1 holds for J2 be TopSpace-yielding non-Empty ManySortedSet of I2 holds for p be Function of I1, I2 st p is bijective & for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic holds (( product J1),( product J2)) are_homeomorphic

    proof

      let I1,I2 be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;

      let p be Function of I1, I2;

      assume that

       A1: p is bijective and

       A2: for i be Element of I1 holds ((J1 . i),((J2 * p) . i)) are_homeomorphic ;

      set H = the ProductHomeo of J1, J2, p;

      H is being_homeomorphism by A1, A2, Th78;

      hence thesis by T_0TOPSP:def 1;

    end;

    theorem :: TOPS_5:80

    for I be non empty set holds for J1,J2 be TopSpace-yielding non-Empty ManySortedSet of I holds for p be Permutation of I st for i be Element of I holds ((J1 . i),((J2 * p) . i)) are_homeomorphic holds (( product J1),( product J2)) are_homeomorphic by Th79;

    theorem :: TOPS_5:81

    for I be non empty set holds for J be TopSpace-yielding non-Empty ManySortedSet of I holds for p be Permutation of I holds (( product J),( product (J * p))) are_homeomorphic

    proof

      let I be non empty set;

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

      let p be Permutation of I;

      reconsider q = (p " ) as Permutation of I;

      now

        let i be Element of I;

        

         A1: J = (J * ( id ( dom J))) by RELAT_1: 52

        .= (J * ( id I)) by PARTFUN1:def 2

        .= (J * (p * q)) by FUNCT_2: 61

        .= ((J * p) * q) by RELAT_1: 36;

        thus ((J . i),(((J * p) * q) . i)) are_homeomorphic by A1;

      end;

      hence (( product J),( product (J * p))) are_homeomorphic by Th79;

    end;

    theorem :: TOPS_5:82

    for I be non empty set holds for J1,J2 be TopSpace-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J1 . i) is SubSpace of (J2 . i) holds ( product J1) is SubSpace of ( product J2)

    proof

      let I be non empty set;

      let J1 be TopSpace-yielding non-Empty ManySortedSet of I;

      let J2 be TopSpace-yielding non-Empty ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J1 . i) is SubSpace of (J2 . i);

      ex K1 be prebasis of ( product J1), K2 be prebasis of ( product J2) st ( [#] ( product J1)) in K1 & K1 = ( INTERSECTION (K2, {( [#] ( product J1))}))

      proof

        reconsider K1 = ( product_prebasis J1) as prebasis of ( product J1) by WAYBEL18:def 3;

        reconsider K2 = ( product_prebasis J2) as prebasis of ( product J2) by WAYBEL18:def 3;

        take K1, K2;

        

         A2: ( [#] ( product J1)) = the carrier of ( product J1) by STRUCT_0:def 3

        .= ( product ( Carrier J1)) by WAYBEL18:def 3;

        then ( [#] ( product J1)) = ( [#] ( product ( Carrier J1))) by SUBSET_1:def 3;

        then

        reconsider P = ( [#] ( product J1)) as Subset of ( product ( Carrier J1));

        ex i be set, T be TopStruct, V be Subset of T st i in I & V is open & T = (J1 . i) & P = ( product (( Carrier J1) +* (i,V)))

        proof

          set i = the Element of I;

          take i, (J1 . i), ( [#] (J1 . i));

          thus i in I & ( [#] (J1 . i)) is open & (J1 . i) = (J1 . i);

          

          thus P = ( product (( Carrier J1) +* (i,(( Carrier J1) . i)))) by A2, FUNCT_7: 35

          .= ( product (( Carrier J1) +* (i,( [#] (J1 . i))))) by PENCIL_3: 7;

        end;

        hence ( [#] ( product J1)) in K1 by WAYBEL18:def 2;

        for U be set holds U in K1 iff ex A,P0 be set st A in K2 & P0 in {( [#] ( product J1))} & U = (A /\ P0)

        proof

          let U be set;

          

           A3: for i be Element of I, V be Subset of (J1 . i), W be Subset of (J2 . i) st V = (W /\ ( [#] (J1 . i))) holds (( Carrier J1) +* (i,V)) = ((( Carrier J2) +* (i,W)) (/\) ( Carrier J1))

          proof

            let i be Element of I, V be Subset of (J1 . i), W be Subset of (J2 . i);

            assume

             A4: V = (W /\ ( [#] (J1 . i)));

            

             A5: ( dom (( Carrier J1) +* (i,V))) = I by PARTFUN1:def 2

            .= ( dom ((( Carrier J2) +* (i,W)) (/\) ( Carrier J1))) by PARTFUN1:def 2;

            for x be object st x in ( dom (( Carrier J1) +* (i,V))) holds ((( Carrier J1) +* (i,V)) . x) = (((( Carrier J2) +* (i,W)) (/\) ( Carrier J1)) . x)

            proof

              let x be object;

              assume

               a6: x in ( dom (( Carrier J1) +* (i,V)));

              then

               A6: x in ( dom ( Carrier J1)) by FUNCT_7: 30;

              

               A7: x in I by a6;

              reconsider j = x as Element of I by a6;

              

               A8: x in ( dom ( Carrier J2)) by A7, PARTFUN1:def 2;

              per cases ;

                suppose

                 A9: x = i;

                

                hence ((( Carrier J1) +* (i,V)) . x) = V by A6, FUNCT_7: 31

                .= (((( Carrier J2) +* (i,W)) . x) /\ ( [#] (J1 . i))) by A4, A8, A9, FUNCT_7: 31

                .= (((( Carrier J2) +* (i,W)) . x) /\ (( Carrier J1) . i)) by PENCIL_3: 7

                .= (((( Carrier J2) +* (i,W)) (/\) ( Carrier J1)) . x) by A9, PBOOLE:def 5;

              end;

                suppose

                 A10: x <> i;

                

                 A11: (( Carrier J1) . j) = ( [#] (J1 . j)) & (( Carrier J2) . j) = ( [#] (J2 . j)) by PENCIL_3: 7;

                

                 a12: (J1 . j) is SubSpace of (J2 . j) by A1;

                

                thus ((( Carrier J1) +* (i,V)) . x) = (( Carrier J1) . x) by A10, FUNCT_7: 32

                .= ((( Carrier J2) . x) /\ (( Carrier J1) . x)) by a12, XBOOLE_1: 28, A11, PRE_TOPC:def 4

                .= (((( Carrier J2) +* (i,W)) . x) /\ (( Carrier J1) . x)) by A10, FUNCT_7: 32

                .= (((( Carrier J2) +* (i,W)) (/\) ( Carrier J1)) . x) by a6, PBOOLE:def 5;

              end;

            end;

            hence (( Carrier J1) +* (i,V)) = ((( Carrier J2) +* (i,W)) (/\) ( Carrier J1)) by A5, FUNCT_1: 2;

          end;

          thus U in K1 implies ex A,P0 be set st A in K2 & P0 in {( [#] ( product J1))} & U = (A /\ P0)

          proof

            assume U in K1;

            then

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

             A13: i in I & V is open & T = (J1 . i) and

             A14: U = ( product (( Carrier J1) +* (i,V))) by WAYBEL18:def 2;

            reconsider i as Element of I by A13;

            

             A15: V in the topology of (J1 . i) by A13, PRE_TOPC:def 2;

            reconsider V as Subset of (J1 . i) by A13;

            (J1 . i) is SubSpace of (J2 . i) by A1;

            then

            consider W be Subset of (J2 . i) such that

             A16: W in the topology of (J2 . i) & V = (W /\ ( [#] (J1 . i))) by A15, PRE_TOPC:def 4;

            set A = ( product (( Carrier J2) +* (i,W)));

            take A, P;

            (( Carrier J2) . i) = ( [#] (J2 . i)) by PENCIL_3: 7

            .= the carrier of (J2 . i) by STRUCT_0:def 3;

            then i in ( dom ( Carrier J2)) & W c= (( Carrier J2) . i) by A13, PARTFUN1:def 2;

            then

             A17: A is Subset of ( product ( Carrier J2)) by Th39;

            ex i9 be set, T9 be TopStruct, V9 be Subset of T9 st i9 in I & V9 is open & T9 = (J2 . i9) & A = ( product (( Carrier J2) +* (i9,V9))) by A16, PRE_TOPC:def 2;

            hence A in K2 by A17, WAYBEL18:def 2;

            thus P in {( [#] ( product J1))} by TARSKI:def 1;

            

            thus U = ( product ((( Carrier J2) +* (i,W)) (/\) ( Carrier J1))) by A14, A16, A3

            .= (A /\ P) by A2, Th33;

          end;

          given A,P0 be set such that

           A18: A in K2 & P0 in {( [#] ( product J1))} & U = (A /\ P0);

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

           A19: i in I & W is open & T = (J2 . i) and

           A20: A = ( product (( Carrier J2) +* (i,W))) by A18, WAYBEL18:def 2;

          reconsider i as Element of I by A19;

          

           A21: W in the topology of (J2 . i) by A19, PRE_TOPC:def 2;

          reconsider W as Subset of (J2 . i) by A19;

          set V = (W /\ ( [#] (J1 . i)));

          

           A22: V c= ( [#] (J1 . i)) by XBOOLE_1: 17;

          reconsider V as Subset of (J1 . i);

          P0 = ( product ( Carrier J1)) by A2, A18, TARSKI:def 1;

          

          then

           A23: U = ( product ((( Carrier J2) +* (i,W)) (/\) ( Carrier J1))) by A18, A20, Th33

          .= ( product (( Carrier J1) +* (i,V))) by A3;

          

           A24: i in ( dom ( Carrier J1)) by A19, PARTFUN1:def 2;

          V c= (( Carrier J1) . i) by A22, PENCIL_3: 7;

          then

           A25: U c= ( product ( Carrier J1)) by A23, A24, Th39;

          ex i9 be set, T9 be TopStruct, V9 be Subset of T9 st i9 in I & V9 is open & T9 = (J1 . i9) & U = ( product (( Carrier J1) +* (i9,V9)))

          proof

            take i, (J1 . i), V;

            thus i in I;

            (J1 . i) is SubSpace of (J2 . i) by A1;

            then V in the topology of (J1 . i) by A21, PRE_TOPC:def 4;

            hence thesis by A23, PRE_TOPC:def 2;

          end;

          hence U in K1 by A25, WAYBEL18:def 2;

        end;

        hence thesis by SETFAM_1:def 5;

      end;

      hence thesis by Th51;

    end;