mfold_2.miz



    begin

    registration

      cluster {} -> {} -valued;

      correctness by FUNCTOR0: 1;

      cluster {} -> onto;

      correctness

      proof

        ( rng {} ) = {} ;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    theorem :: MFOLD_2:1

    

     Th1: for f be Function, Y be set holds ( dom (Y |` f)) = (f " Y)

    proof

      let f be Function;

      let Y be set;

      for x be object holds x in ( dom (Y |` f)) iff x in (f " Y)

      proof

        let x be object;

        hereby

          assume x in ( dom (Y |` f));

          then

          consider y be object such that

           A1: [x, y] in (Y |` f) by XTUPLE_0:def 12;

          y in Y & [x, y] in f by A1, RELAT_1:def 12;

          hence x in (f " Y) by RELAT_1:def 14;

        end;

        assume x in (f " Y);

        then

        consider y be object such that

         A2: [x, y] in f & y in Y by RELAT_1:def 14;

         [x, y] in (Y |` f) by A2, RELAT_1:def 12;

        hence x in ( dom (Y |` f)) by XTUPLE_0:def 12;

      end;

      hence ( dom (Y |` f)) = (f " Y) by TARSKI: 2;

    end;

    theorem :: MFOLD_2:2

    

     Th2: for f be Function, Y1,Y2 be set st Y2 c= Y1 holds ((Y1 |` f) " Y2) = (f " Y2)

    proof

      let f be Function;

      let Y1,Y2 be set;

      assume

       A1: Y2 c= Y1;

      for x be object holds x in ((Y1 |` f) " Y2) iff x in (f " Y2)

      proof

        let x be object;

        hereby

          assume x in ((Y1 |` f) " Y2);

          then

          consider y be object such that

           A2: [x, y] in (Y1 |` f) & y in Y2 by RELAT_1:def 14;

           [x, y] in f by A2, RELAT_1:def 12;

          hence x in (f " Y2) by A2, RELAT_1:def 14;

        end;

        assume x in (f " Y2);

        then

        consider y be object such that

         A3: [x, y] in f & y in Y2 by RELAT_1:def 14;

         [x, y] in (Y1 |` f) by A3, A1, RELAT_1:def 12;

        hence x in ((Y1 |` f) " Y2) by A3, RELAT_1:def 14;

      end;

      hence ((Y1 |` f) " Y2) = (f " Y2) by TARSKI: 2;

    end;

    theorem :: MFOLD_2:3

    

     Th3: for S,T be TopStruct, f be Function of S, T holds f is being_homeomorphism implies (f " ) is being_homeomorphism

    proof

      let S,T be TopStruct;

      let f be Function of S, T;

      assume

       A1: f is being_homeomorphism;

      then

       A2: ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one & f is continuous & (f " ) is continuous by TOPS_2:def 5;

      per cases ;

        suppose S is non empty & T is non empty;

        hence (f " ) is being_homeomorphism by A1, TOPS_2: 56;

      end;

        suppose

         A3: S is empty or T is empty;

        

         A4: f = {}

        proof

          per cases by A3;

            suppose S is empty;

            hence thesis;

          end;

            suppose T is empty;

            hence thesis;

          end;

        end;

        reconsider g = f as onto one-to-one PartFunc of {} , {} by A4, FUNCTOR0: 1;

        

         A5: (f " ) = (g " ) by A2;

        

         A6: ( dom (f " )) = ( [#] T) & ( rng (f " )) = ( [#] S) by A2, A4;

        reconsider g1 = (f " ) as onto one-to-one PartFunc of {} , {} by A5;

        ((f " ) " ) = (g1 " ) by A2, A4;

        hence thesis by A4, A6, A2, TOPS_2:def 5;

      end;

    end;

    definition

      let S,T be TopStruct;

      :: original: are_homeomorphic

      redefine

      pred S,T are_homeomorphic ;

      symmetry

      proof

        let S,T be TopStruct;

        assume (S,T) are_homeomorphic ;

        then

        consider f be Function of S, T such that

         A1: f is being_homeomorphism by T_0TOPSP:def 1;

        (f " ) is being_homeomorphism by A1, Th3;

        hence thesis by T_0TOPSP:def 1;

      end;

    end

    reserve T1,T2,T3 for TopSpace,

A1 for Subset of T1,

A2 for Subset of T2,

A3 for Subset of T3;

    theorem :: MFOLD_2:4

    

     Th4: for f be Function of T1, T2 st f is being_homeomorphism holds for g be Function of (T1 | (f " A2)), (T2 | A2) st g = (A2 |` f) holds g is being_homeomorphism

    proof

      let f be Function of T1, T2 such that

       A1: f is being_homeomorphism;

      

       A2: ( dom f) = ( [#] T1) & ( rng f) = ( [#] T2) by A1, TOPS_2:def 5;

      (T1,T2) are_homeomorphic by A1, T_0TOPSP:def 1;

      then T1 is empty iff T2 is empty by YELLOW14: 18;

      then

       A3: ( [#] T1) = {} iff ( [#] T2) = {} ;

      

       A4: ( rng f) = ( [#] T2) by A1, TOPS_2:def 5;

      set A = (f " A2);

      let g be Function of (T1 | A), (T2 | A2) such that

       A5: g = (A2 |` f);

      

       A6: ( rng g) = A2 by A2, A5, RELAT_1: 89;

      

       A7: f is one-to-one by A1, TOPS_2:def 5;

      then

       A8: g is one-to-one by A5, FUNCT_1: 58;

      set TA = (T1 | A), TB = (T2 | A2);

      

       A10: ( [#] TA) = A by PRE_TOPC:def 5;

      

       A11: ( [#] TA) = {} iff ( [#] TB) = {} by A6;

      

       A12: ( [#] TB) = A2 by PRE_TOPC:def 5;

      

       A13: f is continuous by A1, TOPS_2:def 5;

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

      proof

        let P be Subset of TB;

        assume P is open;

        then

        consider P1 be Subset of T2 such that

         A14: P1 is open and

         A15: P = (P1 /\ A2) by A12, TSP_1:def 1;

        

         A16: (f " P1) is open by A3, A13, A14, TOPS_2: 43;

        (g " P) = (f " P) by A5, Th2, A15, XBOOLE_1: 17

        .= ((f " P1) /\ the carrier of TA) by A10, A15, FUNCT_1: 68;

        hence thesis by A16, TSP_1:def 1;

      end;

      then

       A17: g is continuous by A11, TOPS_2: 43;

      

       A18: (f " ) is continuous by A1, TOPS_2:def 5;

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

      proof

        let P be Subset of TA;

        assume P is open;

        then

        consider P1 be Subset of T1 such that

         A19: P1 is open and

         A20: P = (P1 /\ A) by A10, TSP_1:def 1;

        

         A21: ((f " ) " P1) is open by A3, A18, A19, TOPS_2: 43;

        A2 = (f .: (f " A2)) by A2, FUNCT_1: 77;

        then

         A22: the carrier of TB = ((f " ) " A) by A12, A4, A7, TOPS_2: 54;

        ((g " ) " P) = ((A2 |` f) .: P) by A5, A6, A8, A12, TOPS_2: 54

        .= ((f .: P) /\ the carrier of TB) by A12, FUNCT_1: 67

        .= (((f " ) " (P1 /\ A)) /\ the carrier of TB) by A4, A7, A20, TOPS_2: 54

        .= ((((f " ) " P1) /\ ((f " ) " A)) /\ the carrier of TB) by FUNCT_1: 68

        .= (((f " ) " P1) /\ (((f " ) " A) /\ the carrier of TB)) by XBOOLE_1: 16

        .= (((f " ) " P1) /\ the carrier of TB) by A22;

        hence thesis by A21, TSP_1:def 1;

      end;

      then (g " ) is continuous by A11, TOPS_2: 43;

      hence thesis by A6, A5, Th1, A10, A8, A12, A17, TOPS_2:def 5;

    end;

    theorem :: MFOLD_2:5

    for f be Function of T1, T2 st f is being_homeomorphism holds ((f " A2),A2) are_homeomorphic

    proof

      let f be Function of T1, T2 such that

       A1: f is being_homeomorphism;

      

       A2: ( dom (A2 |` f)) = (f " A2) by Th1

      .= ( [#] (T1 | (f " A2))) by PRE_TOPC:def 5;

      ( rng f) = ( [#] T2) by A1, TOPS_2:def 5;

      

      then ( rng (A2 |` f)) = A2 by RELAT_1: 89

      .= ( [#] (T2 | A2)) by PRE_TOPC:def 5;

      then

      reconsider g = (A2 |` f) as Function of (T1 | (f " A2)), (T2 | A2) by A2, FUNCT_2: 1;

      g is being_homeomorphism by A1, Th4;

      hence thesis by T_0TOPSP:def 1, METRIZTS:def 1;

    end;

    theorem :: MFOLD_2:6

    (A1,A2) are_homeomorphic implies (A2,A1) are_homeomorphic

    proof

      assume (A1,A2) are_homeomorphic ;

      then ((T1 | A1),(T2 | A2)) are_homeomorphic by METRIZTS:def 1;

      hence (A2,A1) are_homeomorphic by METRIZTS:def 1;

    end;

    theorem :: MFOLD_2:7

    

     Th7: (A1,A2) are_homeomorphic implies (A1 is empty iff A2 is empty)

    proof

      assume (A1,A2) are_homeomorphic ;

      then

      consider f be Function of (T1 | A1), (T2 | A2) such that

       A1: f is being_homeomorphism by METRIZTS:def 1, T_0TOPSP:def 1;

      ( dom f) = ( [#] (T1 | A1)) & ( rng f) = ( [#] (T2 | A2)) & f is one-to-one & f is continuous & (f " ) is continuous by A1, TOPS_2:def 5;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: MFOLD_2:8

    (A1,A2) are_homeomorphic & (A2,A3) are_homeomorphic implies (A1,A3) are_homeomorphic

    proof

      assume

       A1: (A1,A2) are_homeomorphic ;

      then

       A2: ((T1 | A1),(T2 | A2)) are_homeomorphic by METRIZTS:def 1;

      assume

       A3: (A2,A3) are_homeomorphic ;

      then

       A4: ((T2 | A2),(T3 | A3)) are_homeomorphic by METRIZTS:def 1;

      per cases ;

        suppose

         A5: A2 is non empty;

        then

         A6: A1 is non empty & A3 is non empty by A1, A3, Th7;

        T1 is non empty & T2 is non empty & T3 is non empty by A5, A1, A3, Th7;

        hence (A1,A3) are_homeomorphic by A2, A4, A6, A5, BORSUK_3: 3, METRIZTS:def 1;

      end;

        suppose A2 is empty;

        then

         A7: A1 is empty & A3 is empty by A1, A3, Th7;

        reconsider f = {} as Function;

        

         A8: the carrier of (T1 | A1) = {} & the carrier of (T3 | A3) = {} by A7;

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

        then

        reconsider f as Function of (T1 | A1), (T3 | A3) by A8, FUNCT_2: 1;

        

         A9: ( dom f) = ( [#] (T1 | A1)) & ( rng f) = ( [#] (T3 | A3)) by A8;

        for P1 be Subset of (T3 | A3) st P1 is closed holds (f " P1) is closed;

        then

         A10: f is continuous by PRE_TOPC:def 6;

        reconsider g = f as onto one-to-one PartFunc of {} , {} by FUNCTOR0: 1;

        for P1 be Subset of (T1 | A1) st P1 is closed holds ((f " ) " P1) is closed by A7;

        then (f " ) is continuous by PRE_TOPC:def 6;

        then f is being_homeomorphism by A9, A10, TOPS_2:def 5;

        hence thesis by METRIZTS:def 1, T_0TOPSP:def 1;

      end;

    end;

    theorem :: MFOLD_2:9

    

     Th9: T1 is second-countable & (T1,T2) are_homeomorphic implies T2 is second-countable

    proof

      assume T1 is second-countable;

      then

       A1: ( weight T1) c= omega by WAYBEL23:def 6;

      assume (T1,T2) are_homeomorphic ;

      then ( weight T1) = ( weight T2) by METRIZTS: 4;

      hence T2 is second-countable by A1, WAYBEL23:def 6;

    end;

    reserve n,k for Nat;

    reserve M,N for non empty TopSpace;

    theorem :: MFOLD_2:10

    

     Th10: M is Hausdorff & (M,N) are_homeomorphic implies N is Hausdorff

    proof

      assume

       A1: M is Hausdorff;

      assume (M,N) are_homeomorphic ;

      then

      consider f be Function of N, M such that

       A2: f is being_homeomorphism by T_0TOPSP:def 1;

      

       A3: ( dom f) = ( [#] N) & ( rng f) = ( [#] M) & f is one-to-one & f is continuous & (f " ) is continuous by A2, TOPS_2:def 5;

      for p,q be Point of N st p <> q holds ex N1,N2 be Subset of N st N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2

      proof

        let p,q be Point of N;

        assume p <> q;

        then

        consider M1,M2 be Subset of M such that

         A4: M1 is open & M2 is open & (f . p) in M1 & (f . q) in M2 & M1 misses M2 by A1, A3, PRE_TOPC:def 10;

        reconsider N1 = (f " M1) as Subset of N;

        reconsider N2 = (f " M2) as Subset of N;

        take N1, N2;

        thus N1 is open & N2 is open by A4, A3, TOPS_2: 43;

        thus p in N1 & q in N2 by A4, FUNCT_2: 38;

        thus N1 misses N2 by A4, FUNCT_1: 71;

      end;

      hence N is Hausdorff by PRE_TOPC:def 10;

    end;

    ::$Canceled

    theorem :: MFOLD_2:12

    

     Th12: M is n -manifold & (M,N) are_homeomorphic implies N is n -manifold

    proof

      assume

       A1: M is n -manifold;

      assume

       A2: (M,N) are_homeomorphic ;

      then

       A3: N is second-countable by A1, Th9;

      

       A4: N is Hausdorff by A1, A2, Th10;

      N is n -locally_euclidean by A1, A2, MFOLD_0: 10, MFOLD_0: 11;

      hence N is n -manifold by A3, A4;

    end;

    theorem :: MFOLD_2:13

    

     Th13: for x1,x2 be FinSequence of REAL , i be Element of NAT st i in ( dom ( mlt (x1,x2))) holds (( mlt (x1,x2)) . i) = ((x1 /. i) * (x2 /. i)) & (( mlt (x1,x2)) /. i) = ((x1 /. i) * (x2 /. i))

    proof

      let x1,x2 be FinSequence of REAL , i be Element of NAT ;

      assume

       A1: i in ( dom ( mlt (x1,x2)));

      

       A2: ( mlt (x1,x2)) = ( multreal .: (x1,x2)) by RVSUM_1:def 9;

      ( dom multreal ) = [: REAL , REAL :] & ( rng x1) c= REAL by FUNCT_2:def 1;

      then [:( rng x1), ( rng x2):] c= ( dom multreal ) by ZFMISC_1: 96;

      then

       A3: ( dom ( mlt (x1,x2))) = (( dom x1) /\ ( dom x2)) by A2, FUNCOP_1: 69;

      then i in ( dom x2) by A1, XBOOLE_0:def 4;

      then

       A4: (x2 /. i) = (x2 . i) by PARTFUN1:def 6;

      i in ( dom x1) by A1, A3, XBOOLE_0:def 4;

      then (x1 /. i) = (x1 . i) by PARTFUN1:def 6;

      hence (( mlt (x1,x2)) . i) = ((x1 /. i) * (x2 /. i)) by A4, RVSUM_1: 59;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: MFOLD_2:14

    

     Th14: for x1,x2,y1,y2 be FinSequence of REAL st ( len x1) = ( len x2) & ( len y1) = ( len y2) holds ( mlt ((x1 ^ y1),(x2 ^ y2))) = (( mlt (x1,x2)) ^ ( mlt (y1,y2)))

    proof

      let x1,x2,y1,y2 be FinSequence of REAL ;

      assume that

       A1: ( len x1) = ( len x2) and

       A2: ( len y1) = ( len y2);

      

       A3: ( multreal .: ((x1 ^ y1),(x2 ^ y2))) = ( multreal * <:(x1 ^ y1), (x2 ^ y2):>) by FUNCOP_1:def 3;

      

       A4: ( dom (x1 ^ y1)) = ( Seg ( len (x1 ^ y1))) by FINSEQ_1:def 3;

      ( dom multreal ) = [: REAL , REAL :] & ( rng (x1 ^ y1)) c= REAL by FUNCT_2:def 1;

      then [:( rng (x1 ^ y1)), ( rng (x2 ^ y2)):] c= ( dom multreal ) by ZFMISC_1: 96;

      then

       A5: ( dom ( multreal * <:(x1 ^ y1), (x2 ^ y2):>)) = (( dom (x1 ^ y1)) /\ ( dom (x2 ^ y2))) by A3, FUNCOP_1: 69;

      

       A6: ( len (x2 ^ y2)) = (( len x2) + ( len y2)) by FINSEQ_1: 22;

      then ( dom (x1 ^ y1)) = ( dom (x2 ^ y2)) by A1, A2, A4, FINSEQ_1: 22, FINSEQ_1:def 3;

      then

       A7: ( dom ( mlt ((x1 ^ y1),(x2 ^ y2)))) = ( dom (x1 ^ y1)) by A3, A5, RVSUM_1:def 9;

      

       A8: ( multreal .: (y1,y2)) = ( multreal * <:y1, y2:>) by FUNCOP_1:def 3;

      

       A9: ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

      then [:( rng y1), ( rng y2):] c= ( dom multreal ) by ZFMISC_1: 96;

      then

       A10: ( dom ( multreal * <:y1, y2:>)) = (( dom y1) /\ ( dom y2)) by A8, FUNCOP_1: 69;

      ( dom y2) = ( Seg ( len y1)) by A2, FINSEQ_1:def 3

      .= ( dom y1) by FINSEQ_1:def 3;

      then

       A11: ( dom ( mlt (y1,y2))) = ( dom y1) by A8, A10, RVSUM_1:def 9;

      then ( dom ( mlt (y1,y2))) = ( Seg ( len y1)) by FINSEQ_1:def 3;

      then

       A12: ( len ( mlt (y1,y2))) = ( len y1) by FINSEQ_1:def 3;

      

       A13: ( multreal .: (x1,x2)) = ( multreal * <:x1, x2:>) by FUNCOP_1:def 3;

       [:( rng x1), ( rng x2):] c= ( dom multreal ) by A9, ZFMISC_1: 96;

      then

       A14: ( dom ( multreal * <:x1, x2:>)) = (( dom x1) /\ ( dom x2)) by A13, FUNCOP_1: 69;

      

       A15: ( len (x1 ^ y1)) = (( len x1) + ( len y1)) by FINSEQ_1: 22;

      ( dom x2) = ( Seg ( len x1)) by A1, FINSEQ_1:def 3

      .= ( dom x1) by FINSEQ_1:def 3;

      then

       A16: ( dom ( mlt (x1,x2))) = ( dom x1) by A13, A14, RVSUM_1:def 9;

      then

       A17: ( dom ( mlt (x1,x2))) = ( Seg ( len x1)) by FINSEQ_1:def 3;

      

       A18: for i be Nat st 1 <= i & i <= ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) holds (( mlt ((x1 ^ y1),(x2 ^ y2))) . i) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i)

      proof

        let i be Nat;

        assume that

         A19: 1 <= i and

         A20: i <= ( len ( mlt ((x1 ^ y1),(x2 ^ y2))));

        i in ( Seg ( len ( mlt ((x1 ^ y1),(x2 ^ y2))))) by A19, A20;

        then

         A21: i in ( dom ( mlt ((x1 ^ y1),(x2 ^ y2)))) by FINSEQ_1:def 3;

        then i <= ( len (x1 ^ y1)) by A4, A7, FINSEQ_1: 1;

        then

         A22: ((x1 ^ y1) /. i) = ((x1 ^ y1) . i) by A19, FINSEQ_4: 15;

        i <= ( len (x2 ^ y2)) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1: 1;

        then

         A23: ((x2 ^ y2) /. i) = ((x2 ^ y2) . i) by A19, FINSEQ_4: 15;

        

         A24: i <= (( len x1) + ( len y1)) by A15, A4, A7, A21, FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A25: i <= ( len x1);

            then

             A26: i in ( Seg ( len x1)) by A19;

            then

             A27: i in ( dom x1) by FINSEQ_1:def 3;

            i in ( dom x2) by A1, A26, FINSEQ_1:def 3;

            then

             A28: ((x2 ^ y2) . i) = (x2 . i) by FINSEQ_1:def 7;

            

             A29: i in ( dom ( mlt (x1,x2))) by A16, A26, FINSEQ_1:def 3;

            

            then

             A30: ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) = (( mlt (x1,x2)) . i) by FINSEQ_1:def 7

            .= ((x1 /. i) * (x2 /. i)) by A29, Th13;

            (x1 /. i) = (x1 . i) & (x2 /. i) = (x2 . i) by A1, A19, A25, FINSEQ_4: 15;

            hence (((x1 ^ y1) /. i) * ((x2 ^ y2) /. i)) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) by A22, A23, A27, A28, A30, FINSEQ_1:def 7;

          end;

            suppose

             A31: i > ( len x1);

            i <= ( len (x2 ^ y2)) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1: 1;

            then

             A32: ((x2 ^ y2) /. i) = ((x2 ^ y2) . i) by A19, FINSEQ_4: 15;

            i <= ( len (x1 ^ y1)) by A4, A7, A21, FINSEQ_1: 1;

            then

             A33: ((x1 ^ y1) /. i) = ((x1 ^ y1) . i) by A19, FINSEQ_4: 15;

            set k = (i -' ( len x1));

            

             A34: k = (i - ( len x1)) by A31, XREAL_1: 233;

            then

             A35: i = (( len x1) + k);

            (i - ( len x1)) <= ((( len x1) + ( len y1)) - ( len x1)) by A24, XREAL_1: 13;

            then

             A36: k <= ( len y1) by A31, XREAL_1: 233;

            k > 0 by A31, A34, XREAL_1: 50;

            then (k + 1) > ( 0 + 1) by XREAL_1: 6;

            then

             A37: 1 <= k by NAT_1: 13;

            then

             A38: k in ( Seg ( len y1)) by A36;

            then

             A39: k in ( dom ( mlt (y1,y2))) by A11, FINSEQ_1:def 3;

            i = (( len ( mlt (x1,x2))) + k) by A17, A35, FINSEQ_1:def 3;

            

            then

             A40: ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) = (( mlt (y1,y2)) . k) by A39, FINSEQ_1:def 7

            .= ((y1 /. k) * (y2 /. k)) by A39, Th13;

            k in ( dom y1) by A38, FINSEQ_1:def 3;

            then

             A41: ((x1 ^ y1) . i) = (y1 . k) by A35, FINSEQ_1:def 7;

            k in ( Seg ( len y1)) by A37, A36;

            then

             A42: k in ( dom y2) by A2, FINSEQ_1:def 3;

            (y1 /. k) = (y1 . k) & (y2 /. k) = (y2 . k) by A2, A37, A36, FINSEQ_4: 15;

            hence (((x1 ^ y1) /. i) * ((x2 ^ y2) /. i)) = ((( mlt (x1,x2)) ^ ( mlt (y1,y2))) . i) by A1, A35, A42, A41, A33, A32, A40, FINSEQ_1:def 7;

          end;

        end;

        hence thesis by A21, Th13;

      end;

      ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) = ( len (x1 ^ y1)) by A4, A7, FINSEQ_1:def 3

      .= (( len x1) + ( len y1)) by FINSEQ_1: 22;

      then ( len ( mlt ((x1 ^ y1),(x2 ^ y2)))) = (( len ( mlt (x1,x2))) + ( len ( mlt (y1,y2)))) by A17, A12, FINSEQ_1:def 3;

      hence thesis by A18, FINSEQ_1: 22;

    end;

    theorem :: MFOLD_2:15

    

     Th15: for x1,x2,y1,y2 be FinSequence of REAL st ( len x1) = ( len x2) & ( len y1) = ( len y2) holds |((x1 ^ y1), (x2 ^ y2))| = ( |(x1, x2)| + |(y1, y2)|)

    proof

      let x1,x2,y1,y2 be FinSequence of REAL ;

      

       A1: ( Sum (( mlt (x1,x2)) ^ ( mlt (y1,y2)))) = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by RVSUM_1: 75;

      assume ( len x1) = ( len x2) & ( len y1) = ( len y2);

      then ( Sum ( mlt ((x1 ^ y1),(x2 ^ y2)))) = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by A1, Th14;

      then |((x1 ^ y1), (x2 ^ y2))| = (( Sum ( mlt (x1,x2))) + ( Sum ( mlt (y1,y2)))) by RVSUM_1:def 16;

      then |((x1 ^ y1), (x2 ^ y2))| = (( Sum ( mlt (x1,x2))) + |(y1, y2)|) by RVSUM_1:def 16;

      hence thesis by RVSUM_1:def 16;

    end;

    

     Lm1: the carrier of ( RealVectSpace ( Seg n)) = the carrier of ( TOP-REAL n)

    proof

      reconsider D = REAL as non empty set;

      

       A1: ( Funcs (( Seg n),D)) = ( REAL n) by FINSEQ_2: 93;

      ( RealVectSpace ( Seg n)) = RLSStruct (# ( Funcs (( Seg n), REAL )), ( RealFuncZero ( Seg n)), ( RealFuncAdd ( Seg n)), ( RealFuncExtMult ( Seg n)) #) by FUNCSDOM:def 6;

      hence thesis by A1, EUCLID: 22;

    end;

    

     Lm2: ( 0. ( RealVectSpace ( Seg n))) = ( 0. ( TOP-REAL n))

    proof

      ( RealVectSpace ( Seg n)) = RLSStruct (# ( Funcs (( Seg n), REAL )), ( RealFuncZero ( Seg n)), ( RealFuncAdd ( Seg n)), ( RealFuncExtMult ( Seg n)) #) by FUNCSDOM:def 6;

      

      hence ( 0. ( RealVectSpace ( Seg n))) = (( Seg n) --> 0 ) by FUNCSDOM:def 4

      .= ( 0* n) by FINSEQ_2:def 2

      .= ( 0. ( TOP-REAL n)) by EUCLID: 70;

    end;

    reserve p,q,p1,p2 for Point of ( TOP-REAL n);

    reserve r for Real;

    theorem :: MFOLD_2:16

    

     Th16: k in ( Seg n) implies ((p1 + p2) . k) = ((p1 . k) + (p2 . k))

    proof

      

       A1: ( dom (p1 + p2)) = ( Seg n) by FINSEQ_1: 89;

      thus thesis by A1, VALUED_1:def 1;

    end;

    theorem :: MFOLD_2:17

    

     Th17: for X be set holds X is Linear_Combination of ( RealVectSpace ( Seg n)) iff X is Linear_Combination of ( TOP-REAL n)

    proof

      let X be set;

      set V = ( RealVectSpace ( Seg n));

      set T = ( TOP-REAL n);

      hereby

        assume X is Linear_Combination of V;

        then

        reconsider L = X as Linear_Combination of V;

        consider S be finite Subset of V such that

         A1: for v be Element of V st not v in S holds (L . v) = 0 by RLVECT_2:def 3;

         A2:

        now

          let v be Element of T;

          assume

           A3: not v in S;

          v is Element of V by Lm1;

          hence 0 = (L . v) by A1, A3;

        end;

        (L is Element of ( Funcs (the carrier of T, REAL ))) & S is finite Subset of T by Lm1;

        hence X is Linear_Combination of T by A2, RLVECT_2:def 3;

      end;

      assume X is Linear_Combination of T;

      then

      reconsider L = X as Linear_Combination of T;

      consider S be finite Subset of T such that

       A4: for v be Element of T st not v in S holds (L . v) = 0 by RLVECT_2:def 3;

       A5:

      now

        let v be Element of V;

        assume

         A6: not v in S;

        v is Element of T by Lm1;

        hence 0 = (L . v) by A4, A6;

      end;

      L is Element of ( Funcs (the carrier of V, REAL )) & S is finite Subset of V by Lm1;

      hence thesis by A5, RLVECT_2:def 3;

    end;

    theorem :: MFOLD_2:18

    

     Th18: for F be FinSequence of ( TOP-REAL n), fr be Function of ( TOP-REAL n), REAL , Fv be FinSequence of ( RealVectSpace ( Seg n)), fv be Function of ( RealVectSpace ( Seg n)), REAL st fr = fv & F = Fv holds (fr (#) F) = (fv (#) Fv)

    proof

      let F be FinSequence of ( TOP-REAL n), fr be Function of ( TOP-REAL n), REAL , Fv be FinSequence of ( RealVectSpace ( Seg n)), fv be Function of ( RealVectSpace ( Seg n)), REAL ;

      assume that

       A1: fr = fv and

       A2: F = Fv;

      

       A3: ( len (fv (#) Fv)) = ( len Fv) by RLVECT_2:def 7;

      

       A4: ( len (fr (#) F)) = ( len F) by RLVECT_2:def 7;

      now

        reconsider T = ( TOP-REAL n) as RealLinearSpace;

        let i be Nat;

        reconsider Fi = (F /. i) as FinSequence of REAL by EUCLID: 24;

        

         A5: the carrier of (n -VectSp_over F_Real ) = the carrier of ( TOP-REAL n)

        proof

          

          thus the carrier of (n -VectSp_over F_Real ) = ( REAL n) by MATRIX13: 102

          .= the carrier of ( TOP-REAL n) by EUCLID: 22;

        end;

        the carrier of (n -VectSp_over F_Real ) = (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

        then

        reconsider Fvi = (Fv /. i) as Element of (n -tuples_on the carrier of F_Real ) by Lm1, A5;

        reconsider Fii = (F /. i) as Element of T;

        assume

         A6: 1 <= i & i <= ( len F);

        then

         A7: i in ( dom (fv (#) Fv)) by A2, A3, FINSEQ_3: 25;

        i in ( dom F) by A6, FINSEQ_3: 25;

        then

         A8: (F /. i) = (F . i) by PARTFUN1:def 6;

        

         A9: (Fv /. i) = (Fv . i) by A2, A6, FINSEQ_3: 25, PARTFUN1:def 6;

        i in ( dom (fr (#) F)) by A4, A6, FINSEQ_3: 25;

        

        hence ((fr (#) F) . i) = ((fr . Fii) * Fii) by RLVECT_2:def 7

        .= ((fv . (Fv /. i)) * (Fv /. i)) by A1, A2, A8, A9, EUCLID: 65

        .= ((fv (#) Fv) . i) by A7, RLVECT_2:def 7;

      end;

      hence thesis by A2, A4, RLVECT_2:def 7;

    end;

    theorem :: MFOLD_2:19

    

     Th19: for F be FinSequence of ( TOP-REAL n), Fv be FinSequence of ( RealVectSpace ( Seg n)) st Fv = F holds ( Sum F) = ( Sum Fv)

    proof

      set T = ( TOP-REAL n);

      set V = ( RealVectSpace ( Seg n));

      let F be FinSequence of T;

      let Fv be FinSequence of V such that

       A1: Fv = F;

      reconsider T = ( TOP-REAL n) as RealLinearSpace;

      consider f be sequence of the carrier of T such that

       A2: ( Sum F) = (f . ( len F)) and

       A3: (f . 0 ) = ( 0. T) and

       A4: for j be Nat, v be Element of T st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      consider fv be sequence of the carrier of V such that

       A5: ( Sum Fv) = (fv . ( len Fv)) and

       A6: (fv . 0 ) = ( 0. V) and

       A7: for j be Nat, v be Element of V st j < ( len Fv) & v = (Fv . (j + 1)) holds (fv . (j + 1)) = ((fv . j) + v) by RLVECT_1:def 12;

      defpred P[ Nat] means $1 <= ( len F) implies (f . $1) = (fv . $1);

      

       A8: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A9: P[i];

        set i1 = (i + 1);

        

         A10: the carrier of (n -VectSp_over F_Real ) = the carrier of ( TOP-REAL n)

        proof

          

          thus the carrier of (n -VectSp_over F_Real ) = ( REAL n) by MATRIX13: 102

          .= the carrier of ( TOP-REAL n) by EUCLID: 22;

        end;

        the carrier of (n -VectSp_over F_Real ) = (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

        then

        reconsider Fvi1 = (Fv /. i1), fvi = (fv . i) as Element of (n -tuples_on the carrier of F_Real ) by A10, Lm1;

        reconsider Fi1 = (F /. i1) as Element of T;

        assume

         A11: i1 <= ( len F);

        

         A13: i1 in ( dom F) by A11, NAT_1: 11, FINSEQ_3: 25;

        then (F . i1) = (F /. i1) by PARTFUN1:def 6;

        then

         A14: (f . i1) = ((f . i) + Fi1) by A4, A11, NAT_1: 13;

        

         A15: (Fv /. i1) = (Fv . i1) by A1, A13, PARTFUN1:def 6;

        then Fvi1 = (F /. i1) by A1, A13, PARTFUN1:def 6;

        

        hence (f . i1) = ((fv . i) + (Fv /. i1)) by A9, A11, A14, EUCLID: 64, NAT_1: 13

        .= (fv . i1) by A1, A7, A11, NAT_1: 13, A15;

      end;

      

       A16: P[ 0 ] by A3, A6, Lm2;

      for n be Nat holds P[n] from NAT_1:sch 2( A16, A8);

      hence thesis by A1, A2, A5;

    end;

    theorem :: MFOLD_2:20

    

     Th20: for Lv be Linear_Combination of ( RealVectSpace ( Seg n)), Lr be Linear_Combination of ( TOP-REAL n) st Lr = Lv holds ( Sum Lr) = ( Sum Lv)

    proof

      set V = ( RealVectSpace ( Seg n));

      set T = ( TOP-REAL n);

      let Lv be Linear_Combination of V;

      let Lr be Linear_Combination of T such that

       A1: Lr = Lv;

      consider F be FinSequence of the carrier of T such that

       A2: (F is one-to-one) & ( rng F) = ( Carrier Lr) and

       A3: ( Sum Lr) = ( Sum (Lr (#) F)) by RLVECT_2:def 8;

      reconsider F1 = F as FinSequence of the carrier of V by Lm1;

      

       A4: (Lr (#) F) = (Lv (#) F1) by A1, Th18;

      

      thus ( Sum Lv) = ( Sum (Lv (#) F1)) by A1, A2, RLVECT_2:def 8

      .= ( Sum Lr) by A3, A4, Th19;

    end;

    theorem :: MFOLD_2:21

    

     Th21: for Af be Subset of ( RealVectSpace ( Seg n)), Ar be Subset of ( TOP-REAL n) st Af = Ar holds Af is linearly-independent iff Ar is linearly-independent

    proof

      set V = ( RealVectSpace ( Seg n));

      let AV be Subset of V;

      set T = ( TOP-REAL n);

      let AR be Subset of T such that

       A1: AV = AR;

      hereby

        assume

         A2: AV is linearly-independent;

        now

          let L be Linear_Combination of AR;

          reconsider L1 = L as Linear_Combination of V by Th17;

          assume ( Sum L) = ( 0. T);

          

          then

           A3: ( 0. V) = ( Sum L) by Lm2

          .= ( Sum L1) by Th20;

          ( Carrier L) c= AR by RLVECT_2:def 6;

          then L1 is Linear_Combination of AV by A1, RLVECT_2:def 6;

          hence ( Carrier L) = {} by A2, A3, RLVECT_3:def 1;

        end;

        hence AR is linearly-independent by RLVECT_3:def 1;

      end;

      assume

       A4: AR is linearly-independent;

      now

        let L be Linear_Combination of AV;

        reconsider L1 = L as Linear_Combination of T by Th17;

        ( Carrier L) c= AV by RLVECT_2:def 6;

        then

        reconsider L1 as Linear_Combination of AR by A1, RLVECT_2:def 6;

        assume ( Sum L) = ( 0. V);

        

        then ( 0. T) = ( Sum L) by Lm2

        .= ( Sum L1) by Th20;

        hence ( Carrier L) = {} by A4, RLVECT_3:def 1;

      end;

      hence thesis by RLVECT_3:def 1;

    end;

    theorem :: MFOLD_2:22

    

     Th22: for V be Subset of ( TOP-REAL n) st V = ( RN_Base n) holds ex l be Linear_Combination of V st p = ( Sum l)

    proof

      let V be Subset of ( TOP-REAL n);

      assume

       A1: V = ( RN_Base n);

      reconsider p0 = p as Element of ( RealVectSpace ( Seg n)) by Lm1;

      reconsider V0 = V as Subset of ( RealVectSpace ( Seg n)) by Lm1;

      consider l0 be Linear_Combination of V0 such that

       A2: p0 = ( Sum l0) by A1, EUCLID_7: 43;

      reconsider l = l0 as Linear_Combination of ( TOP-REAL n) by Th17;

      ( Carrier l0) c= V0 by RLVECT_2:def 6;

      then

      reconsider l as Linear_Combination of V by RLVECT_2:def 6;

      take l;

      thus p = ( Sum l) by A2, Th20;

    end;

    theorem :: MFOLD_2:23

    ( RN_Base n) is Basis of ( TOP-REAL n)

    proof

      set A = ( RN_Base n);

      set T = ( TOP-REAL n);

      ( RN_Base n) c= ( REAL n);

      then

       A1: ( RN_Base n) c= the carrier of T by EUCLID: 22;

      reconsider A as finite Subset of T by EUCLID: 22;

      reconsider B = ( RN_Base n) as Subset of ( RealVectSpace ( Seg n)) by A1, Lm1;

      B is Basis of ( RealVectSpace ( Seg n)) by EUCLID_7: 45;

      then B is linearly-independent by RLVECT_3:def 3;

      then

       A2: A is linearly-independent by Th21;

      reconsider V1 = ( (Omega). T) as RealLinearSpace;

      for v be VECTOR of T st v in ( Lin A) holds v in V1

      proof

        let v be VECTOR of T;

        assume v in ( Lin A);

        v in the RLSStruct of T;

        hence v in V1 by RLSUB_1:def 4;

      end;

      then

      reconsider X = ( Lin A) as Subspace of V1 by RLSUB_1: 29;

      for x be object holds x in the carrier of X iff x in the carrier of V1

      proof

        let x be object;

        hereby

          assume x in the carrier of X;

          then x in X;

          then x in V1 by RLSUB_1: 9;

          hence x in the carrier of V1;

        end;

        assume x in the carrier of V1;

        then x in the RLSStruct of T by RLSUB_1:def 4;

        then

        reconsider x0 = x as Element of ( TOP-REAL n);

        ex l be Linear_Combination of A st x0 = ( Sum l) by Th22;

        then x in the set of all ( Sum l) where l be Linear_Combination of A;

        hence x in the carrier of X by RLVECT_3:def 2;

      end;

      then ( Lin A) = ( (Omega). T) by TARSKI: 2, EUCLID_7: 9;

      then ( Lin A) = the RLSStruct of T by RLSUB_1:def 4;

      hence ( RN_Base n) is Basis of T by A2, RLVECT_3:def 3;

    end;

    theorem :: MFOLD_2:24

    

     Th24: for V be Subset of ( TOP-REAL n) holds V in the topology of ( TOP-REAL n) iff for p st p in V holds ex r st r > 0 & ( Ball (p,r)) c= V

    proof

      let V be Subset of ( TOP-REAL n);

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      set T = ( TOP-REAL n);

      

       A1: the TopStruct of T = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      

       A2: ( TopSpaceMetr ( Euclid n)) = TopStruct (# the carrier of ( Euclid n), ( Family_open_set ( Euclid n)) #) by PCOMPS_1:def 5;

      reconsider V1 = V as Subset of ( Euclid n) by EUCLID: 67;

      hereby

        assume

         A3: V in the topology of T;

        let p;

        assume

         A4: p in V;

        reconsider x = p as Element of ( Euclid n) by EUCLID: 67;

        consider r be Real such that

         A5: r > 0 & ( Ball (x,r)) c= V1 by A3, A4, A1, A2, PCOMPS_1:def 4;

        reconsider r as Real;

        take r;

        thus r > 0 by A5;

        reconsider x1 = x as Point of ( Euclid n1);

        reconsider p1 = p as Point of ( TOP-REAL n1);

        thus ( Ball (p,r)) c= V by A5, TOPREAL9: 13;

      end;

      assume

       A6: for p st p in V holds ex r be Real st r > 0 & ( Ball (p,r)) c= V;

      for x be Element of ( Euclid n) st x in V1 holds ex r be Real st r > 0 & ( Ball (x,r)) c= V1

      proof

        let x be Element of ( Euclid n);

        assume

         A7: x in V1;

        reconsider p = x as Point of T by EUCLID: 67;

        consider r be Real such that

         A8: r > 0 & ( Ball (p,r)) c= V by A6, A7;

        take r;

        thus r > 0 by A8;

        reconsider x1 = x as Point of ( Euclid n1);

        reconsider p1 = p as Point of ( TOP-REAL n1);

        thus ( Ball (x,r)) c= V1 by A8, TOPREAL9: 13;

      end;

      hence V in the topology of T by A1, A2, PCOMPS_1:def 4;

    end;

    definition

      let n be Nat;

      let p be Point of ( TOP-REAL n);

      :: MFOLD_2:def1

      func InnerProduct (p) -> Function of ( TOP-REAL n), R^1 means

      : Def1: for q be Point of ( TOP-REAL n) holds (it . q) = |(p, q)|;

      existence

      proof

        defpred P[ object, object] means ex q be Point of ( TOP-REAL n) st q = $1 & $2 = |(p, q)|;

        

         A1: for x be object st x in the carrier of ( TOP-REAL n) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in the carrier of ( TOP-REAL n);

          then

          reconsider q3 = x as Point of ( TOP-REAL n);

          take |(p, q3)|;

          thus thesis;

        end;

        consider f1 be Function such that

         A2: ( dom f1) = the carrier of ( TOP-REAL n) & for x be object st x in the carrier of ( TOP-REAL n) holds P[x, (f1 . x)] from CLASSES1:sch 1( A1);

        ( rng f1) c= the carrier of R^1

        proof

          let z be object;

          assume z in ( rng f1);

          then

          consider xz be object such that

           A3: xz in ( dom f1) and

           A4: z = (f1 . xz) by FUNCT_1:def 3;

          ex q4 be Point of ( TOP-REAL n) st q4 = xz & (f1 . xz) = |(p, q4)| by A2, A3;

          hence thesis by A4, TOPMETR: 17, XREAL_0:def 1;

        end;

        then

        reconsider f2 = f1 as Function of ( TOP-REAL n), R^1 by A2, FUNCT_2:def 1, RELSET_1: 4;

        take f2;

        for q be Point of ( TOP-REAL n) holds (f1 . q) = |(p, q)|

        proof

          let q be Point of ( TOP-REAL n);

          ex q2 be Point of ( TOP-REAL n) st q2 = q & (f1 . q) = |(p, q2)| by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( TOP-REAL n), R^1 such that

         A6: for q be Point of ( TOP-REAL n) holds (f1 . q) = |(p, q)| and

         A7: for q be Point of ( TOP-REAL n) holds (f2 . q) = |(p, q)|;

        for q be Point of ( TOP-REAL n) holds (f1 . q) = (f2 . q)

        proof

          let q be Point of ( TOP-REAL n);

          

          thus (f1 . q) = |(p, q)| by A6

          .= (f2 . q) by A7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let n, p;

      cluster ( InnerProduct p) -> continuous;

      correctness

      proof

        set f = ( InnerProduct p);

        

         A1: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid n)), ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

        per cases ;

          suppose

           A2: p = ( 0. ( TOP-REAL n));

          

           A3: for q be Point of ( TOP-REAL n) holds (f . q) = 0

          proof

            let q be Point of ( TOP-REAL n);

            (f . q) = |(q, p)| by Def1;

            hence thesis by A2, EUCLID_2: 32;

          end;

          consider g be Function of ( TOP-REAL n), R^1 such that

           A4: (for p be Point of ( TOP-REAL n) holds (g . p) = 0 ) & g is continuous by JGRAPH_2: 20;

          for x be object st x in the carrier of ( TOP-REAL n) holds (f . x) = (g . x)

          proof

            let x be object;

            assume x in the carrier of ( TOP-REAL n);

            then

            reconsider q = x as Point of ( TOP-REAL n);

            

            thus (f . x) = (f . q)

            .= 0 by A3

            .= (g . q) by A4

            .= (g . x);

          end;

          hence thesis by A4, FUNCT_2: 12;

        end;

          suppose p <> ( 0. ( TOP-REAL n));

          then

           A5: |.p.| > 0 by EUCLID_2: 44;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          now

            let r be Real, u be Element of ( Euclid n), u1 be Element of RealSpace ;

            assume that

             A6: r > 0 and

             A7: u1 = (f1 . u);

            set s1 = (r / |.p.|);

            for w be Element of ( Euclid n), w1 be Element of RealSpace st w1 = (f1 . w) & ( dist (u,w)) < s1 holds ( dist (u1,w1)) < r

            proof

              let w be Element of ( Euclid n), w1 be Element of RealSpace ;

              assume that

               A8: w1 = (f1 . w) and

               A9: ( dist (u,w)) < s1;

              reconsider tu = u1, tw = w1 as Real by METRIC_1:def 13;

              reconsider qw = w, qu = u as Point of ( TOP-REAL n1) by TOPREAL3: 8;

              

               A10: ( dist (u1,w1)) = (the distance of RealSpace . (u1,w1)) by METRIC_1:def 1

              .= |.(tu - tw).| by METRIC_1:def 12, METRIC_1:def 13;

              

               A11: w1 = |(qw, p)| by Def1, A8;

               |.(tu - tw).| = |.( |(qu, p)| - |(qw, p)|).| by Def1, A7, A11

              .= |. |((qu - qw), p)|.| by EUCLID_2: 24;

              then

               A12: ( dist (u1,w1)) <= ( |.(qu - qw).| * |.p.|) by A10, EUCLID_2: 51;

              

               A13: (( dist (u,w)) * |.p.|) = ( |.(qu - qw).| * |.p.|) by JGRAPH_1: 28;

              (( dist (u,w)) * |.p.|) < ((r / |.p.|) * |.p.|) by A9, A5, XREAL_1: 68;

              then (( dist (u,w)) * |.p.|) < (r / ( |.p.| / |.p.|)) by XCMPLX_1: 82;

              then (( dist (u,w)) * |.p.|) < (r / 1) by A5, XCMPLX_1: 60;

              hence thesis by A13, A12, XXREAL_0: 2;

            end;

            hence ex s be Real st s > 0 & for w be Element of ( Euclid n), w1 be Element of RealSpace st w1 = (f1 . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r by A5, A6;

          end;

          then f1 is continuous by UNIFORM1: 3;

          hence thesis by A1, PRE_TOPC: 32, TOPMETR:def 6;

        end;

      end;

    end

    begin

    definition

      let n;

      let p, q;

      :: MFOLD_2:def2

      func Plane (p,q) -> Subset of ( TOP-REAL n) equals { y where y be Point of ( TOP-REAL n) : |(p, (y - q))| = 0 };

      correctness

      proof

        set X = { y where y be Point of ( TOP-REAL n) : |(p, (y - q))| = 0 };

        now

          let x be object;

          assume x in X;

          then

          consider y be Point of ( TOP-REAL n) such that

           A1: x = y & |(p, (y - q))| = 0 ;

          thus x in the carrier of ( TOP-REAL n) by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: MFOLD_2:25

    

     Th25: (( transl (p1,( TOP-REAL n))) .: ( Plane (p,p2))) = ( Plane (p,(p1 + p2)))

    proof

       A1:

      now

        let y be object;

        assume y in (( transl (p1,( TOP-REAL n))) .: ( Plane (p,p2)));

        then

        consider x be object such that

         A2: [x, y] in ( transl (p1,( TOP-REAL n))) & x in ( Plane (p,p2)) by RELAT_1:def 13;

        consider x1 be Point of ( TOP-REAL n) such that

         A3: x = x1 & |(p, (x1 - p2))| = 0 by A2;

        

         A4: y = (( transl (p1,( TOP-REAL n))) . x1) by A2, A3, FUNCT_1: 1

        .= (p1 + x1) by RLTOPSP1:def 10;

        x in ( dom ( transl (p1,( TOP-REAL n)))) & y = (( transl (p1,( TOP-REAL n))) . x) by A2, FUNCT_1: 1;

        then y in ( rng ( transl (p1,( TOP-REAL n)))) by FUNCT_1: 3;

        then

        reconsider y1 = y as Point of ( TOP-REAL n);

        (x1 - p2) = ((x1 - p2) + ( 0. ( TOP-REAL n))) by RLVECT_1: 4

        .= ((x1 - p2) + (p1 + ( - p1))) by RLVECT_1: 5

        .= (((x1 + ( - p2)) + p1) + ( - p1)) by RLVECT_1:def 3

        .= ((y1 - p2) - p1) by A4, RLVECT_1:def 3

        .= (y1 - (p1 + p2)) by RLVECT_1: 27;

        hence y in ( Plane (p,(p1 + p2))) by A3;

      end;

      now

        let y be object;

        assume y in ( Plane (p,(p1 + p2)));

        then

        consider y1 be Point of ( TOP-REAL n) such that

         A5: y = y1 & |(p, (y1 - (p1 + p2)))| = 0 ;

        set x = (y1 - p1);

        x in the carrier of ( TOP-REAL n);

        then

         A6: x in ( dom ( transl (p1,( TOP-REAL n)))) by FUNCT_2:def 1;

        (p1 + x) = y1 by RLVECT_4: 1;

        then (( transl (p1,( TOP-REAL n))) . x) = y1 by RLTOPSP1:def 10;

        then

         A7: [x, y1] in ( transl (p1,( TOP-REAL n))) by A6, FUNCT_1: 1;

        (x - p2) = (y1 - (p1 + p2)) by RLVECT_1: 27;

        then x in ( Plane (p,p2)) by A5;

        hence y in (( transl (p1,( TOP-REAL n))) .: ( Plane (p,p2))) by A5, A7, RELAT_1:def 13;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: MFOLD_2:26

    

     Th26: p <> ( 0. ( TOP-REAL n)) implies ex A be linearly-independent Subset of ( TOP-REAL n) st ( card A) = (n - 1) & ( [#] ( Lin A)) = ( Plane (p,( 0. ( TOP-REAL n))))

    proof

      assume

       A1: p <> ( 0. ( TOP-REAL n));

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      

       A2: ( 0. ( TOP-REAL n)) = ( - ( 0. ( TOP-REAL n1))) by JGRAPH_5: 10

      .= ( - ( 0. ( TOP-REAL n)));

      set V1 = ( Plane (p,( 0. ( TOP-REAL n))));

       |(p, ( 0. ( TOP-REAL n)))| = 0 by EUCLID_2: 32;

      then |(p, (( 0. ( TOP-REAL n)) - ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 5;

      then

       A3: ( 0. ( TOP-REAL n)) in V1;

      

       A4: for v,u be VECTOR of ( TOP-REAL n) st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v,u be VECTOR of ( TOP-REAL n);

        assume v in V1;

        then

        consider v1 be Point of ( TOP-REAL n) such that

         A5: v = v1 & |(p, (v1 - ( 0. ( TOP-REAL n))))| = 0 ;

        assume u in V1;

        then

        consider u1 be Point of ( TOP-REAL n) such that

         A6: u = u1 & |(p, (u1 - ( 0. ( TOP-REAL n))))| = 0 ;

         |(p, ((v1 + u1) - ( 0. ( TOP-REAL n))))| = |(p, (v1 + (u1 - ( 0. ( TOP-REAL n)))))| by RLVECT_1:def 3

        .= ( |(p, v1)| + |(p, (u1 - ( 0. ( TOP-REAL n))))|) by EUCLID_2: 26

        .= 0 by A5, A2, A6, RLVECT_1: 4;

        hence (v + u) in V1 by A5, A6;

      end;

      for a be Real holds for v be VECTOR of ( TOP-REAL n) st v in V1 holds (a * v) in V1

      proof

        let a be Real;

        let v be VECTOR of ( TOP-REAL n);

        assume v in V1;

        then

        consider v1 be Point of ( TOP-REAL n) such that

         A7: v = v1 & |(p, (v1 - ( 0. ( TOP-REAL n))))| = 0 ;

         |(p, (a * (v1 - ( 0. ( TOP-REAL n)))))| = (a * 0 qua Real) by A7, EUCLID_2: 20;

        then |(p, ((a * v1) - (a * ( 0. ( TOP-REAL n)))))| = 0 by RLVECT_1: 34;

        then |(p, ((a * v1) - ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 10;

        hence (a * v) in V1 by A7;

      end;

      then

      consider W be strict Subspace of ( TOP-REAL n) such that

       A8: V1 = the carrier of W by A3, RLSUB_1: 35, A4, RLSUB_1:def 1;

      set A1 = the Basis of W;

      

       A10: ( [#] ( Lin A1)) = ( Plane (p,( 0. ( TOP-REAL n)))) by A8, RLVECT_3:def 3;

      reconsider A = A1 as linearly-independent Subset of ( TOP-REAL n) by RLVECT_3:def 3, RLVECT_5: 14;

      take A;

      reconsider A2 = {p} as linearly-independent Subset of ( TOP-REAL n) by A1, RLVECT_3: 8;

      

       A11: ( dim ( Lin A2)) = ( card A2) by RLVECT_5: 29

      .= 1 by CARD_1: 30;

      for v be VECTOR of ( TOP-REAL n) holds ex v1,v2 be VECTOR of ( TOP-REAL n) st v1 in ( Lin A) & v2 in ( Lin A2) & v = (v1 + v2)

      proof

        let v be VECTOR of ( TOP-REAL n);

        set a = ( |(p, v)| / |(p, p)|);

        set v2 = (a * p);

        set v1 = (v - v2);

        reconsider v1, v2 as VECTOR of ( TOP-REAL n);

        take v1, v2;

        

         A12: |(p, p)| > 0 by A1, EUCLID_2: 43;

         |(p, v1)| = ( |(p, v)| - |(p, v2)|) by EUCLID_2: 27

        .= ( |(p, v)| - (a * |(p, p)|)) by EUCLID_2: 20

        .= ( |(p, v)| - |(p, v)|) by A12, XCMPLX_1: 87

        .= 0 ;

        then |(p, (v1 - ( 0. ( TOP-REAL n))))| = 0 by A2, RLVECT_1: 4;

        then v1 in ( Lin A1) by A10;

        hence v1 in ( Lin A) by RLVECT_5: 20;

        thus v2 in ( Lin A2) by RLVECT_4: 8;

        thus thesis by RLVECT_4: 1;

      end;

      then

       A13: the RLSStruct of ( TOP-REAL n) = (( Lin A) + ( Lin A2)) by RLSUB_2: 44;

      (( Lin A) /\ ( Lin A2)) = ( (0). ( TOP-REAL n))

      proof

        for v be VECTOR of ( TOP-REAL n) holds v in (( Lin A) /\ ( Lin A2)) iff v in ( (0). ( TOP-REAL n))

        proof

          let v be VECTOR of ( TOP-REAL n);

          hereby

            assume v in (( Lin A) /\ ( Lin A2));

            then

             A14: v in ( Lin A) & v in ( Lin A2) by RLSUB_2: 3;

            then

            consider a be Real such that

             A15: v = (a * p) by RLVECT_4: 8;

            v in ( Plane (p,( 0. ( TOP-REAL n)))) by A10, A14, RLVECT_5: 20;

            then

            consider y be Point of ( TOP-REAL n) such that

             A16: y = v & |(p, (y - ( 0. ( TOP-REAL n))))| = 0 ;

             |(p, v)| = 0 by A2, A16, RLVECT_1: 4;

            then

             A17: (a * |(p, p)|) = 0 by A15, EUCLID_2: 20;

             |(p, p)| > 0 by A1, EUCLID_2: 43;

            then a = 0 by A17;

            then v = ( 0. ( TOP-REAL n)) by A15, RLVECT_1: 10;

            hence v in ( (0). ( TOP-REAL n)) by RLVECT_3: 29;

          end;

          assume v in ( (0). ( TOP-REAL n));

          then v = ( 0. ( TOP-REAL n)) by RLVECT_3: 29;

          hence v in (( Lin A) /\ ( Lin A2)) by RLSUB_1: 17;

        end;

        hence thesis by RLSUB_1: 31;

      end;

      then ( dim ( TOP-REAL n)) = (( dim ( Lin A)) + ( dim ( Lin A2))) by RLVECT_5: 37, A13, RLSUB_2:def 4;

      then n = (( dim ( Lin A)) + 1) by A11, RLAFFIN3: 4;

      hence ( card A) = (n - 1) by RLVECT_5: 29;

      thus ( [#] ( Lin A)) = ( Plane (p,( 0. ( TOP-REAL n)))) by A10, RLVECT_5: 20;

    end;

    theorem :: MFOLD_2:27

    

     Th27: p1 <> ( 0. ( TOP-REAL n)) & p2 <> ( 0. ( TOP-REAL n)) implies ex R be Function of ( TOP-REAL n), ( TOP-REAL n) st R is being_homeomorphism & (R .: ( Plane (p1,( 0. ( TOP-REAL n))))) = ( Plane (p2,( 0. ( TOP-REAL n))))

    proof

      assume p1 <> ( 0. ( TOP-REAL n));

      then

      consider B1 be linearly-independent Subset of ( TOP-REAL n) such that

       A1: ( card B1) = (n - 1) & ( [#] ( Lin B1)) = ( Plane (p1,( 0. ( TOP-REAL n)))) by Th26;

      assume p2 <> ( 0. ( TOP-REAL n));

      then

      consider B2 be linearly-independent Subset of ( TOP-REAL n) such that

       A2: ( card B2) = (n - 1) & ( [#] ( Lin B2)) = ( Plane (p2,( 0. ( TOP-REAL n)))) by Th26;

      consider M be Matrix of n, F_Real such that

       A3: M is invertible & (( Mx2Tran M) .: ( [#] ( Lin B1))) = ( [#] ( Lin B2)) by A1, A2, MATRTOP2: 22;

      reconsider M as invertible Matrix of n, F_Real by A3;

      take ( Mx2Tran M);

      thus thesis by A1, A2, A3;

    end;

    definition

      let n;

      let p, q;

      :: MFOLD_2:def3

      func TPlane (p,q) -> non empty SubSpace of ( TOP-REAL n) equals (( TOP-REAL n) | ( Plane (p,q)));

      correctness

      proof

         |(p, ( 0. ( TOP-REAL n)))| = 0 by EUCLID_2: 32;

        then |(p, (q - q))| = 0 by RLVECT_1: 5;

        then q in ( Plane (p,q));

        hence thesis;

      end;

    end

    theorem :: MFOLD_2:28

    

     Th28: ( Base_FinSeq ((n + 1),(n + 1))) = (( 0. ( TOP-REAL n)) ^ <*1*>)

    proof

      set N = ( Base_FinSeq ((n + 1),(n + 1)));

      set p = ( 0. ( TOP-REAL n));

      set q = <*1*>;

      

       A1: ( dom N) = ( Seg (n + 1)) by FINSEQ_1: 89

      .= ( Seg (n + ( len q))) by FINSEQ_1: 39

      .= ( Seg (( len p) + ( len q))) by CARD_1:def 7;

      

       A2: for k st k in ( dom p) holds (N . k) = (p . k)

      proof

        let k;

        assume k in ( dom p);

        then k in ( Seg n) by FINSEQ_1: 89;

        then

         A3: 1 <= k & k <= n by FINSEQ_1: 1;

        ( 0 + n) <= (1 + n) by XREAL_1: 6;

        then

         A4: k <= (n + 1) by A3, XXREAL_0: 2;

        

         A5: (n + 1) <> k by A3, NAT_1: 13;

        

        thus (N . k) = 0 by A4, A3, A5, MATRIXR2: 76

        .= (( 0* n) . k)

        .= (p . k) by EUCLID: 70;

      end;

      for k st k in ( dom q) holds (N . (( len p) + k)) = (q . k)

      proof

        let k;

        assume k in ( dom q);

        then k in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A6: k = 1 by TARSKI:def 1;

        

         A7: ( 0 + 1) <= (n + 1) by XREAL_1: 6;

        

        thus (N . (( len p) + k)) = (( Base_FinSeq ((n + 1),(n + 1))) . (n + 1)) by A6, CARD_1:def 7

        .= 1 by A7, MATRIXR2: 75

        .= (q . k) by A6, FINSEQ_1: 40;

      end;

      hence thesis by A1, A2, FINSEQ_1:def 7;

    end;

    

     Lm3: for p0 be Point of ( TOP-REAL (n + 1)) st p0 = ( Base_FinSeq ((n + 1),(n + 1))) holds (( TOP-REAL n),( TPlane (p0,( 0. ( TOP-REAL (n + 1)))))) are_homeomorphic

    proof

      let p0 be Point of ( TOP-REAL (n + 1)) such that

       A1: p0 = ( Base_FinSeq ((n + 1),(n + 1)));

      set T = ( TOP-REAL n);

      set S = ( TPlane (p0,( 0. ( TOP-REAL (n + 1)))));

      defpred P[ set, set] means for p be Element of T st $1 = p holds $2 = (p ^ <* 0 *>);

      

       A2: for p be Element of T holds (p ^ <* 0 *>) is Element of S

      proof

        let p be Element of T;

        

         A3: ( len p) = n by CARD_1:def 7;

        

         A4: ( len (p ^ <* 0 *>)) = (n + 1) by CARD_1:def 7;

        ( rng (p ^ <* 0 *>)) c= REAL ;

        then (p ^ <* 0 *>) in ( REAL (n + 1)) by A4, FINSEQ_2: 132;

        then

        reconsider q = (p ^ <* 0 *>) as Point of ( TOP-REAL (n + 1)) by EUCLID: 22;

        reconsider r0 = 0 as Real;

        ( dom p0) = ( Seg (n + 1)) & ( dom q) = ( Seg (n + 1)) by FINSEQ_1: 89;

        then (( dom p0) /\ ( dom q)) = ( Seg (n + 1));

        then

         A5: ( dom ( mlt (p0,q))) = ( Seg (n + 1)) by VALUED_1:def 4;

        for y be object holds y in ( rng ( mlt (p0,q))) iff y = r0

        proof

          let y be object;

          set f = ( mlt (p0,q));

           A6:

          now

            let x be set;

            assume x in ( Seg (n + 1));

            then

            consider k be Nat such that

             A7: x = k & 1 <= k & k <= (n + 1);

            

             A8: (f . x) = ((p0 . x) * (q . x)) by VALUED_1: 5;

            per cases ;

              suppose

               A9: k = (n + 1);

              1 <= ( len <*r0*>) by FINSEQ_1: 39;

              

              then (q . (( len p) + 1)) = ( <*r0*> . 1) by FINSEQ_1: 65

              .= r0 by FINSEQ_1: 40;

              hence (f . x) = r0 by A8, A7, A9, A3;

            end;

              suppose k <> (n + 1);

              then (p0 . x) = 0 by A1, A7, MATRIXR2: 76;

              hence (f . x) = r0 by A8;

            end;

          end;

          hereby

            assume y in ( rng f);

            then

            consider x be object such that

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

            thus y = r0 by A10, A5, A6;

          end;

          assume

           A11: y = r0;

          consider x be object such that

           A12: x in ( Seg (n + 1)) by XBOOLE_0:def 1;

          y = (f . x) by A11, A12, A6;

          hence y in ( rng f) by A12, A5, FUNCT_1:def 3;

        end;

        then ( mlt (p0,q)) = (( Seg (n + 1)) --> r0) by A5, FUNCOP_1: 9, TARSKI:def 1;

        then

         A14: ( mlt (p0,q)) = ((n + 1) |-> r0) by FINSEQ_2:def 2;

        

         A15: |(p0, q)| = ( Sum ( mlt (p0,q))) by RVSUM_1:def 16

        .= ((n + 1) * r0) by A14, RVSUM_1: 80

        .= 0 ;

         |(p0, (q - ( 0. ( TOP-REAL (n + 1)))))| = ( |(p0, q)| - |(p0, ( 0. ( TOP-REAL (n + 1))))|) by EUCLID_2: 27

        .= ( |(p0, q)| - 0 ) by EUCLID_2: 32

        .= 0 by A15;

        then (p ^ <* 0 *>) in ( Plane (p0,( 0. ( TOP-REAL (n + 1)))));

        then (p ^ <* 0 *>) in ( [#] S) by PRE_TOPC:def 5;

        hence (p ^ <* 0 *>) is Element of S;

      end;

      

       A16: for x be Element of T holds ex y be Element of S st P[x, y]

      proof

        let x be Element of T;

        set y = (x ^ <* 0 *>);

        reconsider y as Element of S by A2;

        take y;

        thus P[x, y];

      end;

      consider f be Function of T, S such that

       A17: for x be Element of T holds P[x, (f . x)] from FUNCT_2:sch 3( A16);

      

       A18: ( dom f) = ( [#] T) by FUNCT_2:def 1;

      

       A19: for y be object holds y in ( [#] S) iff ex x be object st x in ( dom f) & y = (f . x)

      proof

        let y be object;

        hereby

          assume y in ( [#] S);

          then y in ( Plane (p0,( 0. ( TOP-REAL (n + 1))))) by PRE_TOPC:def 5;

          then

          consider q be Point of ( TOP-REAL (n + 1)) such that

           A20: y = q & |(p0, (q - ( 0. ( TOP-REAL (n + 1)))))| = 0 ;

          

           A21: ( len q) = (n + 1) & ( rng q) c= REAL by CARD_1:def 7;

          then

          reconsider q1 = q as FinSequence of REAL by FINSEQ_1:def 4;

          set p = (q1 | n);

          reconsider x = p as object;

          take x;

          ( 0 + n) <= (1 + n) by XREAL_1: 6;

          then

           A22: ( len p) = n by A21, FINSEQ_1: 59;

          

           A23: ( rng p) c= REAL ;

          

           A24: p in ( REAL n) by A22, A23, FINSEQ_2: 132;

          hence x in ( dom f) by A18, EUCLID: 22;

          reconsider x1 = x as Element of T by A24, EUCLID: 22;

           P[x1, (f . x1)] by A17;

          then

           A25: (f . x) = (p ^ <* 0 *>);

          

           A26: q = (p ^ <*(q . (n + 1))*>) by CARD_1:def 7, FINSEQ_3: 55;

          

           A27: |(p0, (q - ( 0. ( TOP-REAL (n + 1)))))| = ( |(p0, q)| - |(p0, ( 0. ( TOP-REAL (n + 1))))|) by EUCLID_2: 27

          .= ( |(p0, q)| - 0 ) by EUCLID_2: 32

          .= |(p0, q)|;

          reconsider f0 = ( 0. ( TOP-REAL n)) as FinSequence of REAL by EUCLID: 24;

          ( rng <*1*>) c= REAL ;

          then

          reconsider f1 = <*1*> as FinSequence of REAL by FINSEQ_1:def 4;

          reconsider f3 = <*(q . (n + 1))*> as FinSequence of REAL by RVSUM_1: 145;

          p in ( REAL n) by A22, A23, FINSEQ_2: 132;

          then

          reconsider p1 = p as Point of ( TOP-REAL n) by EUCLID: 22;

          

           A28: |((f0 ^ f1), (p ^ f3))| = 0 by A1, A26, A27, A20, Th28;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          ( 0. ( TOP-REAL n)) in the carrier of ( TOP-REAL n);

          then f0 in ( REAL n) by EUCLID: 22;

          then f0 in ( Funcs (( Seg n1), REAL )) by FINSEQ_2: 93;

          then

          consider g be Function such that

           A29: f0 = g & ( dom g) = ( Seg n1) & ( rng g) c= REAL by FUNCT_2:def 2;

          

           A30: ( len f0) = ( len p) by A22, A29, FINSEQ_1:def 3;

          ( len f1) = 1 by FINSEQ_1: 39

          .= ( len f3) by FINSEQ_1: 39;

          then ( |(( 0. ( TOP-REAL n)), p1)| + |(f1, f3)|) = 0 by A28, A30, Th15;

          then ( 0 + |(f1, f3)|) = 0 by EUCLID_2: 33;

          then ( Sum ( mlt (f1,f3))) = 0 by RVSUM_1:def 16;

          then ( Sum <*(1 * (q . (n + 1)))*>) = 0 by RVSUM_1: 62;

          hence y = (f . x) by A20, A25, A26, RVSUM_1: 73;

        end;

        given x be object such that

         A31: x in ( dom f) & y = (f . x);

        reconsider p = x as Element of T by A31;

         P[p, (f . p)] by A17;

        hence y in ( [#] S) by A31;

      end;

      then

       A32: ( rng f) = ( [#] S) by FUNCT_1: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

         A33: x1 in ( dom f) & x2 in ( dom f);

        assume

         A34: (f . x1) = (f . x2);

        reconsider p1 = x1, p2 = x2 as Element of T by A33;

        (f . p1) = (p1 ^ <* 0 *>) & (f . p2) = (p2 ^ <* 0 *>) by A17;

        hence x1 = x2 by A34, FINSEQ_1: 33;

      end;

      then

       A35: f is one-to-one;

      set T1 = ( TOP-REAL (n + 1));

      

       A36: for p1 be Point of T holds (f . p1) is Point of T1

      proof

        let p1 be Point of T;

        ( [#] S) c= ( [#] T1) by PRE_TOPC:def 4;

        hence (f . p1) is Point of T1;

      end;

      

       A37: for p1 be Point of T, q1 be Point of T1 st q1 = (f . p1) holds |.p1.| = |.q1.|

      proof

        let p1 be Point of T;

        let q1 be Point of T1;

        assume q1 = (f . p1);

        then

         A38: q1 = (p1 ^ <* 0 *>) by A17;

        reconsider x = q1 as Element of ( REAL (n + 1)) by EUCLID: 22;

        

         A39: ( len p1) = n & ( rng p1) c= REAL by CARD_1:def 7;

        

         A40: (x | n) = ((p1 ^ <* 0 *>) | ( dom p1)) by A38, FINSEQ_1: 89

        .= p1 by FINSEQ_1: 21;

        

         A41: (x . (n + 1)) = 0 by A38, A39, FINSEQ_1: 42;

        

         A42: ( |.q1.| ^2 ) = (( |.p1.| ^2 ) + ( 0 ^2 )) by A40, A41, REAL_NS1: 10

        .= (( |.p1.| ^2 ) + ( 0 * 0 )) by SQUARE_1:def 1

        .= ( |.p1.| ^2 );

        ( |.q1.| * |.q1.|) >= 0 ;

        then

         A43: ( |.q1.| ^2 ) >= 0 by SQUARE_1:def 1;

        ( |.p1.| * |.p1.|) >= 0 ;

        then ( |.p1.| ^2 ) >= 0 by SQUARE_1:def 1;

        

        hence |.p1.| = ( sqrt ( |.q1.| ^2 )) by A42, SQUARE_1:def 2

        .= |.q1.| by A43, SQUARE_1:def 2;

      end;

      

       A44: for p1,p2 be Point of T, q1,q2 be Point of T1 st q1 = (f . p1) & q2 = (f . p2) holds (f . (p1 - p2)) = (q1 - q2)

      proof

        let p1,p2 be Point of T;

        let q1,q2 be Point of T1;

        assume q1 = (f . p1);

        then

         A45: q1 = (p1 ^ <* 0 *>) by A17;

        assume q2 = (f . p2);

        then

         A46: q2 = (p2 ^ <* 0 *>) by A17;

        

         A47: (f . (p1 - p2)) = ((p1 - p2) ^ <* 0 *>) by A17;

        reconsider qa = (f . (p1 - p2)) as Point of T1 by A36;

        

         A48: ( dom ((p1 - p2) ^ <* 0 *>)) = ( Seg (n + 1)) by FINSEQ_1: 89

        .= ( dom (q1 - q2)) by FINSEQ_1: 89;

        for k be Nat st k in ( dom (q1 - q2)) holds ((q1 - q2) . k) = (((p1 - p2) ^ <* 0 *>) . k)

        proof

          let k be Nat;

          assume k in ( dom (q1 - q2));

          then

           A49: k in ( Seg (n + 1)) by FINSEQ_1: 89;

          

           A50: ((q1 - q2) . k) = ((q1 . k) + (( - q2) . k)) by A49, Th16

          .= ((q1 . k) + ((( - 1) * q2) . k)) by RLVECT_1: 16

          .= ((q1 . k) + (( - 1) * (q2 . k))) by VALUED_1: 6;

          

           A51: k in (( Seg n) \/ {(n + 1)}) by A49, FINSEQ_1: 9;

          per cases by A51, XBOOLE_0:def 3;

            suppose

             A52: k in ( Seg n);

            then k in ( dom p1) & k in ( dom p2) by FINSEQ_1: 89;

            then

             A53: (q1 . k) = (p1 . k) & (q2 . k) = (p2 . k) by A45, A46, FINSEQ_1:def 7;

            k in ( dom (p1 - p2)) by A52, FINSEQ_1: 89;

            

            then (((p1 - p2) ^ <* 0 *>) . k) = ((p1 - p2) . k) by FINSEQ_1:def 7

            .= ((p1 . k) + (( - p2) . k)) by A52, Th16

            .= ((p1 . k) + ((( - 1) * p2) . k)) by RLVECT_1: 16

            .= ((p1 . k) + (( - 1) * (p2 . k))) by VALUED_1: 6;

            hence thesis by A50, A53;

          end;

            suppose k in {(n + 1)};

            then

             A54: k = (n + 1) by TARSKI:def 1;

            ( len p1) = n & ( len p2) = n by CARD_1:def 7;

            then

             A55: (q1 . k) = 0 & (q2 . k) = 0 by A45, A46, A54, FINSEQ_1: 42;

            ( len (p1 - p2)) = n by CARD_1:def 7;

            hence thesis by A50, A55, A54, FINSEQ_1: 42;

          end;

        end;

        hence (f . (p1 - p2)) = (q1 - q2) by A47, A48, FINSEQ_1: 13;

      end;

      

       A56: (f .: ( [#] T)) = ( [#] S) by A32, RELSET_1: 22;

      for P be Subset of T holds P is closed iff (f .: P) is closed

      proof

        let P be Subset of T;

        hereby

          assume P is closed;

          then

           A57: (( [#] T) \ P) in the topology of T by PRE_TOPC:def 2, PRE_TOPC:def 3;

          set FQ = { ( Ball (q,r)) where q be Point of T1, r be Real : ex p be Point of T st q = (f . p) & ( Ball (p,r)) c= (( [#] T) \ P) };

          for x be object st x in FQ holds x in ( bool ( [#] T1))

          proof

            let x be object;

            assume x in FQ;

            then

            consider q be Point of T1, r be Real such that

             A58: x = ( Ball (q,r)) & ex p be Point of T st q = (f . p) & ( Ball (p,r)) c= (( [#] T) \ P);

            thus x in ( bool ( [#] T1)) by A58;

          end;

          then

          reconsider FQ as Subset-Family of T1 by TARSKI:def 3;

          

           B60: for Q be Subset of T1 st Q in FQ holds Q is open

          proof

            let Q be Subset of T1;

            assume Q in FQ;

            then

            consider q be Point of T1, r be Real such that

             A59: Q = ( Ball (q,r)) & ex p be Point of T st q = (f . p) & ( Ball (p,r)) c= (( [#] T) \ P);

            thus Q is open by A59;

          end;

          set Q = ( union FQ);

          Q is open by B60, TOPS_2:def 1, TOPS_2: 19;

          then

           A61: Q in the topology of T1 by PRE_TOPC:def 2;

          for y be Element of S holds y in (f .: (( [#] T) \ P)) iff y in (Q /\ ( [#] S))

          proof

            let y be Element of S;

            hereby

              assume y in (f .: (( [#] T) \ P));

              then

              consider x be object such that

               A62: x in ( dom f) & x in (( [#] T) \ P) & y = (f . x) by FUNCT_1:def 6;

              reconsider p = x as Point of T by A62;

              reconsider q = y as Point of T1 by A62, A36;

              consider r be Real such that

               A63: r > 0 & ( Ball (p,r)) c= (( [#] T) \ P) by A62, A57, Th24;

              

               A64: ( Ball (q,r)) in FQ by A62, A63;

              q in ( Ball (q,r)) by A63, JORDAN: 16;

              then y in Q by A64, TARSKI:def 4;

              hence y in (Q /\ ( [#] S)) by XBOOLE_0:def 4;

            end;

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

            then y in Q by XBOOLE_0:def 4;

            then

            consider Y be set such that

             A65: y in Y & Y in FQ by TARSKI:def 4;

            consider q be Point of T1, r be Real such that

             A66: Y = ( Ball (q,r)) and

             A67: ex p be Point of T st q = (f . p) & ( Ball (p,r)) c= (( [#] T) \ P) by A65;

            consider p be Point of T such that

             A68: q = (f . p) & ( Ball (p,r)) c= (( [#] T) \ P) by A67;

            consider x be object such that

             A69: x in ( dom f) & y = (f . x) by A19;

            reconsider p1 = x as Point of T by A69;

            reconsider q1 = y as Point of T1 by A69, A36;

            q1 in { qy where qy be Point of T1 : |.(qy - q).| < r } by A65, A66, TOPREAL9:def 1;

            then

            consider qy be Point of T1 such that

             A70: qy = q1 & |.(qy - q).| < r;

            (f . (p1 - p)) = (q1 - q) by A69, A68, A44;

            then |.(p1 - p).| < r by A70, A37;

            then p1 in { px where px be Point of T : |.(px - p).| < r };

            then p1 in ( Ball (p,r)) by TOPREAL9:def 1;

            hence y in (f .: (( [#] T) \ P)) by A69, A68, FUNCT_1:def 6;

          end;

          then

           A71: (f .: (( [#] T) \ P)) = (Q /\ ( [#] S)) by SUBSET_1: 3;

          (( [#] S) \ (f .: P)) = (Q /\ ( [#] S)) by A71, A35, A56, FUNCT_1: 64;

          then (( [#] S) \ (f .: P)) in the topology of S by A61, PRE_TOPC:def 4;

          hence (f .: P) is closed by PRE_TOPC:def 2, PRE_TOPC:def 3;

        end;

        assume (f .: P) is closed;

        then (( [#] S) \ (f .: P)) in the topology of S by PRE_TOPC:def 3, PRE_TOPC:def 2;

        then

        consider Q be Subset of T1 such that

         A72: Q in the topology of T1 & (( [#] S) \ (f .: P)) = (Q /\ ( [#] S)) by PRE_TOPC:def 4;

        for p be Point of T st p in (( [#] T) \ P) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (( [#] T) \ P)

        proof

          let p be Point of T;

          assume p in (( [#] T) \ P);

          then (f . p) in (f .: (( [#] T) \ P)) by A18, FUNCT_1:def 6;

          then

           A73: (f . p) in (( [#] S) \ (f .: P)) by A56, A35, FUNCT_1: 64;

          reconsider q = (f . p) as Point of T1 by A36;

          q in Q by A72, A73, XBOOLE_0:def 4;

          then

          consider r be Real such that

           A74: r > 0 & ( Ball (q,r)) c= Q by A72, Th24;

          take r;

          thus r > 0 by A74;

          let x be object;

          assume x in ( Ball (p,r));

          then x in { px where px be Point of T : |.(px - p).| < r } by TOPREAL9:def 1;

          then

          consider p1 be Point of T such that

           A75: x = p1 & |.(p1 - p).| < r;

          reconsider q1 = (f . p1) as Point of T1 by A36;

          (f . (p1 - p)) = (q1 - q) by A44;

          then |.(q1 - q).| < r by A75, A37;

          then q1 in { qx where qx be Point of T1 : |.(qx - q).| < r };

          then q1 in ( Ball (q,r)) by TOPREAL9:def 1;

          then q1 in (Q /\ ( [#] S)) by A74, XBOOLE_0:def 4;

          then not q1 in (f .: P) by A72, XBOOLE_0:def 5;

          then not x in P by A18, A75, FUNCT_1:def 6;

          hence x in (( [#] T) \ P) by A75, XBOOLE_0:def 5;

        end;

        then (( [#] T) \ P) is open by Th24, PRE_TOPC:def 2;

        hence P is closed by PRE_TOPC:def 3;

      end;

      hence thesis by T_0TOPSP:def 1, A18, A32, A35, TOPS_2: 58;

    end;

    theorem :: MFOLD_2:29

    

     Th29: for p,q be Point of ( TOP-REAL (n + 1)) st p <> ( 0. ( TOP-REAL (n + 1))) holds (( TOP-REAL n),( TPlane (p,q))) are_homeomorphic

    proof

      set T1 = ( TOP-REAL (n + 1));

      let p,q be Point of T1;

      assume

       A1: p <> ( 0. T1);

      reconsider p0 = ( Base_FinSeq ((n + 1),(n + 1))) as Point of T1 by EUCLID: 22;

      

       A2: p0 <> ( 0. T1)

      proof

        assume

         A3: p0 = ( 0. T1);

        ( 0 + 1) <= (n + 1) by XREAL_1: 6;

        then |.p0.| = 1 by EUCLID_7: 28;

        hence contradiction by A3, EUCLID_2: 39;

      end;

      

       A4: (( TOP-REAL n),( TPlane (p0,( 0. ( TOP-REAL (n + 1)))))) are_homeomorphic by Lm3;

      ex R be Function of T1, T1 st R is being_homeomorphism & (R .: ( Plane (p0,( 0. T1)))) = ( Plane (p,( 0. T1))) by A1, A2, Th27;

      then (( TPlane (p0,( 0. T1))),( TPlane (p,( 0. T1)))) are_homeomorphic by METRIZTS: 3, METRIZTS:def 1;

      then

       A5: (( TOP-REAL n),( TPlane (p,( 0. T1)))) are_homeomorphic by A4, BORSUK_3: 3;

      (( transl (q,T1)) .: ( Plane (p,( 0. T1)))) = ( Plane (p,(( 0. T1) + q))) by Th25

      .= ( Plane (p,q)) by RLVECT_1: 4;

      then ((T1 | ( Plane (p,( 0. T1)))),(T1 | ( Plane (p,q)))) are_homeomorphic by METRIZTS: 3, METRIZTS:def 1;

      hence thesis by A5, BORSUK_3: 3;

    end;

    theorem :: MFOLD_2:30

    for p,q be Point of ( TOP-REAL (n + 1)) st p <> ( 0. ( TOP-REAL (n + 1))) holds ( TPlane (p,q)) is n -manifold

    proof

      let p,q be Point of ( TOP-REAL (n + 1));

      assume p <> ( 0. ( TOP-REAL (n + 1)));

      then (( TOP-REAL n),( TPlane (p,q))) are_homeomorphic by Th29;

      hence thesis by Th12;

    end;

    begin

    definition

      let n;

      :: MFOLD_2:def4

      func TUnitSphere (n) -> TopSpace equals ( Tunit_circle (n + 1));

      correctness ;

    end

    registration

      let n;

      cluster ( TUnitSphere n) -> non empty;

      correctness ;

    end

    definition

      let n, p;

      let S be SubSpace of ( TOP-REAL n);

      assume

       A1: p in ( Sphere (( 0. ( TOP-REAL n)),1));

      :: MFOLD_2:def5

      func stereographic_projection (S,p) -> Function of S, ( TPlane (p,( 0. ( TOP-REAL n)))) means

      : Def5: for q st q in S holds (it . q) = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p)));

      existence

      proof

        set T = ( TPlane (p,( 0. ( TOP-REAL n))));

        defpred P[ object, object] means for q be Point of ( TOP-REAL n) st q = $1 & q in S holds $2 = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p)));

        

         A2: for x be object st x in ( [#] S) holds ex y be object st y in ( [#] T) & P[x, y]

        proof

          let x be object;

          assume

           A3: x in ( [#] S);

          ( [#] S) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider q = x as Point of ( TOP-REAL n) by A3;

          set y = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p)));

          take y;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          reconsider p1 = p as Point of ( TOP-REAL n1);

           |.(p1 - ( 0. ( TOP-REAL n1))).| = 1 by A1, TOPREAL9: 9;

          then |.(p1 + (( - 1) * ( 0. ( TOP-REAL n1)))).| = 1 by RLVECT_1: 16;

          then |.(p1 + ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 10;

          then |.p.| = 1 by RLVECT_1: 4;

          then |(p, p)| = (1 ^2 ) by EUCLID_2: 4;

          then

           A4: |(p, p)| = (1 * 1) by SQUARE_1:def 1;

          

           A5: |(p, ( |(q, p)| * p))| = ( |(q, p)| * |(p, p)|) by EUCLID_2: 20

          .= |(p, q)| by A4;

           |(p, y)| = ((1 / (1 - |(q, p)|)) * |(p, (q - ( |(q, p)| * p)))|) by EUCLID_2: 20

          .= ((1 / (1 - |(q, p)|)) * ( |(p, q)| - |(p, ( |(q, p)| * p))|)) by EUCLID_2: 27

          .= 0 by A5;

          then |(p, (y + ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 4;

          then |(p, (y + (( - 1) * ( 0. ( TOP-REAL n)))))| = 0 by RLVECT_1: 10;

          then |(p, (y - ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 16;

          then y in ( Plane (p,( 0. ( TOP-REAL n))));

          hence y in ( [#] T) by PRE_TOPC:def 5;

          thus P[x, y];

        end;

        consider f be Function of ( [#] S), ( [#] T) such that

         A6: for x be object st x in ( [#] S) holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

        reconsider f as Function of S, T;

        take f;

        let q be Point of ( TOP-REAL n);

        assume

         A7: q in S;

        thus thesis by A6, A7;

      end;

      uniqueness

      proof

        let f1,f2 be Function of S, ( TPlane (p,( 0. ( TOP-REAL n)))) such that

         A8: for q be Point of ( TOP-REAL n) st q in S holds (f1 . q) = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p))) and

         A9: for q be Point of ( TOP-REAL n) st q in S holds (f2 . q) = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p)));

        for x be object st x in ( [#] S) holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A10: x in ( [#] S);

          ( [#] S) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider q = x as Point of ( TOP-REAL n) by A10;

          

           A11: q in S by A10;

          

          thus (f1 . x) = ((1 / (1 - |(q, p)|)) * (q - ( |(q, p)| * p))) by A11, A8

          .= (f2 . x) by A11, A9;

        end;

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    theorem :: MFOLD_2:31

    

     Th31: for S be SubSpace of ( TOP-REAL n) st ( [#] S) = (( Sphere (( 0. ( TOP-REAL n)),1)) \ {p}) & p in ( Sphere (( 0. ( TOP-REAL n)),1)) holds ( stereographic_projection (S,p)) is being_homeomorphism

    proof

      let S be SubSpace of ( TOP-REAL n);

      assume

       A1: ( [#] S) = (( Sphere (( 0. ( TOP-REAL n)),1)) \ {p});

      assume

       A2: p in ( Sphere (( 0. ( TOP-REAL n)),1));

      set f = ( stereographic_projection (S,p));

      set T = ( TPlane (p,( 0. ( TOP-REAL n))));

      

       A3: ( dom f) = ( [#] S) by FUNCT_2:def 1;

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      reconsider p1 = p as Point of ( TOP-REAL n1);

       |.(p1 - ( 0. ( TOP-REAL n1))).| = 1 by A2, TOPREAL9: 9;

      then |.(p1 + (( - 1) * ( 0. ( TOP-REAL n1)))).| = 1 by RLVECT_1: 16;

      then |.(p1 + ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 10;

      then

       A4: |.p.| = 1 by RLVECT_1: 4;

      then |(p, p)| = (1 ^2 ) by EUCLID_2: 4;

      then

       A5: |(p, p)| = (1 * 1) by SQUARE_1:def 1;

      defpred P[ object, object] means for q be Point of ( TOP-REAL n) st q = $1 & q in T holds $2 = ((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p)));

      

       A6: for x be object st x in ( [#] T) holds ex y be object st y in ( [#] S) & P[x, y]

      proof

        let x be object;

        assume

         A7: x in ( [#] T);

        ( [#] T) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        then

        reconsider q = x as Point of ( TOP-REAL n) by A7;

        set y = ((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p)));

        take y;

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        reconsider p1 = p as Point of ( TOP-REAL n1);

        q in ( Plane (p,( 0. ( TOP-REAL n)))) by A7, PRE_TOPC:def 5;

        then

        consider x1 be Point of ( TOP-REAL n) such that

         A8: x1 = q & |(p, (x1 - ( 0. ( TOP-REAL n))))| = 0 ;

         |(p, (q + (( - 1) * ( 0. ( TOP-REAL n)))))| = 0 by A8, RLVECT_1: 16;

        then |(p, (q + ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 10;

        then

         A9: |(p, q)| = 0 by RLVECT_1: 4;

        

         A10: |(q, q)| >= 0 by EUCLID_2: 35;

        

         A11: not y in {p}

        proof

          assume

           A12: y in {p};

          

           A13: |(((2 * q) + (( |(q, q)| - 1) * p)), p)| = ((2 * |(q, p)|) + (( |(q, q)| - 1) * |(p, p)|)) by EUCLID_2: 25

          .= (( |(q, q)| - 1) * |(p, p)|) by A9;

           |(((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p))), p)| = ((1 / ( |(q, q)| + 1)) * |(((2 * q) + (( |(q, q)| - 1) * p)), p)|) by EUCLID_2: 19

          .= (((1 / ( |(q, q)| + 1)) * ( |(q, q)| - 1)) * |(p, p)|) by A13;

          

          then (( |(q, q)| + 1) * 1) = (( |(q, q)| + 1) * ((1 / ( |(q, q)| + 1)) * ( |(q, q)| - 1))) by A5, A12, TARSKI:def 1

          .= ((( |(q, q)| + 1) * (1 / ( |(q, q)| + 1))) * ( |(q, q)| - 1))

          .= ((( |(q, q)| + 1) / ( |(q, q)| + 1)) * ( |(q, q)| - 1)) by XCMPLX_1: 99

          .= (1 * ( |(q, q)| - 1)) by A10, XCMPLX_1: 60;

          hence contradiction;

        end;

        reconsider y1 = y as Point of ( TOP-REAL n1);

        

         A14: |(q, ((2 * q) + (( |(q, q)| - 1) * p)))| = ((2 * |(q, q)|) + (( |(q, q)| - 1) * |(p, q)|)) by EUCLID_2: 25

        .= (2 * |(q, q)|) by A9;

        

         A15: |(p, ((2 * q) + (( |(q, q)| - 1) * p)))| = ((2 * |(q, p)|) + (( |(q, q)| - 1) * |(p, p)|)) by EUCLID_2: 25

        .= ( |(q, q)| - 1) by A5, A9;

        

         A16: |(((2 * q) + (( |(q, q)| - 1) * p)), ((2 * q) + (( |(q, q)| - 1) * p)))| = ((2 * (2 * |(q, q)|)) + (( |(q, q)| - 1) * |(p, ((2 * q) + (( |(q, q)| - 1) * p)))|)) by A14, EUCLID_2: 25

        .= (( |(q, q)| + 1) * ( |(q, q)| + 1)) by A15;

        

         A17: |(((2 * q) + (( |(q, q)| - 1) * p)), ((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p))))| = ((1 / ( |(q, q)| + 1)) * |(((2 * q) + (( |(q, q)| - 1) * p)), ((2 * q) + (( |(q, q)| - 1) * p)))|) by EUCLID_2: 20;

         |(((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p))), ((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p))))| = ((1 / ( |(q, q)| + 1)) * |(((2 * q) + (( |(q, q)| - 1) * p)), ((1 / ( |(q, q)| + 1)) * ((2 * q) + (( |(q, q)| - 1) * p))))|) by EUCLID_2: 19

        .= (((1 / ( |(q, q)| + 1)) * ((1 / ( |(q, q)| + 1)) * ( |(q, q)| + 1))) * ( |(q, q)| + 1)) by A16, A17

        .= (((1 / ( |(q, q)| + 1)) * (( |(q, q)| + 1) / ( |(q, q)| + 1))) * ( |(q, q)| + 1)) by XCMPLX_1: 99

        .= (((1 / ( |(q, q)| + 1)) * 1) * ( |(q, q)| + 1)) by A10, XCMPLX_1: 60

        .= (( |(q, q)| + 1) / ( |(q, q)| + 1)) by XCMPLX_1: 99

        .= 1 by A10, XCMPLX_1: 60;

        then |.y.| = 1 by EUCLID_2: 5, SQUARE_1: 18;

        then |.(y + ( 0. ( TOP-REAL n))).| = 1 by RLVECT_1: 4;

        then |.(y + (( - 1) * ( 0. ( TOP-REAL n)))).| = 1 by RLVECT_1: 10;

        then |.(y - ( 0. ( TOP-REAL n))).| = 1 by RLVECT_1: 16;

        then y1 in ( Sphere (( 0. ( TOP-REAL n)),1)) by TOPREAL9: 9;

        hence y in ( [#] S) by A1, A11, XBOOLE_0:def 5;

        thus P[x, y];

      end;

      consider g1 be Function of ( [#] T), ( [#] S) such that

       A18: for x be object st x in ( [#] T) holds P[x, (g1 . x)] from FUNCT_2:sch 1( A6);

      reconsider g = g1 as Function of T, S;

      reconsider f1 = f as Function of ( [#] S), ( [#] T);

       |.( 0. ( TOP-REAL n)).| <> |.p.| by A4, EUCLID_2: 39;

      then ( 0. ( TOP-REAL n)) <> ((1 + 1) * p) by RLVECT_1: 11;

      then ( 0. ( TOP-REAL n)) <> ((1 * p) + (1 * p)) by RLVECT_1:def 6;

      then ( 0. ( TOP-REAL n)) <> ((1 * p) + p) by RLVECT_1:def 8;

      then ( 0. ( TOP-REAL n)) <> (p + p) by RLVECT_1:def 8;

      then (p + ( - p)) <> (p + p) by RLVECT_1: 5;

      then

       A19: not ( - p) in {p} by TARSKI:def 1;

       |.( - p).| = 1 by A4, EUCLID: 71;

      then |.(( - p) + ( 0. ( TOP-REAL n))).| = 1 by RLVECT_1: 4;

      then |.(( - p) + (( - 1) * ( 0. ( TOP-REAL n)))).| = 1 by RLVECT_1: 10;

      then |.(( - p) - ( 0. ( TOP-REAL n))).| = 1 by RLVECT_1: 16;

      then

       A20: ( - p) in ( Sphere (( 0. ( TOP-REAL n1)),1)) by TOPREAL9: 9;

      then

       A21: ( [#] S) <> {} by A1, A19, XBOOLE_0:def 5;

      

       A22: for y,x be object holds y in ( [#] T) & (g1 . y) = x iff x in ( [#] S) & (f1 . x) = y

      proof

        let y,x be object;

        hereby

          assume

           A23: y in ( [#] T);

          assume

           A24: (g1 . y) = x;

          hence

           A25: x in ( [#] S) by A23, A21, FUNCT_2: 5;

          ( [#] S) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider qx = x as Point of ( TOP-REAL n) by A25;

          ( [#] T) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider qy = y as Point of ( TOP-REAL n) by A23;

          qy in T by A23;

          then

           A26: qx = ((1 / ( |(qy, qy)| + 1)) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by A18, A24;

          qx in S by A24, A23, A21, FUNCT_2: 5;

          then

           A27: (f . qx) = ((1 / (1 - |(qx, p)|)) * (qx - ( |(qx, p)| * p))) by A2, Def5;

          qy in ( Plane (p,( 0. ( TOP-REAL n)))) by A23, PRE_TOPC:def 5;

          then

          consider y1 be Point of ( TOP-REAL n) such that

           A28: y1 = qy & |(p, (y1 - ( 0. ( TOP-REAL n))))| = 0 ;

           |(p, (qy + (( - 1) * ( 0. ( TOP-REAL n)))))| = 0 by A28, RLVECT_1: 16;

          then |(p, (qy + ( 0. ( TOP-REAL n))))| = 0 by RLVECT_1: 10;

          then

           A29: |(p, qy)| = 0 by RLVECT_1: 4;

          

           A30: |(((2 * qy) + (( |(qy, qy)| - 1) * p)), p)| = ((2 * |(qy, p)|) + (( |(qy, qy)| - 1) * |(p, p)|)) by EUCLID_2: 25

          .= ( |(qy, qy)| - 1) by A5, A29;

          

           A31: |(qx, p)| = ((1 / ( |(qy, qy)| + 1)) * |(((2 * qy) + (( |(qy, qy)| - 1) * p)), p)|) by A26, EUCLID_2: 19

          .= ((( |(qy, qy)| - 1) / ( |(qy, qy)| + 1)) * 1) by A30, XCMPLX_1: 75;

          

           A32: |(qy, qy)| >= 0 by EUCLID_2: 35;

          

           A33: (1 - |(qx, p)|) = ((( |(qy, qy)| + 1) / ( |(qy, qy)| + 1)) - (( |(qy, qy)| - 1) / ( |(qy, qy)| + 1))) by A31, A32, XCMPLX_1: 60

          .= ((( |(qy, qy)| + 1) - ( |(qy, qy)| - 1)) / ( |(qy, qy)| + 1)) by XCMPLX_1: 120

          .= (2 / ( |(qy, qy)| + 1));

          

           A34: (1 / (1 - |(qx, p)|)) = (( |(qy, qy)| + 1) / 2) by A33, XCMPLX_1: 57;

          

           A35: ((( |(qy, qy)| + 1) / 2) * qx) = (((( |(qy, qy)| + 1) / 2) * (1 / ( |(qy, qy)| + 1))) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by A26, RLVECT_1:def 7

          .= (((( |(qy, qy)| + 1) * 1) / (2 * ( |(qy, qy)| + 1))) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by XCMPLX_1: 76

          .= (((( |(qy, qy)| + 1) / ( |(qy, qy)| + 1)) * (1 / 2)) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by XCMPLX_1: 76

          .= ((1 * (1 / 2)) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by A32, XCMPLX_1: 60

          .= (((1 / 2) * (2 * qy)) + ((1 / 2) * (( |(qy, qy)| - 1) * p))) by RLVECT_1:def 5

          .= ((((1 / 2) * 2) * qy) + ((1 / 2) * (( |(qy, qy)| - 1) * p))) by RLVECT_1:def 7

          .= ((1 * qy) + (((1 / 2) * ( |(qy, qy)| - 1)) * p)) by RLVECT_1:def 7

          .= (qy + ((( |(qy, qy)| - 1) / 2) * p)) by RLVECT_1:def 8;

          

           A36: ((( |(qy, qy)| + 1) / 2) * |(qx, p)|) = ((( |(qy, qy)| + 1) / ( |(qy, qy)| + 1)) * (( |(qy, qy)| - 1) / 2)) by A31, XCMPLX_1: 85

          .= (1 * (( |(qy, qy)| - 1) / 2)) by A32, XCMPLX_1: 60

          .= (( |(qy, qy)| - 1) / 2);

          

          thus (f1 . x) = (((( |(qy, qy)| + 1) / 2) * qx) - ((( |(qy, qy)| + 1) / 2) * ( |(qx, p)| * p))) by A27, A34, RLVECT_1: 34

          .= (((( |(qy, qy)| + 1) / 2) * qx) - ((( |(qy, qy)| - 1) / 2) * p)) by A36, RLVECT_1:def 7

          .= y by A35, RLVECT_4: 1;

        end;

        assume

         A37: x in ( [#] S);

        assume

         A38: (f1 . x) = y;

        hence y in ( [#] T) by A37, FUNCT_2: 5;

        ( [#] S) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        then

        reconsider qx = x as Point of ( TOP-REAL n) by A37;

        qx in S by A37;

        then

         A40: y = ((1 / (1 - |(qx, p)|)) * (qx - ( |(qx, p)| * p))) by A38, A2, Def5;

        then

        reconsider qy = y as Point of ( TOP-REAL n);

        

         A41: qy in T by A38, A37, FUNCT_2: 5;

        

         A42: (g1 . qy) = ((1 / ( |(qy, qy)| + 1)) * ((2 * qy) + (( |(qy, qy)| - 1) * p))) by A41, A18;

        reconsider qx1 = qx as Point of ( TOP-REAL n1);

        qx1 in ( Sphere (( 0. ( TOP-REAL n)),1)) by A37, A1, XBOOLE_0:def 5;

        then |.(qx1 - ( 0. ( TOP-REAL n1))).| = 1 by TOPREAL9: 9;

        then |.(qx1 + (( - 1) * ( 0. ( TOP-REAL n1)))).| = 1 by RLVECT_1: 16;

        then |.(qx1 + ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 10;

        then |.qx.| = 1 by RLVECT_1: 4;

        then |(qx, qx)| = (1 ^2 ) by EUCLID_2: 4;

        then

         A43: |(qx, qx)| = (1 * 1) by SQUARE_1:def 1;

        

         A44: |(( |(qx, p)| * p), (qx - ( |(qx, p)| * p)))| = ( |(( |(qx, p)| * p), qx)| - |(( |(qx, p)| * p), ( |(qx, p)| * p))|) by EUCLID_2: 27

        .= (( |(qx, p)| * |(qx, p)|) - |(( |(qx, p)| * p), ( |(qx, p)| * p))|) by EUCLID_2: 19

        .= (( |(qx, p)| * |(qx, p)|) - ( |(qx, p)| * |(p, ( |(qx, p)| * p))|)) by EUCLID_2: 19

        .= (( |(qx, p)| * |(qx, p)|) - ( |(qx, p)| * ( |(qx, p)| * |(p, p)|))) by EUCLID_2: 20

        .= 0 by A5;

        

         A45: |(qx, (qx - ( |(qx, p)| * p)))| = ( |(qx, qx)| - |(qx, ( |(qx, p)| * p))|) by EUCLID_2: 24

        .= (1 - ( |(qx, p)| * |(qx, p)|)) by A43, EUCLID_2: 20;

        

         A46: |((qx - ( |(qx, p)| * p)), (qx - ( |(qx, p)| * p)))| = ( |(qx, (qx - ( |(qx, p)| * p)))| - |(( |(qx, p)| * p), (qx - ( |(qx, p)| * p)))|) by EUCLID_2: 24

        .= ((1 - ( |(qx, p)| * |(qx, p)|)) + 0 ) by A45, A44;

         |(qx, p)| <> 1

        proof

          assume

           A47: |(qx, p)| = 1;

          

           A48: not qx in {p} by A1, A37, XBOOLE_0:def 5;

          ( |(qx, p)| - |(qx, qx)|) = 0 by A43, A47;

          then

           A49: |(qx, (p - qx))| = 0 by EUCLID_2: 27;

          ( |(p, p)| - |(qx, p)|) = 0 by A5, A47;

          then

           A50: |((p - qx), p)| = 0 by EUCLID_2: 24;

           |((p - qx), (p - qx))| = ( 0 - 0 ) by A49, A50, EUCLID_2: 24;

          then (p - qx) = ( 0. ( TOP-REAL n)) by EUCLID_2: 41;

          then p = qx by RLVECT_1: 21;

          hence contradiction by A48, TARSKI:def 1;

        end;

        then

         A51: (1 - |(qx, p)|) <> 0 ;

        then

         A52: ((1 - |(qx, p)|) * (1 - |(qx, p)|)) <> 0 ;

        

         A53: |(qy, qy)| = ((1 / (1 - |(qx, p)|)) * |((qx - ( |(qx, p)| * p)), qy)|) by A40, EUCLID_2: 19

        .= ((1 / (1 - |(qx, p)|)) * ((1 / (1 - |(qx, p)|)) * |((qx - ( |(qx, p)| * p)), (qx - ( |(qx, p)| * p)))|)) by A40, EUCLID_2: 19

        .= (((1 / (1 - |(qx, p)|)) * (1 / (1 - |(qx, p)|))) * (1 - ( |(qx, p)| * |(qx, p)|))) by A46

        .= ((1 / ((1 - |(qx, p)|) * (1 - |(qx, p)|))) * (1 - ( |(qx, p)| * |(qx, p)|))) by XCMPLX_1: 102

        .= ((1 - ( |(qx, p)| * |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) by XCMPLX_1: 99;

        

         A54: ( |(qy, qy)| + 1) = (((1 - ( |(qx, p)| * |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) + (((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|)))) by A53, A52, XCMPLX_1: 60

        .= (((1 - ( |(qx, p)| * |(qx, p)|)) + ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) by XCMPLX_1: 62

        .= ((2 * (1 - |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|)))

        .= (2 * ((1 - |(qx, p)|) / ((1 - |(qx, p)|) * (1 - |(qx, p)|)))) by XCMPLX_1: 74

        .= (2 * (((1 - |(qx, p)|) / (1 - |(qx, p)|)) / (1 - |(qx, p)|))) by XCMPLX_1: 78

        .= (2 * (1 / (1 - |(qx, p)|))) by A51, XCMPLX_1: 60

        .= ((2 * 1) / (1 - |(qx, p)|)) by XCMPLX_1: 74;

        

         A55: ( |(qy, qy)| - 1) = (((1 - ( |(qx, p)| * |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) - (((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|)) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|)))) by A53, A52, XCMPLX_1: 60

        .= (((1 - ( |(qx, p)| * |(qx, p)|)) - ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) / ((1 - (2 * |(qx, p)|)) + ( |(qx, p)| * |(qx, p)|))) by XCMPLX_1: 120

        .= (((2 * |(qx, p)|) * (1 - |(qx, p)|)) / ((1 - |(qx, p)|) * (1 - |(qx, p)|)))

        .= ((2 * |(qx, p)|) * ((1 - |(qx, p)|) / ((1 - |(qx, p)|) * (1 - |(qx, p)|)))) by XCMPLX_1: 74

        .= ((2 * |(qx, p)|) * (((1 - |(qx, p)|) / (1 - |(qx, p)|)) / (1 - |(qx, p)|))) by XCMPLX_1: 78

        .= ((2 * |(qx, p)|) * (1 / (1 - |(qx, p)|))) by A51, XCMPLX_1: 60

        .= (((2 * |(qx, p)|) * 1) / (1 - |(qx, p)|)) by XCMPLX_1: 74;

        

         A56: (1 / ( |(qy, qy)| + 1)) = ((1 - |(qx, p)|) / 2) by A54, XCMPLX_1: 57;

        

         A57: (( |(qy, qy)| - 1) / ( |(qy, qy)| + 1)) = ((2 * |(qx, p)|) / ((1 - |(qx, p)|) * (2 / (1 - |(qx, p)|)))) by A54, A55, XCMPLX_1: 78

        .= ((2 * |(qx, p)|) / ((2 * (1 - |(qx, p)|)) / (1 - |(qx, p)|))) by XCMPLX_1: 74

        .= ((2 * |(qx, p)|) / (2 * ((1 - |(qx, p)|) / (1 - |(qx, p)|)))) by XCMPLX_1: 74

        .= ((2 * |(qx, p)|) / (2 * 1)) by A51, XCMPLX_1: 60

        .= |(qx, p)|;

        

         A58: ((1 - |(qx, p)|) * qy) = (((1 - |(qx, p)|) * (1 / (1 - |(qx, p)|))) * (qx - ( |(qx, p)| * p))) by A40, RLVECT_1:def 7

        .= ((((1 - |(qx, p)|) * 1) / (1 - |(qx, p)|)) * (qx - ( |(qx, p)| * p))) by XCMPLX_1: 74

        .= (1 * (qx - ( |(qx, p)| * p))) by A51, XCMPLX_1: 60

        .= (qx - ( |(qx, p)| * p)) by RLVECT_1:def 8;

        

        thus (g1 . y) = (((1 / ( |(qy, qy)| + 1)) * (2 * qy)) + ((1 / ( |(qy, qy)| + 1)) * (( |(qy, qy)| - 1) * p))) by A42, RLVECT_1:def 5

        .= ((((1 / ( |(qy, qy)| + 1)) * 2) * qy) + ((1 / ( |(qy, qy)| + 1)) * (( |(qy, qy)| - 1) * p))) by RLVECT_1:def 7

        .= ((((1 / ( |(qy, qy)| + 1)) * 2) * qy) + (((1 / ( |(qy, qy)| + 1)) * ( |(qy, qy)| - 1)) * p)) by RLVECT_1:def 7

        .= (((1 - |(qx, p)|) * qy) + (((1 * ( |(qy, qy)| - 1)) / ( |(qy, qy)| + 1)) * p)) by A56, XCMPLX_1: 74

        .= (qx - (( |(qx, p)| * p) - ( |(qx, p)| * p))) by A57, A58, RLVECT_1: 29

        .= (qx - ( 0. ( TOP-REAL n))) by RLVECT_1: 5

        .= (qx + (( - 1) * ( 0. ( TOP-REAL n)))) by RLVECT_1: 16

        .= (qx + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

        .= x by RLVECT_1: 4;

      end;

      for y be object holds y in ( [#] T) iff ex x be object st x in ( dom f) & y = (f . x)

      proof

        let y be object;

        hereby

          assume

           A59: y in ( [#] T);

          reconsider x = (g . y) as object;

          take x;

          thus x in ( dom f) by A22, A3, A59;

          thus y = (f . x) by A59, A22;

        end;

        given x be object such that

         A60: x in ( dom f) & y = (f . x);

        thus y in ( [#] T) by A60, FUNCT_2: 5;

      end;

      then

       A61: ( rng f) = ( [#] T) by FUNCT_1:def 3;

      

       A62: f is one-to-one

      proof

        let x1,x2 be object;

        assume

         A63: x1 in ( dom f) & x2 in ( dom f);

        assume

         A64: (f . x1) = (f . x2);

        (g1 . (f . x1)) = x1 & (g1 . (f . x2)) = x2 by A63, A22;

        hence x1 = x2 by A64;

      end;

      

       A65: f is continuous

      proof

        

         A66: ( [#] S) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        set f0 = ( InnerProduct p);

        consider f1 be Function of ( TOP-REAL n1), R^1 such that

         A67: (for q be Point of ( TOP-REAL n) holds (f1 . q) = 1) & f1 is continuous by JGRAPH_2: 20;

        consider f2 be Function of ( TOP-REAL n), R^1 such that

         A68: (for q be Point of ( TOP-REAL n), r1,r2 be Real st (f1 . q) = r1 & (f0 . q) = r2 holds (f2 . q) = (r1 - r2)) & f2 is continuous by A67, JGRAPH_2: 21;

        reconsider f2 as continuous Function of ( TOP-REAL n), R^1 by A68;

        reconsider S1 = S as non empty TopSpace by A20, A1, A19, XBOOLE_0:def 5;

        set f3 = (f2 | S1);

        

         A69: for q be Point of ( TOP-REAL n) st q in S1 holds (f3 . q) = (1 - |(q, p)|)

        proof

          let q be Point of ( TOP-REAL n);

          assume

           B70: q in S1;

          

           A71: ( [#] S1) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          (f0 . q) = |(q, p)| & (f1 . q) = 1 by Def1, A67;

          then

           A72: (f2 . q) = (1 - |(q, p)|) by A68;

          

          thus (f3 . q) = ((f2 | the carrier of S1) . q) by A71, TMAP_1:def 3

          .= (1 - |(q, p)|) by A72, B70, FUNCT_1: 49;

        end;

        

         A73: for q be Point of S1 holds (f3 . q) <> 0

        proof

          let q be Point of S1;

          reconsider qx = q as Point of ( TOP-REAL n) by A66;

          reconsider qx1 = qx as Point of ( TOP-REAL n1);

          qx1 in ( Sphere (( 0. ( TOP-REAL n)),1)) by A1, XBOOLE_0:def 5;

          then |.(qx1 - ( 0. ( TOP-REAL n1))).| = 1 by TOPREAL9: 9;

          then |.(qx1 + (( - 1) * ( 0. ( TOP-REAL n1)))).| = 1 by RLVECT_1: 16;

          then |.(qx1 + ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 10;

          then |.qx.| = 1 by RLVECT_1: 4;

          then |(qx, qx)| = (1 ^2 ) by EUCLID_2: 4;

          then

           A74: |(qx, qx)| = (1 * 1) by SQUARE_1:def 1;

           |(qx, p)| <> 1

          proof

            assume

             A75: |(qx, p)| = 1;

            

             A76: not qx in {p} by A1, XBOOLE_0:def 5;

            ( |(qx, p)| - |(qx, qx)|) = 0 by A74, A75;

            then

             A77: |(qx, (p - qx))| = 0 by EUCLID_2: 27;

            ( |(p, p)| - |(qx, p)|) = 0 by A5, A75;

            then

             A78: |((p - qx), p)| = 0 by EUCLID_2: 24;

             |((p - qx), (p - qx))| = ( 0 - 0 ) by A77, A78, EUCLID_2: 24;

            then (p - qx) = ( 0. ( TOP-REAL n)) by EUCLID_2: 41;

            then p = qx by RLVECT_1: 21;

            hence contradiction by A76, TARSKI:def 1;

          end;

          then

           A79: (1 - |(qx, p)|) <> 0 ;

          qx in S1;

          hence thesis by A69, A79;

        end;

        then

        consider f4 be Function of S1, R^1 such that

         A80: (for q be Point of S1, r1 be Real st (f3 . q) = r1 holds (f4 . q) = (1 / r1)) & f4 is continuous by JGRAPH_2: 26;

        consider f5 be Function of S1, ( TOP-REAL n1) such that

         A81: (for a be Point of S1, b be Point of ( TOP-REAL n), r be Real st a = b & (f4 . a) = r holds (f5 . b) = (r * b)) & f5 is continuous by A80, MFOLD_1: 2;

        set f6 = (f0 | S1);

        

         A82: for q be Point of ( TOP-REAL n) st q in S1 holds (f6 . q) = |(q, p)|

        proof

          let q be Point of ( TOP-REAL n);

          assume

           B83: q in S1;

          

           A84: ( [#] S1) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          

           A85: (f0 . q) = |(q, p)| by Def1;

          

          thus (f6 . q) = ((f0 | the carrier of S1) . q) by A84, TMAP_1:def 3

          .= |(q, p)| by A85, B83, FUNCT_1: 49;

        end;

        consider f7 be Function of S1, R^1 such that

         A86: (for q be Point of S1, r1,r2 be Real st (f6 . q) = r1 & (f3 . q) = r2 holds (f7 . q) = (r1 / r2)) & f7 is continuous by A73, JGRAPH_2: 27;

        reconsider p1 = ( - p) as Point of ( TOP-REAL n1);

        consider f8 be Function of S1, ( TOP-REAL n1) such that

         A87: (for r be Point of S1 holds (f8 . r) = ((f7 . r) * p1)) & f8 is continuous by A86, JGRAPH_6: 9;

        consider f9 be Function of S, ( TOP-REAL n) such that

         A88: (for r be Point of S1 holds (f9 . r) = ((f5 . r) + (f8 . r))) & f9 is continuous by A87, A81, JGRAPH_6: 12;

        

         A89: ( dom f) = ( [#] S) by FUNCT_2:def 1

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

        for x be object st x in ( dom f) holds (f . x) = (f9 . x)

        proof

          let x be object;

          assume

           A90: x in ( dom f);

          then

          reconsider qx = x as Point of ( TOP-REAL n) by A66;

          

           A91: qx in S by A90;

          reconsider r = qx as Point of S1 by A90;

          

           A92: (f3 . r) = (1 - |(qx, p)|) by A69, A91;

          

           A93: (f4 . r) = (1 / (1 - |(qx, p)|)) by A92, A80;

          

           A94: (f6 . r) = |(qx, p)| by A82, A91;

          

           A95: (f8 . r) = ((f7 . r) * ( - p)) by A87

          .= (( |(qx, p)| / (1 - |(qx, p)|)) * ( - p)) by A92, A94, A86;

          (f9 . x) = ((f5 . r) + (f8 . r)) by A88

          .= (((1 / (1 - |(qx, p)|)) * qx) + (((1 * |(qx, p)|) / (1 - |(qx, p)|)) * ( - p))) by A93, A81, A95

          .= (((1 / (1 - |(qx, p)|)) * qx) + (((1 / (1 - |(qx, p)|)) * |(qx, p)|) * ( - p))) by XCMPLX_1: 74

          .= (((1 / (1 - |(qx, p)|)) * qx) + ((1 / (1 - |(qx, p)|)) * ( |(qx, p)| * ( - p)))) by RLVECT_1:def 7

          .= ((1 / (1 - |(qx, p)|)) * (qx + ( |(qx, p)| * ( - p)))) by RLVECT_1:def 5

          .= ((1 / (1 - |(qx, p)|)) * (qx - ( |(qx, p)| * p))) by RLVECT_1: 25;

          hence (f . x) = (f9 . x) by A91, A2, Def5;

        end;

        hence thesis by A88, A89, FUNCT_1: 2, PRE_TOPC: 27;

      end;

      

       A96: g is continuous

      proof

        consider g0 be Function of ( TOP-REAL n1), R^1 such that

         A98: (for q be Point of ( TOP-REAL n1) holds (g0 . q) = |.q.|) & g0 is continuous by JORDAN2C: 84;

        consider g1 be Function of ( TOP-REAL n), R^1 such that

         A99: (for q be Point of ( TOP-REAL n), r1 be Real st (g0 . q) = r1 holds (g1 . q) = (r1 * r1)) & g1 is continuous by A98, JGRAPH_2: 22;

        consider g2 be Function of ( TOP-REAL n), R^1 such that

         A100: (for q be Point of ( TOP-REAL n), r1 be Real st (g1 . q) = r1 holds (g2 . q) = (r1 + 1)) & g2 is continuous by A99, JGRAPH_2: 24;

        consider g3 be Function of ( TOP-REAL n), R^1 such that

         A101: (for q be Point of ( TOP-REAL n), r1 be Real st (g1 . q) = r1 holds (g3 . q) = (r1 + ( - 1))) & g3 is continuous by A99, JGRAPH_2: 24;

        consider g4 be Function of ( TOP-REAL n), R^1 such that

         A102: (for q be Point of ( TOP-REAL n) holds (g4 . q) = 2) & g4 is continuous by JGRAPH_2: 20;

        

         A103: for q be Point of ( TOP-REAL n) holds (g2 . q) <> 0

        proof

          let q be Point of ( TOP-REAL n);

          (g0 . q) = |.q.| by A98;

          then (g1 . q) = ( |.q.| * |.q.|) by A99;

          then (g2 . q) = (( |.q.| * |.q.|) + 1) by A100;

          hence (g2 . q) <> 0 ;

        end;

        then

        consider g5 be Function of ( TOP-REAL n), R^1 such that

         A104: (for q be Point of ( TOP-REAL n), r1,r2 be Real st (g4 . q) = r1 & (g2 . q) = r2 holds (g5 . q) = (r1 / r2)) & g5 is continuous by A102, A100, JGRAPH_2: 27;

        reconsider g6 = (g5 | T) as continuous Function of T, R^1 by A104;

        consider g7 be Function of T, ( TOP-REAL n1) such that

         A105: (for a be Point of T, b be Point of ( TOP-REAL n), r be Real st a = b & (g6 . a) = r holds (g7 . b) = (r * b)) & g7 is continuous by MFOLD_1: 2;

        consider g8 be Function of ( TOP-REAL n), R^1 such that

         A106: (for q be Point of ( TOP-REAL n), r1,r2 be Real st (g3 . q) = r1 & (g2 . q) = r2 holds (g8 . q) = (r1 / r2)) & g8 is continuous by A103, A100, A101, JGRAPH_2: 27;

        reconsider p1 = p as Point of ( TOP-REAL n1);

        reconsider g9 = (g8 | T) as continuous Function of T, R^1 by A106;

        consider g10 be Function of T, ( TOP-REAL n1) such that

         A107: (for r be Point of T holds (g10 . r) = ((g9 . r) * p1)) & g10 is continuous by JGRAPH_6: 9;

        consider g11 be Function of T, ( TOP-REAL n1) such that

         A108: (for r be Point of T holds (g11 . r) = ((g7 . r) + (g10 . r))) & g11 is continuous by A105, A107, JGRAPH_6: 12;

        

         A109: ( dom g) = ( [#] T) by A21, FUNCT_2:def 1

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

        for x be object st x in ( dom g) holds (g . x) = (g11 . x)

        proof

          let x be object;

          assume

           A110: x in ( dom g);

          ( [#] T) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider qx = x as Point of ( TOP-REAL n) by A110;

          

           A112: qx in T by A110;

          reconsider r = qx as Point of T by A110;

          

           A113: ( [#] T) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          

           A114: (g0 . qx) = |.qx.| by A98;

          

           A115: (g1 . qx) = ( |.qx.| * |.qx.|) by A99, A114

          .= ( |.qx.| ^2 ) by SQUARE_1:def 1

          .= |(qx, qx)| by EUCLID_2: 4;

          

           A116: (g2 . qx) = ( |(qx, qx)| + 1) by A100, A115;

          

           A117: (g4 . qx) = 2 by A102;

          

           A118: (g6 . qx) = ((g5 | the carrier of T) . qx) by A113, TMAP_1:def 3

          .= (g5 . qx) by A110, FUNCT_1: 49

          .= (2 / ( |(qx, qx)| + 1)) by A104, A117, A116;

          

           A119: (g3 . qx) = ( |(qx, qx)| + ( - 1)) by A101, A115;

          

           A120: (g9 . qx) = ((g8 | the carrier of T) . qx) by A113, TMAP_1:def 3

          .= (g8 . qx) by A110, FUNCT_1: 49

          .= (( |(qx, qx)| - 1) / ( |(qx, qx)| + 1)) by A116, A119, A106;

          

           A121: (g7 . r) = ((2 / ( |(qx, qx)| + 1)) * qx) by A105, A118;

          (g11 . x) = ((g7 . r) + (g10 . r)) by A108

          .= ((((1 * 2) / ( |(qx, qx)| + 1)) * qx) + (((1 * ( |(qx, qx)| - 1)) / ( |(qx, qx)| + 1)) * p)) by A120, A107, A121

          .= ((((1 * 2) / ( |(qx, qx)| + 1)) * qx) + (((1 / ( |(qx, qx)| + 1)) * ( |(qx, qx)| - 1)) * p)) by XCMPLX_1: 74

          .= ((((1 / ( |(qx, qx)| + 1)) * 2) * qx) + (((1 / ( |(qx, qx)| + 1)) * ( |(qx, qx)| - 1)) * p)) by XCMPLX_1: 74

          .= ((((1 / ( |(qx, qx)| + 1)) * 2) * qx) + ((1 / ( |(qx, qx)| + 1)) * (( |(qx, qx)| - 1) * p))) by RLVECT_1:def 7

          .= (((1 / ( |(qx, qx)| + 1)) * (2 * qx)) + ((1 / ( |(qx, qx)| + 1)) * (( |(qx, qx)| - 1) * p))) by RLVECT_1:def 7

          .= ((1 / ( |(qx, qx)| + 1)) * ((2 * qx) + (( |(qx, qx)| - 1) * p))) by RLVECT_1:def 5;

          hence (g . x) = (g11 . x) by A18, A112;

        end;

        hence thesis by A108, A109, FUNCT_1: 2, PRE_TOPC: 27;

      end;

      reconsider f2 = f1 as ( [#] T) -valued Relation;

      f2 is onto by A61, FUNCT_2:def 3;

      then

       A122: (f1 " ) = (f1 qua Function " ) by A62, TOPS_2:def 4;

      g1 = (f1 qua Function " ) by A61, A62, A22, A21, FUNCT_2: 28;

      hence thesis by A3, A61, A62, A65, A96, A122, TOPS_2:def 5;

    end;

    registration

      let n;

      cluster ( TUnitSphere n) -> second-countable;

      correctness ;

      cluster ( TUnitSphere n) -> without_boundaryn -locally_euclidean;

      correctness

      proof

        set M = ( TUnitSphere n);

        for p be Point of M holds ex U be a_neighborhood of p st (U,( [#] ( TOP-REAL n))) are_homeomorphic

        proof

          let p be Point of M;

          reconsider n1 = (n + 1) as Element of NAT by ORDINAL1:def 12;

          ( [#] ( Tunit_circle (n + 1))) c= ( [#] ( TOP-REAL (n + 1))) by PRE_TOPC:def 4;

          then

          reconsider p1 = p as Point of ( TOP-REAL n1);

          

           A1: |.p1.| = 1 by TOPREALB: 12;

          

           A2: |.( - p1).| = ( sqrt |(( - p1), ( - p1))|) by EUCLID_2: 37

          .= ( sqrt |(p1, p1)|) by EUCLID_2: 23

          .= 1 by A1, EUCLID_2: 37;

          then |.(( - p1) + ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 4;

          then |.(( - p1) + (( - 1) * ( 0. ( TOP-REAL n1)))).| = 1 by RLVECT_1: 10;

          then

           B3: |.(( - p1) - ( 0. ( TOP-REAL n1))).| = 1 by RLVECT_1: 16;

          then ( - p1) in ( Sphere (( 0. ( TOP-REAL n1)),1)) by TOPREAL9: 9;

          then ( - p1) in ( [#] (( TOP-REAL n1) | ( Sphere (( 0. ( TOP-REAL n1)),1)))) by PRE_TOPC:def 5;

          then ( - p1) in the carrier of ( Tcircle (( 0. ( TOP-REAL n1)),1)) by TOPREALB:def 6;

          then ( - p1) in the carrier of ( Tunit_circle n1) by TOPREALB:def 7;

          then

          reconsider A = {( - p1)} as Subset of M by ZFMISC_1: 31;

          reconsider U1 = (( [#] ( TUnitSphere n)) \ A) as Subset of M;

           |.( 0. ( TOP-REAL n1)).| <> |.( - p1).| by A2, EUCLID_2: 39;

          then ( 0. ( TOP-REAL n1)) <> ((1 + 1) * ( - p1)) by RLVECT_1: 11;

          then ( 0. ( TOP-REAL n1)) <> ((1 * ( - p1)) + (1 * ( - p1))) by RLVECT_1:def 6;

          then ( 0. ( TOP-REAL n1)) <> ((1 * ( - p1)) + ( - p1)) by RLVECT_1:def 8;

          then ( 0. ( TOP-REAL n1)) <> (( - p1) + ( - p1)) by RLVECT_1:def 8;

          then (( - p1) + ( - ( - p1))) <> (( - p1) + ( - p1)) by RLVECT_1: 5;

          then

           A4: not p1 in {( - p1)} by TARSKI:def 1;

          then p1 in U1 by XBOOLE_0:def 5;

          then

          reconsider U = U1 as a_neighborhood of p by CONNSP_2: 3, FRECHET: 4;

          take U;

          reconsider m = (n + 1) as Nat;

          

           A5: M = ( Tcircle (( 0. ( TOP-REAL m)),1)) by TOPREALB:def 7

          .= (( TOP-REAL m) | ( Sphere (( 0. ( TOP-REAL m)),1))) by TOPREALB:def 6;

          reconsider S = ( Sphere (( 0. ( TOP-REAL m)),1)) as Subset of ( TOP-REAL m);

          reconsider U11 = U1 as Subset of (( TOP-REAL m) | S) by A5;

          U1 c= ( [#] ( Tunit_circle m));

          then

           A6: U1 c= ( Sphere (( 0. ( TOP-REAL m)),1)) by A5, PRE_TOPC:def 5;

          then

          reconsider V = U11 as non empty Subset of ( TOP-REAL m) by A4, XBOOLE_0:def 5, XBOOLE_1: 1;

          (M | U) = (( TOP-REAL m) | V) by A5, A6, PRE_TOPC: 7;

          then

          reconsider U2 = (M | U) as non empty SubSpace of ( TOP-REAL m);

          reconsider p2 = ( - p1) as Point of ( TOP-REAL m);

          p2 <> ( 0. ( TOP-REAL m)) by A2, EUCLID_2: 39;

          then

           A7: (( TOP-REAL n),( TPlane (p2,( 0. ( TOP-REAL m))))) are_homeomorphic by Th29;

          

           A8: (( TOP-REAL n) | ( [#] ( TOP-REAL n))) = the TopStruct of ( TOP-REAL n) by TSEP_1: 93;

          

           A9: (( TOP-REAL n), the TopStruct of ( TOP-REAL n)) are_homeomorphic by YELLOW14: 19;

          ( [#] U2) = U by PRE_TOPC:def 5

          .= (the carrier of ( Tcircle (( 0. ( TOP-REAL m)),1)) \ {p2}) by TOPREALB:def 7

          .= (( [#] (( TOP-REAL m) | ( Sphere (( 0. ( TOP-REAL m)),1)))) \ {p2}) by TOPREALB:def 6

          .= (( Sphere (( 0. ( TOP-REAL m)),1)) \ {p2}) by PRE_TOPC:def 5;

          then ( stereographic_projection (U2,p2)) is being_homeomorphism by B3, TOPREAL9: 9, Th31;

          then (U2,( TPlane (p2,( 0. ( TOP-REAL m))))) are_homeomorphic by T_0TOPSP:def 1;

          then (( TOP-REAL n),U2) are_homeomorphic by A7, BORSUK_3: 3;

          hence (U,( [#] ( TOP-REAL n))) are_homeomorphic by A8, METRIZTS:def 1, A9, BORSUK_3: 3;

        end;

        hence thesis by MFOLD_1: 14;

      end;

      cluster ( TUnitSphere n) -> n -manifold;

      correctness ;

    end