fintopo5.miz



    begin

    theorem :: FINTOPO5:1

    

     Th1: for X be set, Y be non empty set, f be Function of X, Y, A be Subset of X st f is one-to-one holds ((f " ) .: (f .: A)) = A

    proof

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

      

       A1: ( dom f) = X by FUNCT_2:def 1;

      assume f is one-to-one;

      hence thesis by A1, FUNCT_1: 107;

    end;

    theorem :: FINTOPO5:2

    for n be Nat holds n > 0 iff ( Seg n) <> {} ;

    definition

      let FT1,FT2 be RelStr, h be Function of FT1, FT2;

      :: FINTOPO5:def1

      attr h is being_homeomorphism means h is one-to-one onto & for x be Element of FT1 holds (h .: ( U_FT x)) = ( Im (the InternalRel of FT2,(h . x)));

    end

    theorem :: FINTOPO5:3

    

     Th3: for FT1,FT2 be non empty RelStr, h be Function of FT1, FT2 st h is being_homeomorphism holds ex g be Function of FT2, FT1 st g = (h " ) & g is being_homeomorphism

    proof

      let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2;

      assume

       A1: h is being_homeomorphism;

      then

       A2: h is one-to-one onto;

      then

       A3: ( rng h) = the carrier of FT2 by FUNCT_2:def 3;

      then

      reconsider g2 = (h " ) as Function of FT2, FT1 by A2, FUNCT_2: 25;

      

       A4: for y be Element of FT2 holds (g2 .: ( U_FT y)) = ( Im (the InternalRel of FT1,(g2 . y)))

      proof

        let y be Element of FT2;

        reconsider x = (g2 . y) as Element of FT1;

        y = (h . x) & (h .: ( U_FT x)) = ( Im (the InternalRel of FT2,(h . x))) by A1, A3, FUNCT_1: 35;

        hence thesis by A2, Th1;

      end;

      ( rng g2) = ( dom h) by A2, FUNCT_1: 33

      .= the carrier of FT1 by FUNCT_2:def 1;

      then

       A5: g2 is onto by FUNCT_2:def 3;

      g2 is one-to-one by A2, FUNCT_1: 40;

      then g2 is being_homeomorphism by A5, A4;

      hence thesis;

    end;

    theorem :: FINTOPO5:4

    

     Th4: for FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat, x be Element of FT1, y be Element of FT2 st h is being_homeomorphism & y = (h . x) holds for z be Element of FT1 holds z in ( U_FT (x,n)) iff (h . z) in ( U_FT (y,n))

    proof

      let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat, x be Element of FT1, y be Element of FT2;

      assume that

       A1: h is being_homeomorphism and

       A2: y = (h . x);

      

       A3: h is one-to-one onto by A1;

      let z be Element of FT1;

      x in the carrier of FT1;

      then

       A4: x in ( dom h) by FUNCT_2:def 1;

      z in the carrier of FT1;

      then

       A5: z in ( dom h) by FUNCT_2:def 1;

       A6:

      now

        defpred P[ Nat] means for w be Element of FT2 holds w in ( U_FT (y,$1)) implies ((h " ) . w) in ( U_FT (x,$1));

        assume

         A7: (h . z) in ( U_FT (y,n));

        consider g be Function of FT2, FT1 such that

         A8: g = (h " ) and

         A9: g is being_homeomorphism by A1, Th3;

        

         A10: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A11: P[k];

          for w be Element of FT2 holds w in ( U_FT (y,(k + 1))) implies ((h " ) . w) in ( U_FT (x,(k + 1)))

          proof

            let w be Element of FT2;

            

             A12: ( U_FT (y,(k + 1))) = (( U_FT (y,k)) ^f ) by FINTOPO3: 48;

            assume w in ( U_FT (y,(k + 1)));

            then

            consider x3 be Element of FT2 such that

             A13: x3 = w and

             A14: ex y3 be Element of FT2 st y3 in ( U_FT (y,k)) & x3 in ( U_FT y3) by A12;

            consider y2 be Element of FT2 such that

             A15: y2 in ( U_FT (y,k)) and

             A16: x3 in ( U_FT y2) by A14;

            reconsider q = (g . y2), p = (g . x3) as Element of FT1;

            

             A17: for w2 be Element of FT2 holds w2 in ( U_FT (y2, 0 )) implies ((h " ) . w2) in ( U_FT (q, 0 ))

            proof

              let w2 be Element of FT2;

              w2 in the carrier of FT2;

              then

               A18: w2 in ( dom g) by FUNCT_2:def 1;

              

               A19: ((h " ) .: ( U_FT y2)) = ( Class (the InternalRel of FT1,((h " ) . y2))) by A8, A9;

              hereby

                assume w2 in ( U_FT (y2, 0 ));

                then w2 in ( U_FT y2) by FINTOPO3: 47;

                then ((h " ) . w2) in ( U_FT q) by A8, A19, A18, FUNCT_1:def 6;

                hence ((h " ) . w2) in ( U_FT (q, 0 )) by FINTOPO3: 47;

              end;

            end;

            x3 in ( U_FT (y2, 0 )) by A16, FINTOPO3: 47;

            then p in ( U_FT (q, 0 )) by A8, A17;

            then

             A20: p in ( U_FT q) by FINTOPO3: 47;

            q in ( U_FT (x,k)) by A8, A11, A15;

            then p in (( U_FT (x,k)) ^f ) by A20;

            hence thesis by A8, A13, FINTOPO3: 48;

          end;

          hence thesis;

        end;

        

         A21: (g . y) = x by A2, A4, A3, A8, FUNCT_1: 34;

        for w be Element of FT2 holds w in ( U_FT (y, 0 )) implies ((h " ) . w) in ( U_FT (x, 0 ))

        proof

          let w be Element of FT2;

          w in the carrier of FT2;

          then

           A22: w in ( dom g) by FUNCT_2:def 1;

          

           A23: (g .: ( U_FT y)) = ( Class (the InternalRel of FT1,(g . y))) by A9;

          hereby

            assume w in ( U_FT (y, 0 ));

            then w in ( U_FT y) by FINTOPO3: 47;

            then (g . w) in ( U_FT x) by A21, A23, A22, FUNCT_1:def 6;

            hence ((h " ) . w) in ( U_FT (x, 0 )) by A8, FINTOPO3: 47;

          end;

        end;

        then

         A24: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A24, A10);

        then ((h " ) . (h . z)) in ( U_FT (x,n)) by A7;

        hence z in ( U_FT (x,n)) by A3, A5, FUNCT_1: 34;

      end;

      now

        defpred P[ Nat] means for w be Element of FT1 holds w in ( U_FT (x,$1)) implies (h . w) in ( U_FT (y,$1));

        assume

         A25: z in ( U_FT (x,n));

        

         A26: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A27: P[k];

          for w be Element of FT1 holds w in ( U_FT (x,(k + 1))) implies (h . w) in ( U_FT (y,(k + 1)))

          proof

            let w be Element of FT1;

            

             A28: ( U_FT (x,(k + 1))) = (( U_FT (x,k)) ^f ) by FINTOPO3: 48;

            assume w in ( U_FT (x,(k + 1)));

            then

            consider x3 be Element of FT1 such that

             A29: x3 = w and

             A30: ex y3 be Element of FT1 st y3 in ( U_FT (x,k)) & x3 in ( U_FT y3) by A28;

            consider y2 be Element of FT1 such that

             A31: y2 in ( U_FT (x,k)) and

             A32: x3 in ( U_FT y2) by A30;

            reconsider q = (h . y2), p = (h . x3) as Element of FT2;

            

             A33: for w2 be Element of FT1 holds w2 in ( U_FT (y2, 0 )) implies (h . w2) in ( U_FT (q, 0 ))

            proof

              let w2 be Element of FT1;

              w2 in the carrier of FT1;

              then

               A34: w2 in ( dom h) by FUNCT_2:def 1;

              

               A35: (h .: ( U_FT y2)) = ( Class (the InternalRel of FT2,(h . y2))) by A1;

              hereby

                assume w2 in ( U_FT (y2, 0 ));

                then w2 in ( U_FT y2) by FINTOPO3: 47;

                then (h . w2) in ( U_FT q) by A35, A34, FUNCT_1:def 6;

                hence (h . w2) in ( U_FT (q, 0 )) by FINTOPO3: 47;

              end;

            end;

            x3 in ( U_FT (y2, 0 )) by A32, FINTOPO3: 47;

            then p in ( U_FT (q, 0 )) by A33;

            then

             A36: p in ( U_FT q) by FINTOPO3: 47;

            q in ( U_FT (y,k)) by A27, A31;

            then p in (( U_FT (y,k)) ^f ) by A36;

            hence thesis by A29, FINTOPO3: 48;

          end;

          hence thesis;

        end;

        for w be Element of FT1 holds w in ( U_FT (x, 0 )) implies (h . w) in ( U_FT (y, 0 ))

        proof

          let w be Element of FT1;

          w in the carrier of FT1;

          then

           A37: w in ( dom h) by FUNCT_2:def 1;

          

           A38: (h .: ( U_FT x)) = ( Class (the InternalRel of FT2,(h . x))) by A1;

          hereby

            assume w in ( U_FT (x, 0 ));

            then w in ( U_FT x) by FINTOPO3: 47;

            then (h . w) in ( U_FT y) by A2, A38, A37, FUNCT_1:def 6;

            hence (h . w) in ( U_FT (y, 0 )) by FINTOPO3: 47;

          end;

        end;

        then

         A39: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A39, A26);

        hence (h . z) in ( U_FT (y,n)) by A25;

      end;

      hence thesis by A6;

    end;

    theorem :: FINTOPO5:5

    for FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat, x be Element of FT1, y be Element of FT2 st h is being_homeomorphism & y = (h . x) holds for v be Element of FT2 holds ((h " ) . v) in ( U_FT (x,n)) iff v in ( U_FT (y,n))

    proof

      let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat, x be Element of FT1, y be Element of FT2;

      assume that

       A1: h is being_homeomorphism and

       A2: y = (h . x);

      x in the carrier of FT1;

      then

       A3: x in ( dom h) by FUNCT_2:def 1;

      consider g be Function of FT2, FT1 such that

       A4: g = (h " ) and

       A5: g is being_homeomorphism by A1, Th3;

      h is one-to-one onto by A1;

      then x = (g . y) by A2, A4, A3, FUNCT_1: 34;

      hence thesis by A4, A5, Th4;

    end;

    theorem :: FINTOPO5:6

    for n be non zero Nat, f be Function of ( FTSL1 n), ( FTSL1 n) st f is_continuous 0 holds ex p be Element of ( FTSL1 n) st (f . p) in ( U_FT (p, 0 ))

    proof

      let n be non zero Nat, f be Function of ( FTSL1 n), ( FTSL1 n);

      assume

       A1: f is_continuous 0 ;

      assume

       A2: for p be Element of ( FTSL1 n) holds not (f . p) in ( U_FT (p, 0 ));

      defpred P2[ Nat] means $1 > 0 & for j be Nat st $1 <= n & j = (f . $1) holds $1 > j;

      

       A3: n >= ( 0 + 1) by NAT_1: 13;

      

       A4: RelStr (# ( Seg n), ( Nbdl1 n) #) = ( FTSL1 n) by FINTOPO4:def 4;

      

       A5: ( FTSL1 n) is filled by FINTOPO4: 18;

      now

        

         A6: n in the carrier of ( FTSL1 n) by A3, A4;

        then

        reconsider p2 = n as Element of ( FTSL1 n);

        p2 in ( U_FT p2) by A5;

        then

         A7: p2 in ( U_FT (p2, 0 )) by FINTOPO3: 47;

        given j be Nat such that

         A8: j = (f . n) and

         A9: n <= j;

        (f . n) in the carrier of ( FTSL1 n) by A6, FUNCT_2: 5;

        then j <= n by A4, A8, FINSEQ_1: 1;

        then n = j by A9, XXREAL_0: 1;

        hence contradiction by A2, A8, A7;

      end;

      then

       A10: for j be Nat st n <= n & j = (f . n) holds n > j;

      then

       A11: ex k be Nat st P2[k];

      ex k be Nat st P2[k] & for m be Nat st P2[m] holds k <= m from NAT_1:sch 5( A11);

      then

      consider k be Nat such that

       A12: P2[k] and

       A13: for m be Nat st P2[m] holds k <= m;

      

       A14: ( 0 + 1) <= k by A12, NAT_1: 13;

      then

       A15: (k - 1) >= 0 by XREAL_1: 48;

      then

       A16: (k - 1) = (k -' 1) by XREAL_0:def 2;

      

       A17: k <= n by A10, A13;

      then

      reconsider pk = k as Element of ( FTSL1 n) by A4, A14, FINSEQ_1: 1;

      k < (k + 1) by NAT_1: 13;

      then

       A18: (k - 1) < ((k + 1) - 1) by XREAL_1: 9;

      now

        per cases by A13, A16, A18;

          case

           A19: (k -' 1) <= 0 ;

          1 in the carrier of ( FTSL1 n) by A3, A4;

          then

           A20: (f . 1) in ( Seg n) by A4, FUNCT_2: 5;

          then

          reconsider j0 = (f . 1) as Nat;

          (k - 1) = 0 by A15, A19, XREAL_0:def 2;

          then 1 > j0 by A3, A12;

          hence contradiction by A20, FINSEQ_1: 1;

        end;

          case

           A21: (k -' 1) > 0 & ex j be Nat st (k -' 1) <= n & j = (f . (k -' 1)) & (k -' 1) <= j;

          

           A22: k in the carrier of ( FTSL1 n) by A4, A17, A14;

          then

           A23: (f . k) in ( Seg n) by A4, FUNCT_2: 5;

          then

          reconsider jn = (f . k) as Nat;

          jn < (jn + 1) by NAT_1: 13;

          then

           A24: (jn - 1) < ((jn + 1) - 1) by XREAL_1: 9;

          

           A25: (k -' 1) >= ( 0 + 1) by A21, NAT_1: 13;

          then

           A26: (k -' 1) = k or (k -' 1) = ( max ((k -' 1),1)) or (k -' 1) = ( min ((k + 1),n)) by XXREAL_0:def 10;

          consider j be Nat such that

           A27: (k -' 1) <= n and

           A28: j = (f . (k -' 1)) and

           A29: (k -' 1) <= j by A21;

          reconsider pkm = (k -' 1) as Element of ( FTSL1 n) by A4, A27, A25, FINSEQ_1: 1;

          (k -' 1) in ( Seg n) by A27, A25;

          then

           A30: ( Im (( Nbdl1 n),pkm)) = {(k -' 1), ( max (((k -' 1) -' 1),1)), ( min (((k -' 1) + 1),n))} by FINTOPO4:def 3;

          ( Im (( Nbdl1 n),k)) = {k, ( max ((k -' 1),1)), ( min ((k + 1),n))} by A4, A22, FINTOPO4:def 3;

          then (k -' 1) in ( U_FT pk) by A4, A26, ENUMSET1:def 1;

          then

           A31: (k -' 1) in ( U_FT (pk, 0 )) by FINTOPO3: 47;

          reconsider pfk = jn as Element of ( FTSL1 n) by A22, FUNCT_2: 5;

          

           A32: (f .: ( U_FT (pk, 0 ))) c= ( U_FT (pfk, 0 )) by A1, FINTOPO4:def 2;

          

           A33: jn < k by A12, A17;

          then

           A34: (jn + 1) <= k by NAT_1: 13;

          

           A35: (k -' 1) in the carrier of ( FTSL1 n) by A4, A27, A25;

          now

            assume

             A36: (k -' 1) = j;

            then

            reconsider pj = j as Element of ( FTSL1 n) by A35;

            pj in ( U_FT pj) by A5;

            then (f . j) in ( U_FT (pj, 0 )) by A28, A36, FINTOPO3: 47;

            hence contradiction by A2;

          end;

          then (k -' 1) < j by A29, XXREAL_0: 1;

          then

           A37: ((k -' 1) + 1) <= j by NAT_1: 13;

          then

           A38: jn < j by A16, A33, XXREAL_0: 2;

          j in the carrier of ( FTSL1 n) by A28, A35, FUNCT_2: 5;

          then

           A39: j <= n by A4, FINSEQ_1: 1;

          now

            assume

             A40: k = j;

            then ( min (((k -' 1) + 1),n)) = ((k -' 1) + 1) by A16, A39, XXREAL_0:def 9;

            then k in ( U_FT pkm) by A4, A16, A30, ENUMSET1:def 1;

            then (f . (k -' 1)) in ( U_FT (pkm, 0 )) by A28, A40, FINTOPO3: 47;

            hence contradiction by A2;

          end;

          then

           A41: k < j by A16, A37, XXREAL_0: 1;

           A42:

          now

            per cases ;

              case (jn + 1) <= n;

              hence j <> ( min ((jn + 1),n)) by A41, A34, XXREAL_0:def 9;

            end;

              case

               A43: (jn + 1) > n;

              then jn >= n by NAT_1: 13;

              hence j <> ( min ((jn + 1),n)) by A38, A43, XXREAL_0:def 9;

            end;

          end;

          

           A44: 1 <= jn by A23, FINSEQ_1: 1;

          then (jn - 1) >= 0 by XREAL_1: 48;

          then

           A45: (jn - 1) = (jn -' 1) by XREAL_0:def 2;

           A46:

          now

            per cases ;

              suppose (jn -' 1) >= 1;

              hence j <> ( max ((jn -' 1),1)) by A38, A45, A24, XXREAL_0:def 10;

            end;

              suppose (jn -' 1) < 1;

              hence j <> ( max ((jn -' 1),1)) by A44, A38, XXREAL_0:def 10;

            end;

          end;

          (k -' 1) in ( dom f) by A35, FUNCT_2:def 1;

          then (f . (k -' 1)) in (f .: ( U_FT (pk, 0 ))) by A31, FUNCT_1:def 6;

          then

           A47: j in ( U_FT (pfk, 0 )) by A28, A32;

          ( Im (( Nbdl1 n),jn)) = {jn, ( max ((jn -' 1),1)), ( min ((jn + 1),n))} by A23, FINTOPO4:def 3;

          then not j in ( U_FT pfk) by A4, A16, A37, A33, A46, A42, ENUMSET1:def 1;

          hence contradiction by A47, FINTOPO3: 47;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO5:7

    

     Th7: for T be non empty RelStr, p be Element of T, k be Nat st T is filled holds ( U_FT (p,k)) c= ( U_FT (p,(k + 1)))

    proof

      let T be non empty RelStr, p be Element of T, k be Nat;

      

       A1: ( U_FT (p,(k + 1))) = (( U_FT (p,k)) ^f ) by FINTOPO3: 48;

      assume T is filled;

      hence thesis by A1, FINTOPO3: 1;

    end;

    theorem :: FINTOPO5:8

    

     Th8: for T be non empty RelStr, p be Element of T, k be Nat st T is filled holds ( U_FT (p, 0 )) c= ( U_FT (p,k))

    proof

      let T be non empty RelStr, p be Element of T, k be Nat;

      defpred P[ Nat] means ( U_FT (p, 0 )) c= ( U_FT (p,$1));

      assume

       A1: T is filled;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: P[k];

        ( U_FT (p,k)) c= ( U_FT (p,(k + 1))) by A1, Th7;

        hence thesis by A3, XBOOLE_1: 1;

      end;

      

       A4: P[ 0 ];

      for i be Nat holds P[i] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: FINTOPO5:9

    

     Th9: for n be non zero Nat, jn,j,k be Nat, p be Element of ( FTSL1 n) st p = jn holds j in ( U_FT (p,k)) iff j in ( Seg n) & |.(jn - j).| <= (k + 1)

    proof

      let n be non zero Nat, jn,j,k be Nat, p be Element of ( FTSL1 n);

      

       A1: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

      assume

       A2: p = jn;

       A3:

      now

        defpred P[ Nat] means for j2,jn2 be Nat, p2 be Element of ( FTSL1 n) st jn2 = p2 & j2 in ( Seg n) & |.(jn2 - j2).| <= ($1 + 1) holds j2 in ( U_FT (p2,$1));

        

         A4: P[ 0 ]

        proof

          let j2,jn2 be Nat, p2 be Element of ( FTSL1 n);

          assume that

           A5: jn2 = p2 and

           A6: j2 in ( Seg n) and

           A7: |.(jn2 - j2).| <= ( 0 + 1);

          

           A8: j2 <= n by A6, FINSEQ_1: 1;

          

           A9: 1 <= j2 by A6, FINSEQ_1: 1;

          now

            per cases ;

              case (jn2 - j2) >= 0 ;

              then

               A10: (jn2 - j2) = (jn2 -' j2) by XREAL_0:def 2;

              

               A11: (jn2 -' j2) >= ( 0 + 1) or (jn2 -' j2) = 0 by NAT_1: 13;

              (jn2 - j2) <= 1 by A7, ABSVALUE:def 1;

              then

               A12: (jn2 - j2) = 1 or (jn2 -' j2) = 0 by A10, A11, XXREAL_0: 1;

              per cases by A10, A12;

                suppose

                 A13: (jn2 - 1) = j2;

                then (jn2 - 1) = (jn2 -' 1) by XREAL_0:def 2;

                hence j2 = jn2 or j2 = ( max ((jn2 -' 1),1)) or j2 = ( min ((jn2 + 1),n)) by A9, A13, XXREAL_0:def 10;

              end;

                suppose jn2 = j2;

                hence j2 = jn2 or j2 = ( max ((jn2 -' 1),1)) or j2 = ( min ((jn2 + 1),n));

              end;

            end;

              case

               A14: (jn2 - j2) < 0 ;

              then ((jn2 - j2) + j2) < ( 0 + j2) by XREAL_1: 8;

              then

               A15: (jn2 + 1) <= j2 by NAT_1: 13;

              ( - (jn2 - j2)) <= 1 by A7, A14, ABSVALUE:def 1;

              then ((j2 - jn2) + jn2) <= (1 + jn2) by XREAL_1: 7;

              then (jn2 + 1) = j2 by A15, XXREAL_0: 1;

              hence j2 = jn2 or j2 = ( max ((jn2 -' 1),1)) or j2 = ( min ((jn2 + 1),n)) by A8, XXREAL_0:def 9;

            end;

          end;

          then jn2 in NAT & j2 in {jn2, ( max ((jn2 -' 1),1)), ( min ((jn2 + 1),n))} by ENUMSET1:def 1, ORDINAL1:def 12;

          then j2 in ( U_FT p2) by A1, A5, FINTOPO4:def 3;

          hence thesis by FINTOPO3: 47;

        end;

        

         A16: for jj be Nat st P[jj] holds P[(jj + 1)]

        proof

          let jj be Nat;

          assume

           A17: P[jj];

          let j2,jn2 be Nat, p2 be Element of ( FTSL1 n);

          assume that

           A18: jn2 = p2 and

           A19: j2 in ( Seg n) and

           A20: |.(jn2 - j2).| <= ((jj + 1) + 1);

          

           A21: j2 <= n by A19, FINSEQ_1: 1;

          reconsider x0 = j2 as Element of ( FTSL1 n) by A1, A19;

          

           A22: 1 <= j2 by A19, FINSEQ_1: 1;

          

           A23: jn2 <= n by A1, A18, FINSEQ_1: 1;

          

           A24: 1 <= jn2 by A1, A18, FINSEQ_1: 1;

           A25:

          now

            per cases ;

              suppose

               A26: (jn2 - j2) >= 0 ;

              per cases by A26;

                suppose

                 A27: (jn2 - j2) = 0 ;

                ( FTSL1 n) is filled by FINTOPO4: 18;

                then

                 A28: x0 in ( U_FT p2) by A18, A27;

                 |.(jn2 - j2).| <= (jj + 1) by A27, ABSVALUE:def 1;

                hence ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,jj)) & x0 in ( U_FT y) by A17, A18, A19, A27, A28;

              end;

                suppose

                 A29: (jn2 - j2) > 0 ;

                then (jn2 - j2) = (jn2 -' j2) by XREAL_0:def 2;

                then

                 A30: (jn2 - j2) >= ( 0 + 1) by A29, NAT_1: 13;

                then ((jn2 - j2) + j2) >= (1 + j2) by XREAL_1: 7;

                then

                 A31: n >= (j2 + 1) by A23, XXREAL_0: 2;

                j2 < (j2 + 1) by NAT_1: 13;

                then

                 A32: (jn2 - (j2 + 1)) < (jn2 - j2) by XREAL_1: 15;

                 |.(jn2 - j2).| = (jn2 - j2) by A29, ABSVALUE:def 1;

                then

                 A33: (jn2 - (j2 + 1)) < ((jj + 1) + 1) by A20, A32, XXREAL_0: 2;

                

                 A34: ((jn2 - j2) - 1) >= (1 - 1) by A30, XREAL_1: 9;

                then (jn2 -' (j2 + 1)) = (jn2 - (j2 + 1)) by XREAL_0:def 2;

                then (jn2 - (j2 + 1)) <= (jj + 1) by A33, NAT_1: 13;

                then

                 A35: |.(jn2 - (j2 + 1)).| <= (jj + 1) by A34, ABSVALUE:def 1;

                1 <= (j2 + 1) by A22, NAT_1: 13;

                then

                 A36: (j2 + 1) in ( Seg n) by A31;

                then

                reconsider yj2 = (j2 + 1) as Element of ( FTSL1 n) by A1;

                 |.((j2 + 1) - j2).| = 1 by ABSVALUE:def 1;

                then x0 in ( U_FT (yj2, 0 )) by A4, A19;

                then x0 in ( U_FT yj2) by FINTOPO3: 47;

                hence ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,jj)) & x0 in ( U_FT y) by A17, A18, A36, A35;

              end;

            end;

              suppose (jn2 - j2) < 0 ;

              then

               A37: ((jn2 - j2) + j2) < ( 0 + j2) by XREAL_1: 6;

              then

               A38: (j2 - jn2) > 0 by XREAL_1: 50;

              (j2 - 1) >= 0 by A22, XREAL_1: 48;

              then

               A39: (j2 - 1) = (j2 -' 1) by XREAL_0:def 2;

              (jn2 + 1) <= j2 by A37, NAT_1: 13;

              then

               A40: ((jn2 + 1) - 1) <= (j2 - 1) by XREAL_1: 9;

              then ((j2 - 1) - jn2) >= 0 by XREAL_1: 48;

              then

               A41: |.((j2 -' 1) - jn2).| = ((j2 -' 1) - jn2) by A39, ABSVALUE:def 1;

              j2 < (j2 + 1) by NAT_1: 13;

              then (j2 - 1) < ((j2 + 1) - 1) by XREAL_1: 9;

              then

               A42: (j2 -' 1) < n by A21, A39, XXREAL_0: 2;

               |.(jn2 - j2).| = |.(j2 - jn2).| by UNIFORM1: 11

              .= (1 + ((j2 -' 1) - jn2)) by A39, A38, ABSVALUE:def 1

              .= (1 + |.(jn2 - (j2 -' 1)).|) by A41, UNIFORM1: 11;

              then

               A43: |.(jn2 - (j2 -' 1)).| <= (jj + 1) by A20, XREAL_1: 6;

              (j2 -' 1) >= 1 by A24, A40, A39, XXREAL_0: 2;

              then

               A44: (j2 -' 1) in ( Seg n) by A42;

              then

              reconsider pj21 = (j2 -' 1) as Element of ( FTSL1 n) by A1;

               |.((j2 -' 1) - j2).| = |.(j2 - (j2 -' 1)).| by UNIFORM1: 11

              .= 1 by A39, ABSVALUE:def 1;

              then x0 in ( U_FT (pj21, 0 )) by A4, A19;

              then x0 in ( U_FT pj21) by FINTOPO3: 47;

              hence ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,jj)) & x0 in ( U_FT y) by A17, A18, A44, A43;

            end;

          end;

          ( U_FT (p2,(jj + 1))) = (( U_FT (p2,jj)) ^f ) by FINTOPO3: 48

          .= { x where x be Element of ( FTSL1 n) : ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,jj)) & x in ( U_FT y) };

          hence thesis by A25;

        end;

        

         A45: for ii be Nat holds P[ii] from NAT_1:sch 2( A4, A16);

        assume j in ( Seg n) & |.(jn - j).| <= (k + 1);

        hence j in ( U_FT (p,k)) by A2, A45;

      end;

      now

        defpred P[ Nat] means for j2,jn2 be Nat, p2 be Element of ( FTSL1 n) st jn2 = p2 & j2 in ( U_FT (p2,$1)) holds |.(jn2 - j2).| <= ($1 + 1);

        

         A46: P[ 0 ]

        proof

          let j2,jn2 be Nat, p2 be Element of ( FTSL1 n);

          assume that

           A47: jn2 = p2 and

           A48: j2 in ( U_FT (p2, 0 ));

          

           A49: j2 in ( U_FT p2) by A48, FINTOPO3: 47;

          jn2 in NAT by ORDINAL1:def 12;

          then

           A50: ( Im (( Nbdl1 n),jn2)) = {jn2, ( max ((jn2 -' 1),1)), ( min ((jn2 + 1),n))} by A1, A47, FINTOPO4:def 3;

          

           A51: jn2 <= n by A1, A47, FINSEQ_1: 1;

          per cases by A1, A47, A49, A50, ENUMSET1:def 1;

            suppose j2 = jn2;

            hence |.(jn2 - j2).| <= ( 0 + 1) by ABSVALUE: 2;

          end;

            suppose

             A52: j2 = ( max ((jn2 -' 1),1));

            per cases ;

              suppose

               A53: (jn2 -' 1) >= 1;

              then j2 = (jn2 -' 1) by A52, XXREAL_0:def 10;

              then j2 = (jn2 - 1) by A53, NAT_D: 39;

              hence |.(jn2 - j2).| <= ( 0 + 1) by ABSVALUE:def 1;

            end;

              suppose

               A54: (jn2 -' 1) < 1;

              then (jn2 -' 1) < ( 0 + 1);

              then (jn2 -' 1) = 0 by NAT_1: 13;

              then

               A55: (1 - jn2) >= 0 by NAT_D: 36, XREAL_1: 48;

              1 <= (1 + jn2) by NAT_1: 12;

              then

               A56: (1 - jn2) <= ((1 + jn2) - jn2) by XREAL_1: 9;

              j2 = 1 by A52, A54, XXREAL_0:def 10;

              then |.(j2 - jn2).| = (1 - jn2) by A55, ABSVALUE:def 1;

              hence |.(jn2 - j2).| <= ( 0 + 1) by A56, UNIFORM1: 11;

            end;

          end;

            suppose

             A57: j2 = ( min ((jn2 + 1),n));

            per cases ;

              suppose (jn2 + 1) <= n;

              then j2 = (jn2 + 1) by A57, XXREAL_0:def 9;

              then |.(j2 - jn2).| = 1 by ABSVALUE:def 1;

              hence |.(jn2 - j2).| <= ( 0 + 1) by UNIFORM1: 11;

            end;

              suppose

               A58: (jn2 + 1) > n;

              then jn2 >= n by NAT_1: 13;

              then

               A59: jn2 = n by A51, XXREAL_0: 1;

              j2 = n by A57, A58, XXREAL_0:def 9;

              hence |.(jn2 - j2).| <= ( 0 + 1) by A59, ABSVALUE: 2;

            end;

          end;

        end;

        

         A60: for i2 be Nat st P[i2] holds P[(i2 + 1)]

        proof

          let i2 be Nat;

          assume

           A61: P[i2];

          let j3,jn3 be Nat, p2 be Element of ( FTSL1 n);

          assume that

           A62: jn3 = p2 and

           A63: j3 in ( U_FT (p2,(i2 + 1)));

          ( U_FT (p2,(i2 + 1))) = (( U_FT (p2,i2)) ^f ) by FINTOPO3: 48

          .= { x where x be Element of ( FTSL1 n) : ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,i2)) & x in ( U_FT y) };

          then

          consider x be Element of ( FTSL1 n) such that

           A64: x = j3 and

           A65: ex y be Element of ( FTSL1 n) st y in ( U_FT (p2,i2)) & x in ( U_FT y) by A63;

          consider y be Element of ( FTSL1 n) such that

           A66: y in ( U_FT (p2,i2)) and

           A67: x in ( U_FT y) by A65;

          y in ( Seg n) by A1;

          then

          reconsider iy = y as Nat;

          x in ( U_FT (y, 0 )) by A67, FINTOPO3: 47;

          then

           A68: |.(iy - j3).| <= 1 by A46, A64;

           |.(jn3 - iy).| <= (i2 + 1) by A61, A62, A66;

          then

           A69: ( |.(jn3 - iy).| + |.(iy - j3).|) <= ((i2 + 1) + 1) by A68, XREAL_1: 7;

           |.((jn3 - iy) + (iy - j3)).| <= ( |.(jn3 - iy).| + |.(iy - j3).|) by COMPLEX1: 56;

          hence |.(jn3 - j3).| <= ((i2 + 1) + 1) by A69, XXREAL_0: 2;

        end;

        

         A70: for i3 be Nat holds P[i3] from NAT_1:sch 2( A46, A60);

        assume j in ( U_FT (p,k));

        hence j in ( Seg n) & |.(jn - j).| <= (k + 1) by A2, A1, A70;

      end;

      hence thesis by A3;

    end;

    theorem :: FINTOPO5:10

    for kc,km be Nat, n be non zero Nat, f be Function of ( FTSL1 n), ( FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds ex p be Element of ( FTSL1 n) st (f . p) in ( U_FT (p,km))

    proof

      let kc,km be Nat, n be non zero Nat, f be Function of ( FTSL1 n), ( FTSL1 n);

      assume that

       A1: f is_continuous kc and

       A2: km = [/(kc / 2)\];

      assume

       A3: for p be Element of ( FTSL1 n) holds not (f . p) in ( U_FT (p,km));

      defpred P2[ Nat] means $1 > 0 & for j be Nat st $1 <= n & j = (f . $1) holds $1 > j;

      

       A4: n >= ( 0 + 1) by NAT_1: 13;

      

       A5: RelStr (# ( Seg n), ( Nbdl1 n) #) = ( FTSL1 n) by FINTOPO4:def 4;

      

       A6: ( FTSL1 n) is filled by FINTOPO4: 18;

      now

        

         A7: n in the carrier of ( FTSL1 n) by A4, A5;

        then

        reconsider p2 = n as Element of ( FTSL1 n);

        given j be Nat such that

         A8: j = (f . n) and

         A9: n <= j;

        (f . n) in the carrier of ( FTSL1 n) by A7, FUNCT_2: 5;

        then j <= n by A5, A8, FINSEQ_1: 1;

        then

         A10: n = j by A9, XXREAL_0: 1;

        p2 in ( U_FT p2) by A6;

        then

         A11: p2 in ( U_FT (p2, 0 )) by FINTOPO3: 47;

        ( U_FT (p2, 0 )) c= ( U_FT (p2,km)) by Th8, FINTOPO4: 18;

        hence contradiction by A3, A8, A10, A11;

      end;

      then

       A12: for j be Nat st n <= n & j = (f . n) holds n > j;

      then

       A13: ex k be Nat st P2[k];

      ex k be Nat st P2[k] & for m be Nat st P2[m] holds k <= m from NAT_1:sch 5( A13);

      then

      consider k be Nat such that

       A14: P2[k] and

       A15: for m be Nat st P2[m] holds k <= m;

      

       A16: ( 0 + 1) <= k by A14, NAT_1: 13;

      then

       A17: (k - 1) >= 0 by XREAL_1: 48;

      then

       A18: (k - 1) = (k -' 1) by XREAL_0:def 2;

      k < (k + 1) by NAT_1: 13;

      then

       A19: (k - 1) < ((k + 1) - 1) by XREAL_1: 9;

      

       A20: k <= n by A12, A15;

      then

      reconsider pk = k as Element of ( FTSL1 n) by A5, A16, FINSEQ_1: 1;

      per cases by A15, A18, A19;

        suppose

         A21: (k -' 1) <= 0 ;

        1 in the carrier of ( FTSL1 n) by A4, A5;

        then

         A22: (f . 1) in ( Seg n) by A5, FUNCT_2: 5;

        then

        reconsider j0 = (f . 1) as Nat;

        (k - 1) = 0 by A17, A21, XREAL_0:def 2;

        then 1 > j0 by A4, A14;

        hence contradiction by A22, FINSEQ_1: 1;

      end;

        suppose

         A23: (k -' 1) > 0 & ex j be Nat st (k -' 1) <= n & j = (f . (k -' 1)) & (k -' 1) <= j;

        

         A24: k in the carrier of ( FTSL1 n) by A5, A20, A16;

        then (f . k) in ( Seg n) by A5, FUNCT_2: 5;

        then

        reconsider jn = (f . k) as Nat;

        

         A25: not jn in ( U_FT (pk,km)) by A3;

        

         A26: jn < k by A14, A20;

        then

         A27: (k - jn) > 0 by XREAL_1: 50;

        jn in ( Seg n) by A5, A24, FUNCT_2: 5;

        then not |.(k - jn).| <= (km + 1) by A25, Th9;

        then

         A28: (k - jn) > (km + 1) by A27, ABSVALUE:def 1;

        (k - jn) = (k -' jn) by A27, XREAL_0:def 2;

        then

         A29: (k - jn) >= ((km + 1) + 1) by A28, NAT_1: 13;

        reconsider pfk = jn as Element of ( FTSL1 n) by A24, FUNCT_2: 5;

        

         A30: kc < (kc + 2) by XREAL_1: 29;

        

         A31: (k -' 1) >= ( 0 + 1) by A23, NAT_1: 13;

        then

         A32: (k -' 1) = ( max ((k -' 1),1)) by XXREAL_0:def 10;

        ( Im (( Nbdl1 n),k)) = {k, ( max ((k -' 1),1)), ( min ((k + 1),n))} by A5, A24, FINTOPO4:def 3;

        then (k -' 1) in ( U_FT pk) by A5, A32, ENUMSET1:def 1;

        then

         A33: (k -' 1) in ( U_FT (pk, 0 )) by FINTOPO3: 47;

        consider j be Nat such that

         A34: (k -' 1) <= n and

         A35: j = (f . (k -' 1)) and

         A36: (k -' 1) <= j by A23;

        reconsider pkm = (k -' 1) as Element of ( FTSL1 n) by A5, A34, A31, FINSEQ_1: 1;

        

         A37: not j in ( U_FT (pkm,km)) by A3, A35;

        

         A38: (k -' 1) in the carrier of ( FTSL1 n) by A5, A34, A31;

        then (k -' 1) in ( dom f) by FUNCT_2:def 1;

        then

         A39: (f . (k -' 1)) in (f .: ( U_FT (pk, 0 ))) by A33, FUNCT_1:def 6;

        now

          assume

           A40: (k -' 1) = j;

          then

          reconsider pj = j as Element of ( FTSL1 n) by A38;

          pj in ( U_FT pj) by A6;

          then

           A41: pj in ( U_FT (pj, 0 )) by FINTOPO3: 47;

          ( U_FT (pj, 0 )) c= ( U_FT (pj,km)) by Th8, FINTOPO4: 18;

          hence contradiction by A3, A35, A40, A41;

        end;

        then (k -' 1) < j by A36, XXREAL_0: 1;

        then

         A42: ((k -' 1) + 1) <= j by NAT_1: 13;

        then (j - k) >= 0 by A18, XREAL_1: 48;

        then

         A43: (j - k) = (j -' k) by XREAL_0:def 2;

        j in the carrier of ( FTSL1 n) by A35, A38, FUNCT_2: 5;

        then not |.((k -' 1) - j).| <= (km + 1) by A5, A37, Th9;

        then |.(j - (k -' 1)).| > (km + 1) by UNIFORM1: 11;

        then ((j -' k) + 1) > (km + 1) by A18, A43, ABSVALUE:def 1;

        then ((j - k) + 1) >= ((km + 1) + 1) by A43, NAT_1: 13;

        then ((k - jn) + ((j - k) + 1)) >= (((km + 1) + 1) + ((km + 1) + 1)) by A29, XREAL_1: 7;

        then ((j - jn) + 1) >= ((((km + 1) + 1) + (km + 1)) + 1);

        then (j - jn) >= (((km + 1) + 1) + (km + 1)) by XREAL_1: 6;

        then ((j - jn) - 1) >= (((((km + 1) + 1) + km) + 1) - 1) by XREAL_1: 9;

        then

         A44: (((j - jn) - 1) / 2) >= (((2 * km) + 2) / 2) by XREAL_1: 72;

         [/(kc / 2)\] >= (kc / 2) by INT_1:def 7;

        then ( [/(kc / 2)\] + (2 / 2)) >= ((kc / 2) + (2 / 2)) by XREAL_1: 7;

        then (((j - jn) - 1) / 2) >= ((kc / 2) + (2 / 2)) by A2, A44, XXREAL_0: 2;

        then ((((j - jn) - 1) / 2) * 2) >= (((kc / 2) + (2 / 2)) * 2) by XREAL_1: 64;

        then ((j - jn) - 1) > kc by A30, XXREAL_0: 2;

        then

         A45: (((j - jn) - 1) + 1) > (kc + 1) by XREAL_1: 6;

        jn < j by A18, A42, A26, XXREAL_0: 2;

        then (j - jn) >= 0 by XREAL_1: 48;

        then

         A46: |.(j - jn).| = (j - jn) by ABSVALUE:def 1;

        (f .: ( U_FT (pk, 0 ))) c= ( U_FT (pfk,kc)) & |.(jn - j).| = |.(j - jn).| by A1, FINTOPO4:def 2, UNIFORM1: 11;

        hence contradiction by A35, A39, A46, A45, Th9;

      end;

    end;

    definition

      let A,B be set;

      let R be Relation of A, B, x be set;

      :: original: Im

      redefine

      func Im (R,x) -> Subset of B ;

      coherence

      proof

        ( Im (R,x)) = (R .: {x});

        hence thesis;

      end;

    end

    definition

      let n,m be Nat;

      :: FINTOPO5:def2

      func Nbdl2 (n,m) -> Relation of [:( Seg n), ( Seg m):] means

      : Def2: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (it ,x)) = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):];

      existence

      proof

        defpred P[ object, object] means for i,j be Nat st $1 = [i, j] holds $2 = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):];

        

         A1: for x be object st x in [:( Seg n), ( Seg m):] holds ex y be object st y in ( bool [:( Seg n), ( Seg m):]) & P[x, y]

        proof

          let x be object;

          assume x in [:( Seg n), ( Seg m):];

          then

          consider u,y be object such that

           A2: u in ( Seg n) & y in ( Seg m) and

           A3: x = [u, y] by ZFMISC_1:def 2;

          reconsider i = u, j = y as Nat by A2;

          set y3 = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):];

          

           A4: y3 c= [:( Seg n), ( Seg m):]

          proof

            let z be object;

            assume z in y3;

            then ex x4,y4 be object st x4 in ( Im (( Nbdl1 n),i)) & y4 in ( Im (( Nbdl1 m),j)) & z = [x4, y4] by ZFMISC_1:def 2;

            hence thesis by ZFMISC_1:def 2;

          end;

          for i4,j4 be Nat st x = [i4, j4] holds y3 = [:( Im (( Nbdl1 n),i4)), ( Im (( Nbdl1 m),j4)):]

          proof

            let i4,j4 be Nat;

            assume

             A5: x = [i4, j4];

            then i4 = u by A3, XTUPLE_0: 1;

            hence thesis by A3, A5, XTUPLE_0: 1;

          end;

          hence thesis by A4;

        end;

        consider f be Function of [:( Seg n), ( Seg m):], ( bool [:( Seg n), ( Seg m):]) such that

         A6: for x be object st x in [:( Seg n), ( Seg m):] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        consider R be Relation of [:( Seg n), ( Seg m):] such that

         A7: for i be set st i in [:( Seg n), ( Seg m):] holds ( Im (R,i)) = (f . i) by FUNCT_2: 93;

        take R;

        let x be set such that

         A8: x in [:( Seg n), ( Seg m):];

        let i,j be Nat such that

         A9: x = [i, j];

        

        thus ( Im (R,x)) = (f . x) by A7, A8

        .= [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):] by A6, A8, A9;

      end;

      uniqueness

      proof

        let f1,f2 be Relation of [:( Seg n), ( Seg m):];

        assume that

         A10: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (f1,x)) = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):] and

         A11: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (f2,x)) = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):];

        for x be set st x in [:( Seg n), ( Seg m):] holds ( Im (f1,x)) = ( Im (f2,x))

        proof

          let x be set;

          assume

           A12: x in [:( Seg n), ( Seg m):];

          then

          consider u,y be object such that

           A13: u in ( Seg n) & y in ( Seg m) and

           A14: x = [u, y] by ZFMISC_1:def 2;

          reconsider i = u, j = y as Nat by A13;

          ( Im (f1,x)) = [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):] by A10, A12, A14;

          hence thesis by A11, A12, A14;

        end;

        hence f1 = f2 by RELSET_1: 31;

      end;

    end

    definition

      let n,m be Nat;

      :: FINTOPO5:def3

      func FTSL2 (n,m) -> strict RelStr equals RelStr (# [:( Seg n), ( Seg m):], ( Nbdl2 (n,m)) #);

      coherence ;

    end

    registration

      let n,m be non zero Nat;

      cluster ( FTSL2 (n,m)) -> non empty;

      coherence ;

    end

    theorem :: FINTOPO5:11

    for n,m be non zero Nat holds ( FTSL2 (n,m)) is filled

    proof

      let n,m be non zero Nat;

      for x be Element of ( FTSL2 (n,m)) holds x in ( U_FT x)

      proof

        let x be Element of ( FTSL2 (n,m));

        consider u,y be object such that

         A1: u in ( Seg n) and

         A2: y in ( Seg m) and

         A3: x = [u, y] by ZFMISC_1:def 2;

        reconsider i = u, j = y as Nat by A1, A2;

        

         A4: ( FTSL1 m) = RelStr (# ( Seg m), ( Nbdl1 m) #) by FINTOPO4:def 4;

        then

        reconsider pj = j as Element of ( FTSL1 m) by A2;

        

         A5: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

        then

        reconsider pi = i as Element of ( FTSL1 n) by A1;

        ( FTSL1 m) is filled by FINTOPO4: 18;

        then

         A6: j in ( U_FT pj);

        ( FTSL1 n) is filled by FINTOPO4: 18;

        then i in ( U_FT pi);

        then x in [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):] by A3, A4, A5, A6, ZFMISC_1:def 2;

        hence thesis by A3, Def2;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO5:12

    for n,m be non zero Nat holds ( FTSL2 (n,m)) is symmetric

    proof

      let n,m be non zero Nat;

      for x,y be Element of ( FTSL2 (n,m)) holds y in ( U_FT x) implies x in ( U_FT y)

      proof

        

         A1: ( FTSL1 m) is symmetric by FINTOPO4: 19;

        let x,y be Element of ( FTSL2 (n,m));

        consider xu,xv be object such that

         A2: xu in ( Seg n) and

         A3: xv in ( Seg m) and

         A4: x = [xu, xv] by ZFMISC_1:def 2;

        reconsider i = xu, j = xv as Nat by A2, A3;

        consider yu,yv be object such that

         A5: yu in ( Seg n) and

         A6: yv in ( Seg m) and

         A7: y = [yu, yv] by ZFMISC_1:def 2;

        reconsider i2 = yu, j2 = yv as Nat by A5, A6;

        

         A8: ( FTSL1 m) = RelStr (# ( Seg m), ( Nbdl1 m) #) by FINTOPO4:def 4;

        then

        reconsider pj = j as Element of ( FTSL1 m) by A3;

        reconsider pj2 = j2 as Element of ( FTSL1 m) by A8, A6;

        assume y in ( U_FT x);

        then y in [:( Im (( Nbdl1 n),i)), ( Im (( Nbdl1 m),j)):] by A4, Def2;

        then

         A9: ex y1,y2 be object st y1 in ( Class (( Nbdl1 n),i)) & y2 in ( Class (( Nbdl1 m),j)) & y = [y1, y2] by ZFMISC_1:def 2;

        then j2 in ( U_FT pj) by A8, A7, XTUPLE_0: 1;

        then

         A10: j in ( U_FT pj2) by A1;

        

         A11: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

        then

        reconsider pi = i as Element of ( FTSL1 n) by A2;

        

         A12: ( FTSL1 n) is symmetric by FINTOPO4: 19;

        reconsider pi2 = i2 as Element of ( FTSL1 n) by A11, A5;

        pi2 in ( U_FT pi) by A11, A7, A9, XTUPLE_0: 1;

        then pi in ( U_FT pi2) by A12;

        then x in [:( Im (( Nbdl1 n),i2)), ( Im (( Nbdl1 m),j2)):] by A4, A8, A11, A10, ZFMISC_1:def 2;

        hence thesis by A7, Def2;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO5:13

    for n be non zero Nat holds ex h be Function of ( FTSL2 (n,1)), ( FTSL1 n) st h is being_homeomorphism

    proof

      defpred P[ object, object] means [$2, 1] = $1;

      let n be non zero Nat;

      set FT1 = ( FTSL2 (n,1)), FT2 = ( FTSL1 n);

      

       A1: for x be object st x in the carrier of ( FTSL2 (n,1)) holds ex y be object st y in the carrier of ( FTSL1 n) & P[x, y]

      proof

        let x be object;

        

         A2: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

        assume x in the carrier of ( FTSL2 (n,1));

        then

        consider u,v be object such that

         A3: u in ( Seg n) and

         A4: v in ( Seg 1) and

         A5: x = [u, v] by ZFMISC_1:def 2;

        reconsider nu = u, nv = v as Nat by A3, A4;

        1 <= nv & nv <= 1 by A4, FINSEQ_1: 1;

        then P[x, nu] by A5, XXREAL_0: 1;

        hence thesis by A3, A2;

      end;

      ex f be Function of ( FTSL2 (n,1)), ( FTSL1 n) st for x be object st x in the carrier of ( FTSL2 (n,1)) holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

      then

      consider f be Function of ( FTSL2 (n,1)), ( FTSL1 n) such that

       A6: for x be object st x in the carrier of ( FTSL2 (n,1)) holds P[x, (f . x)];

      

       A7: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

      

       A8: the carrier of ( FTSL1 n) c= ( rng f)

      proof

        let x be object;

        set z = [x, 1];

        

         A9: 1 in ( Seg 1);

        assume x in the carrier of ( FTSL1 n);

        then

         A10: z in the carrier of ( FTSL2 (n,1)) by A7, A9, ZFMISC_1:def 2;

        then [(f . z), 1] = z by A6;

        then

         A11: (f . z) = x by XTUPLE_0: 1;

        z in ( dom f) by A10, FUNCT_2:def 1;

        hence thesis by A11, FUNCT_1:def 3;

      end;

      

       A12: for x be Element of FT1 holds (f .: ( U_FT x)) = ( Im (the InternalRel of FT2,(f . x)))

      proof

        let x be Element of FT1;

        consider u,v be object such that

         A13: u in ( Seg n) and

         A14: v in ( Seg 1) and

         A15: x = [u, v] by ZFMISC_1:def 2;

        

         A16: ( Im (the InternalRel of FT2,(f . x))) c= (f .: ( U_FT x))

        proof

          reconsider nv = v as Nat by A14;

          let y be object;

          assume

           A17: y in ( Im (the InternalRel of FT2,(f . x)));

          1 <= nv & nv <= 1 by A14, FINSEQ_1: 1;

          then

           A18: nv = 1 by XXREAL_0: 1;

          ( Im (( Nbdl1 n),(f . x))) c= ( rng f) by A7, A8;

          then

          consider x3 be object such that

           A19: x3 in ( dom f) and

           A20: y = (f . x3) by A7, A17, FUNCT_1:def 3;

          set u2 = (f . x3), v2 = 1;

          ( Im (( Nbdl1 1),v)) = {nv, ( max ((nv -' 1),1)), ( min ((nv + 1),1))} by A14, FINTOPO4:def 3

          .= {1, ( max ( 0 ,1)), ( min (2,1))} by A18, NAT_2: 8

          .= {1, 1, ( min (2,1))} by XXREAL_0:def 10

          .= {1, ( min (2,1))} by ENUMSET1: 30

          .= {1, 1} by XXREAL_0:def 9

          .= {1} by ENUMSET1: 29;

          then

           A21: v2 in ( Im (( Nbdl1 1),v)) by ZFMISC_1: 31;

          

           A22: ( Im (( Nbdl2 (n,1)),x)) = [:( Im (( Nbdl1 n),u)), ( Im (( Nbdl1 1),v)):] by A13, A14, A15, Def2;

          x = [(f . x), 1] by A6;

          then u2 in ( Im (( Nbdl1 n),u)) by A7, A15, A17, A20, XTUPLE_0: 1;

          then

           A23: [u2, v2] in [:( Im (( Nbdl1 n),u)), ( Im (( Nbdl1 1),v)):] by A21, ZFMISC_1:def 2;

          x3 = [(f . x3), 1] by A6, A19;

          hence thesis by A19, A20, A23, A22, FUNCT_1:def 6;

        end;

        (f .: ( U_FT x)) c= ( Im (the InternalRel of FT2,(f . x)))

        proof

          x = [(f . x), 1] by A6;

          then

           A24: u = (f . x) by A15, XTUPLE_0: 1;

          let y be object;

          assume y in (f .: ( U_FT x));

          then

          consider x2 be object such that

           A25: x2 in ( dom f) and

           A26: x2 in ( Im (( Nbdl2 (n,1)),x)) & y = (f . x2) by FUNCT_1:def 6;

          

           A27: ( Im (( Nbdl2 (n,1)),x)) = [:( Im (( Nbdl1 n),u)), ( Im (( Nbdl1 1),v)):] by A13, A14, A15, Def2;

          x2 = [(f . x2), 1] by A6, A25;

          hence thesis by A7, A26, A27, A24, ZFMISC_1: 87;

        end;

        hence thesis by A16, XBOOLE_0:def 10;

      end;

      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 that

         A28: x1 in ( dom f) and

         A29: x2 in ( dom f) & (f . x1) = (f . x2);

         [(f . x1), 1] = x1 by A6, A28;

        hence thesis by A6, A29;

      end;

      then

       A30: f is one-to-one by FUNCT_1:def 4;

      ( rng f) = the carrier of ( FTSL1 n) by A8, XBOOLE_0:def 10;

      then f is onto by FUNCT_2:def 3;

      then f is being_homeomorphism by A30, A12;

      hence thesis;

    end;

    definition

      let n,m be Nat;

      :: FINTOPO5:def4

      func Nbds2 (n,m) -> Relation of [:( Seg n), ( Seg m):] means

      : Def4: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (it ,x)) = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]);

      existence

      proof

        defpred P[ object, object] means for i,j be Nat st $1 = [i, j] holds $2 = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]);

        

         A1: for x be object st x in [:( Seg n), ( Seg m):] holds ex y be object st y in ( bool [:( Seg n), ( Seg m):]) & P[x, y]

        proof

          let x be object;

          assume x in [:( Seg n), ( Seg m):];

          then

          consider u,y be object such that

           A2: u in ( Seg n) and

           A3: y in ( Seg m) and

           A4: x = [u, y] by ZFMISC_1:def 2;

          reconsider i = u, j = y as Nat by A2, A3;

          set y3 = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),u)), {j}:]);

          

           A5: y3 c= [:( Seg n), ( Seg m):]

          proof

            let z be object;

            assume

             A6: z in y3;

            per cases by A6, XBOOLE_0:def 3;

              suppose z in [: {i}, ( Im (( Nbdl1 m),j)):];

              then

              consider x4,y4 be object such that

               A7: x4 in {i} and

               A8: y4 in ( Im (( Nbdl1 m),j)) & z = [x4, y4] by ZFMISC_1:def 2;

              x4 = i by A7, TARSKI:def 1;

              hence thesis by A2, A8, ZFMISC_1:def 2;

            end;

              suppose z in [:( Im (( Nbdl1 n),u)), {j}:];

              then

              consider x4,y4 be object such that

               A9: x4 in ( Im (( Nbdl1 n),i)) and

               A10: y4 in {j} and

               A11: z = [x4, y4] by ZFMISC_1:def 2;

              y4 in ( Seg m) by A3, A10, TARSKI:def 1;

              hence thesis by A9, A11, ZFMISC_1:def 2;

            end;

          end;

          for i4,j4 be Nat st x = [i4, j4] holds y3 = ( [: {i4}, ( Im (( Nbdl1 m),j4)):] \/ [:( Im (( Nbdl1 n),i4)), {j4}:])

          proof

            let i4,j4 be Nat;

            assume x = [i4, j4];

            then i4 = u & j4 = y by A4, XTUPLE_0: 1;

            hence thesis;

          end;

          hence thesis by A5;

        end;

        consider f be Function of [:( Seg n), ( Seg m):], ( bool [:( Seg n), ( Seg m):]) such that

         A12: for x be object st x in [:( Seg n), ( Seg m):] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        consider R be Relation of [:( Seg n), ( Seg m):] such that

         A13: for i be set st i in [:( Seg n), ( Seg m):] holds ( Im (R,i)) = (f . i) by FUNCT_2: 93;

        take R;

        let x be set such that

         A14: x in [:( Seg n), ( Seg m):];

        let i,j be Nat such that

         A15: x = [i, j];

        

        thus ( Im (R,x)) = (f . x) by A13, A14

        .= ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]) by A12, A14, A15;

      end;

      uniqueness

      proof

        let f1,f2 be Relation of [:( Seg n), ( Seg m):];

        assume that

         A16: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (f1,x)) = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]) and

         A17: for x be set st x in [:( Seg n), ( Seg m):] holds for i,j be Nat st x = [i, j] holds ( Im (f2,x)) = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]);

        for x be set st x in [:( Seg n), ( Seg m):] holds ( Im (f1,x)) = ( Im (f2,x))

        proof

          let x be set;

          assume

           A18: x in [:( Seg n), ( Seg m):];

          then

          consider u,y be object such that

           A19: u in ( Seg n) & y in ( Seg m) and

           A20: x = [u, y] by ZFMISC_1:def 2;

          reconsider i = u, j = y as Nat by A19;

          ( Im (f1,x)) = ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),u)), {j}:]) by A16, A18, A20;

          hence thesis by A17, A18, A20;

        end;

        hence f1 = f2 by RELSET_1: 31;

      end;

    end

    definition

      let n,m be Nat;

      :: FINTOPO5:def5

      func FTSS2 (n,m) -> strict RelStr equals RelStr (# [:( Seg n), ( Seg m):], ( Nbds2 (n,m)) #);

      coherence ;

    end

    registration

      let n,m be non zero Nat;

      cluster ( FTSS2 (n,m)) -> non empty;

      coherence ;

    end

    theorem :: FINTOPO5:14

    for n,m be non zero Nat holds ( FTSS2 (n,m)) is filled

    proof

      let n,m be non zero Nat;

      for x be Element of ( FTSS2 (n,m)) holds x in ( U_FT x)

      proof

        let x be Element of ( FTSS2 (n,m));

        consider u,y be object such that

         A1: u in ( Seg n) and

         A2: y in ( Seg m) and

         A3: x = [u, y] by ZFMISC_1:def 2;

        reconsider i = u, j = y as Nat by A1, A2;

        

         A4: ( FTSL1 m) = RelStr (# ( Seg m), ( Nbdl1 m) #) by FINTOPO4:def 4;

        then

        reconsider pj = j as Element of ( FTSL1 m) by A2;

        

         A5: i in {i} by ZFMISC_1: 31;

        ( FTSL1 m) is filled by FINTOPO4: 18;

        then j in ( U_FT pj);

        then x in [: {i}, ( Im (( Nbdl1 m),j)):] by A3, A4, A5, ZFMISC_1:def 2;

        then x in ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),u)), {j}:]) by XBOOLE_0:def 3;

        hence thesis by A3, Def4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO5:15

    for n,m be non zero Nat holds ( FTSS2 (n,m)) is symmetric

    proof

      let n,m be non zero Nat;

      for x,y be Element of ( FTSS2 (n,m)) holds y in ( U_FT x) implies x in ( U_FT y)

      proof

        let x,y be Element of ( FTSS2 (n,m));

        consider xu,xv be object such that

         A1: xu in ( Seg n) and

         A2: xv in ( Seg m) and

         A3: x = [xu, xv] by ZFMISC_1:def 2;

        reconsider i = xu, j = xv as Nat by A1, A2;

        consider yu,yv be object such that

         A4: yu in ( Seg n) and

         A5: yv in ( Seg m) and

         A6: y = [yu, yv] by ZFMISC_1:def 2;

        reconsider i2 = yu, j2 = yv as Nat by A4, A5;

        

         A7: ( FTSL1 m) = RelStr (# ( Seg m), ( Nbdl1 m) #) by FINTOPO4:def 4;

        then

        reconsider pj = j as Element of ( FTSL1 m) by A2;

        

         A8: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

        then

        reconsider pi = i as Element of ( FTSL1 n) by A1;

        reconsider pj2 = j2 as Element of ( FTSL1 m) by A7, A5;

        reconsider pi2 = i2 as Element of ( FTSL1 n) by A8, A4;

        assume y in ( U_FT x);

        then

         A9: y in ( [: {i}, ( Im (( Nbdl1 m),j)):] \/ [:( Im (( Nbdl1 n),i)), {j}:]) by A3, Def4;

        now

          per cases by A9, XBOOLE_0:def 3;

            case y in [: {i}, ( Im (( Nbdl1 m),j)):];

            then

            consider y1,y2 be object such that

             A10: y1 in {i} and

             A11: y2 in ( Class (( Nbdl1 m),j)) and

             A12: y = [y1, y2] by ZFMISC_1:def 2;

            y1 = i by A10, TARSKI:def 1;

            then

             A13: i in {i2} by A6, A10, A12, XTUPLE_0: 1;

            

             A14: ( FTSL1 m) is symmetric by FINTOPO4: 19;

            pj2 in ( U_FT pj) by A7, A6, A11, A12, XTUPLE_0: 1;

            then pj in ( U_FT pj2) by A14;

            hence x in [: {i2}, ( Im (( Nbdl1 m),j2)):] by A3, A7, A13, ZFMISC_1:def 2;

          end;

            case y in [:( Im (( Nbdl1 n),i)), {j}:];

            then

            consider y1,y2 be object such that

             A15: y1 in ( Class (( Nbdl1 n),i)) and

             A16: y2 in {j} and

             A17: y = [y1, y2] by ZFMISC_1:def 2;

            y2 = j by A16, TARSKI:def 1;

            then

             A18: j in {j2} by A6, A16, A17, XTUPLE_0: 1;

            

             A19: ( FTSL1 n) is symmetric by FINTOPO4: 19;

            pi2 in ( U_FT pi) by A8, A6, A15, A17, XTUPLE_0: 1;

            then pi in ( U_FT pi2) by A19;

            hence x in [:( Im (( Nbdl1 n),i2)), {j2}:] by A3, A8, A18, ZFMISC_1:def 2;

          end;

        end;

        then x in ( [: {i2}, ( Im (( Nbdl1 m),j2)):] \/ [:( Im (( Nbdl1 n),i2)), {j2}:]) by XBOOLE_0:def 3;

        hence thesis by A6, Def4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO5:16

    for n be non zero Nat holds ex h be Function of ( FTSS2 (n,1)), ( FTSL1 n) st h is being_homeomorphism

    proof

      defpred P[ object, object] means [$2, 1] = $1;

      let n be non zero Nat;

      set FT1 = ( FTSS2 (n,1)), FT2 = ( FTSL1 n);

      

       A1: for x be object st x in the carrier of ( FTSS2 (n,1)) holds ex y be object st y in the carrier of ( FTSL1 n) & P[x, y]

      proof

        let x be object;

        

         A2: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

        assume x in the carrier of ( FTSS2 (n,1));

        then

        consider u,v be object such that

         A3: u in ( Seg n) and

         A4: v in ( Seg 1) and

         A5: x = [u, v] by ZFMISC_1:def 2;

        reconsider nu = u, nv = v as Nat by A3, A4;

        1 <= nv & nv <= 1 by A4, FINSEQ_1: 1;

        then P[x, nu] by A5, XXREAL_0: 1;

        hence thesis by A3, A2;

      end;

      ex f be Function of ( FTSS2 (n,1)), ( FTSL1 n) st for x be object st x in the carrier of ( FTSS2 (n,1)) holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

      then

      consider f be Function of ( FTSS2 (n,1)), ( FTSL1 n) such that

       A6: for x be object st x in the carrier of ( FTSS2 (n,1)) holds P[x, (f . x)];

      

       A7: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by FINTOPO4:def 4;

      

       A8: the carrier of ( FTSL1 n) c= ( rng f)

      proof

        let x be object;

        set z = [x, 1];

        

         A9: 1 in ( Seg 1);

        assume x in the carrier of ( FTSL1 n);

        then

         A10: z in the carrier of ( FTSS2 (n,1)) by A7, A9, ZFMISC_1:def 2;

        then [(f . z), 1] = z by A6;

        then

         A11: (f . z) = x by XTUPLE_0: 1;

        z in ( dom f) by A10, FUNCT_2:def 1;

        hence thesis by A11, FUNCT_1:def 3;

      end;

      

       A12: for x be Element of FT1 holds (f .: ( U_FT x)) = ( Im (the InternalRel of FT2,(f . x)))

      proof

        let x be Element of FT1;

        consider u,v be object such that

         A13: u in ( Seg n) and

         A14: v in ( Seg 1) and

         A15: x = [u, v] by ZFMISC_1:def 2;

        

         A16: (f .: ( U_FT x)) c= ( Im (the InternalRel of FT2,(f . x)))

        proof

          let y be object;

          assume y in (f .: ( U_FT x));

          then

          consider x2 be object such that

           A17: x2 in ( dom f) and

           A18: x2 in ( Im (( Nbds2 (n,1)),x)) and

           A19: y = (f . x2) by FUNCT_1:def 6;

          consider u2,v2 be object such that u2 in ( Seg n) and v2 in ( Seg 1) and

           A20: x2 = [u2, v2] by A17, ZFMISC_1:def 2;

          x2 = [(f . x2), 1] by A6, A17;

          then

           A21: u2 = (f . x2) by A20, XTUPLE_0: 1;

          

           A22: ( Im (( Nbds2 (n,1)),x)) = ( [: {u}, ( Im (( Nbdl1 1),v)):] \/ [:( Im (( Nbdl1 n),u)), {v}:]) by A13, A14, A15, Def4;

           A23:

          now

            per cases by A18, A22, A20, XBOOLE_0:def 3;

              suppose

               A24: [u2, v2] in [: {u}, ( Im (( Nbdl1 1),v)):];

              reconsider pu = u as Element of ( FTSL1 n) by A7, A13;

              ( FTSL1 n) is filled by FINTOPO4: 18;

              then

               A25: u in ( U_FT pu);

              u2 in {u} by A24, ZFMISC_1: 87;

              hence u2 in ( Class (( Nbdl1 n),u)) by A7, A25, TARSKI:def 1;

            end;

              suppose [u2, v2] in [:( Im (( Nbdl1 n),u)), {v}:];

              hence u2 in ( Class (( Nbdl1 n),u)) by ZFMISC_1: 87;

            end;

          end;

          x = [(f . x), 1] by A6;

          hence thesis by A7, A15, A19, A21, A23, XTUPLE_0: 1;

        end;

        ( Im (the InternalRel of FT2,(f . x))) c= (f .: ( U_FT x))

        proof

          set X = ( Im (( Nbdl1 n),u)), Y = ( Im (( Nbdl1 1),v));

          reconsider nv = v as Nat by A14;

          let y be object;

          assume

           A26: y in ( Im (the InternalRel of FT2,(f . x)));

          ( Im (( Nbdl1 n),(f . x))) c= ( rng f) by A7, A8;

          then

          consider x3 be object such that

           A27: x3 in ( dom f) and

           A28: y = (f . x3) by A7, A26, FUNCT_1:def 3;

          set u2 = (f . x3), v2 = 1;

          x = [(f . x), 1] by A6;

          then

           A29: u2 in ( Im (( Nbdl1 n),u)) by A7, A15, A26, A28, XTUPLE_0: 1;

          

           A30: ( Im (( Nbds2 (n,1)),x)) = ( [: {u}, Y:] \/ [:X, {v}:]) by A13, A14, A15, Def4;

          1 <= nv & nv <= 1 by A14, FINSEQ_1: 1;

          then

           A31: nv = 1 by XXREAL_0: 1;

          

           A32: ( Im (( Nbdl1 1),v)) = {nv, ( max ((nv -' 1),1)), ( min ((nv + 1),1))} by A14, FINTOPO4:def 3

          .= {1, ( max ( 0 ,1)), ( min (2,1))} by A31, NAT_2: 8

          .= {1, 1, ( min (2,1))} by XXREAL_0:def 10

          .= {1, ( min (2,1))} by ENUMSET1: 30

          .= {1, 1} by XXREAL_0:def 9

          .= {1} by ENUMSET1: 29;

          then v2 in ( Im (( Nbdl1 1),v)) by ZFMISC_1: 31;

          then [u2, v2] in [:( Im (( Nbdl1 n),u)), ( Im (( Nbdl1 1),v)):] by A29, ZFMISC_1:def 2;

          then

           A33: [u2, v2] in ( [:X, {v}:] \/ [: {u}, Y:]) by A31, A32, XBOOLE_0:def 3;

          x3 = [(f . x3), 1] by A6, A27;

          hence thesis by A27, A28, A33, A30, FUNCT_1:def 6;

        end;

        hence thesis by A16, XBOOLE_0:def 10;

      end;

      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 that

         A34: x1 in ( dom f) and

         A35: x2 in ( dom f) & (f . x1) = (f . x2);

         [(f . x1), 1] = x1 by A6, A34;

        hence thesis by A6, A35;

      end;

      then

       A36: f is one-to-one by FUNCT_1:def 4;

      ( rng f) = the carrier of ( FTSL1 n) by A8, XBOOLE_0:def 10;

      then f is onto by FUNCT_2:def 3;

      then f is being_homeomorphism by A36, A12;

      hence thesis;

    end;