rlaffin3.miz



    begin

    reserve x for set,

n,m,k for Nat,

r for Real,

V for RealLinearSpace,

v,u,w,t for VECTOR of V,

Av for finite Subset of V,

Affv for finite affinely-independent Subset of V;

    

     Lm1: for f be n -element real-valued FinSequence holds f is Point of ( TOP-REAL n)

    proof

      let f be n -element real-valued FinSequence;

      ( len f) = n & ( @ ( @ f)) = f by CARD_1:def 7;

      hence thesis by TOPREAL3: 46;

    end;

    theorem :: RLAFFIN3:1

    

     Th1: for f1,f2 be real-valued FinSequence, r be Real holds (( Intervals (f1,r)) ^ ( Intervals (f2,r))) = ( Intervals ((f1 ^ f2),r))

    proof

      let f1,f2 be real-valued FinSequence;

      let r be Real;

      set I1 = ( Intervals (f1,r)), I2 = ( Intervals (f2,r)), f12 = (f1 ^ f2);

      set I12 = ( Intervals (f12,r));

      

       A1: ( dom I12) = ( dom f12) by EUCLID_9:def 3;

      

       A2: ( len f12) = (( len f1) + ( len f2)) & ( len (I1 ^ I2)) = (( len I1) + ( len I2)) by FINSEQ_1: 22;

      

       A3: ( dom I1) = ( dom f1) by EUCLID_9:def 3;

      then

       A4: ( len I1) = ( len f1) by FINSEQ_3: 29;

      

       A5: ( dom I2) = ( dom f2) by EUCLID_9:def 3;

      then ( len I2) = ( len f2) by FINSEQ_3: 29;

      then

       A6: ( dom (I1 ^ I2)) = ( dom I12) by A1, A4, A2, FINSEQ_3: 29;

      now

        let i be Nat;

        assume

         A7: i in ( dom (I1 ^ I2));

        then

         A8: (I12 . i) = ].((f12 . i) - r), ((f12 . i) + r).[ by A1, A6, EUCLID_9:def 3;

        per cases by A7, FINSEQ_1: 25;

          suppose

           A9: i in ( dom I1);

          then ((I1 ^ I2) . i) = (I1 . i) & (f12 . i) = (f1 . i) by A3, FINSEQ_1:def 7;

          hence ((I1 ^ I2) . i) = (I12 . i) by A3, A8, A9, EUCLID_9:def 3;

        end;

          suppose ex j be Nat st j in ( dom I2) & i = (( len I1) + j);

          then

          consider j be Nat such that

           A10: j in ( dom I2) and

           A11: i = (( len I1) + j);

          ((I1 ^ I2) . i) = (I2 . j) & (f12 . i) = (f2 . j) by A5, A4, A10, A11, FINSEQ_1:def 7;

          hence ((I1 ^ I2) . i) = (I12 . i) by A5, A8, A10, EUCLID_9:def 3;

        end;

      end;

      hence thesis by A6, FINSEQ_1: 13;

    end;

    theorem :: RLAFFIN3:2

    

     Th2: for f1,f2 be FinSequence holds x in ( product (f1 ^ f2)) iff ex p1,p2 be FinSequence st x = (p1 ^ p2) & p1 in ( product f1) & p2 in ( product f2)

    proof

      let f1,f2 be FinSequence;

      set f12 = (f1 ^ f2);

      

       A1: ( len f12) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      ( dom f1) = ( Seg ( len f1)) by FINSEQ_1:def 3;

      then

       A2: (f12 | ( Seg ( len f1))) = f1 by FINSEQ_1: 21;

      hereby

        assume

         A3: x in ( product f12);

        then

        consider g be Function such that

         A4: x = g and

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

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

        ( dom f12) = ( Seg ( len f12)) by FINSEQ_1:def 3;

        then

        reconsider g as FinSequence by A5, FINSEQ_1:def 2;

        set p1 = (g | ( len f1));

        consider p2 be FinSequence such that

         A7: g = (p1 ^ p2) by FINSEQ_1: 80;

        take p1, p2;

        thus x = (p1 ^ p2) & p1 in ( product f1) by A2, A3, A4, A7, PRALG_3: 1;

        

         A8: ( len f12) = ( len g) by A5, FINSEQ_3: 29;

        then

         A9: ( len f1) = ( len p1) by A1, FINSEQ_1: 59, NAT_1: 11;

        ( len g) = (( len p1) + ( len p2)) by A7, FINSEQ_1: 22;

        then

         A10: ( dom f2) = ( dom p2) by A1, A8, A9, FINSEQ_3: 29;

        now

          let y be object;

          assume

           A11: y in ( dom f2);

          then

          reconsider i = y as Nat;

          (i + ( len f1)) in ( dom f12) by A11, FINSEQ_1: 28;

          then (g . (i + ( len f1))) in (f12 . (i + ( len f1))) & (f12 . (i + ( len f1))) = (f2 . i) by A6, A11, FINSEQ_1:def 7;

          hence (p2 . y) in (f2 . y) by A7, A9, A10, A11, FINSEQ_1:def 7;

        end;

        hence p2 in ( product f2) by A10, CARD_3:def 5;

      end;

      given p1,p2 be FinSequence such that

       A12: x = (p1 ^ p2) and

       A13: p1 in ( product f1) and

       A14: p2 in ( product f2);

      

       A15: ex g be Function st p2 = g & ( dom g) = ( dom f2) & for y be object st y in ( dom f2) holds (g . y) in (f2 . y) by A14, CARD_3:def 5;

      

       A16: ex g be Function st p1 = g & ( dom g) = ( dom f1) & for y be object st y in ( dom f1) holds (g . y) in (f1 . y) by A13, CARD_3:def 5;

      then

       A17: ( len p1) = ( len f1) by FINSEQ_3: 29;

       A18:

      now

        let y be object;

        assume

         A19: y in ( dom f12);

        then

        reconsider i = y as Nat;

        per cases by A19, FINSEQ_1: 25;

          suppose

           A20: i in ( dom f1);

          then (f12 . y) = (f1 . i) & ((p1 ^ p2) . y) = (p1 . i) by A16, FINSEQ_1:def 7;

          hence ((p1 ^ p2) . y) in (f12 . y) by A16, A20;

        end;

          suppose ex j be Nat st j in ( dom f2) & i = (( len f1) + j);

          then

          consider j be Nat such that

           A21: j in ( dom f2) and

           A22: i = (( len f1) + j);

          (f12 . y) = (f2 . j) & ((p1 ^ p2) . y) = (p2 . j) by A15, A17, A21, A22, FINSEQ_1:def 7;

          hence ((p1 ^ p2) . y) in (f12 . y) by A15, A21;

        end;

      end;

      ( len (p1 ^ p2)) = (( len p1) + ( len p2)) & ( len p2) = ( len f2) by A15, FINSEQ_1: 22, FINSEQ_3: 29;

      then ( dom (p1 ^ p2)) = ( dom f12) by A1, A17, FINSEQ_3: 29;

      hence thesis by A12, A18, CARD_3:def 5;

    end;

    

     Lm2: for A be Subset of V holds ( Lin A) = ( Lin (A \ {( 0. V)}))

    proof

      let A be Subset of V;

      per cases ;

        suppose not ( 0. V) in A;

        hence thesis by ZFMISC_1: 57;

      end;

        suppose

         A1: ( 0. V) in A;

         {( 0. V)} = the carrier of ( (0). V) by RLSUB_1:def 3;

        then

         A2: ( Lin {( 0. V)}) = ( (0). V) by RLVECT_3: 18;

        A = ((A \ {( 0. V)}) \/ {( 0. V)}) by A1, ZFMISC_1: 116;

        

        hence ( Lin A) = (( Lin (A \ {( 0. V)})) + ( (0). V)) by A2, RLVECT_3: 22

        .= ( Lin (A \ {( 0. V)})) by RLSUB_2: 9;

      end;

    end;

    theorem :: RLAFFIN3:3

    

     Th3: V is finite-dimensional iff ( (Omega). V) is finite-dimensional

    proof

      set O = ( (Omega). V);

      thus V is finite-dimensional implies O is finite-dimensional;

      assume O is finite-dimensional;

      then

      consider A be finite Subset of O such that

       A1: A is Basis of O by RLVECT_5:def 1;

      

       A2: the RLSStruct of V = O by RLSUB_1:def 4;

      then

      reconsider a = A as finite Subset of V;

      ( Lin A) = O by A1, RLVECT_3:def 3;

      then

       A3: ( Lin a) = O by RLVECT_5: 20;

      A is linearly-independent by A1, RLVECT_3:def 3;

      then a is linearly-independent by RLVECT_5: 14;

      then a is Basis of V by A2, A3, RLVECT_3:def 3;

      hence thesis by RLVECT_5:def 1;

    end;

    registration

      let V be finite-dimensional RealLinearSpace;

      cluster -> finite for affinely-independent Subset of V;

      coherence

      proof

        let A be affinely-independent Subset of V;

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose A is non empty;

          then

          consider v be VECTOR of V such that v in A and

           A1: ((( - v) + A) \ {( 0. V)}) is linearly-independent by RLAFFIN1:def 4;

          set vA = (( - v) + A);

          ((vA \ {( 0. V)}) \/ {( 0. V)}) = (vA \/ {( 0. V)}) by XBOOLE_1: 39;

          then

           A2: ( card vA) = ( card A) & vA c= ((vA \ {( 0. V)}) \/ {( 0. V)}) by RLAFFIN1: 7, XBOOLE_1: 7;

          (vA \ {( 0. V)}) is finite by A1, RLVECT_5: 24;

          hence thesis by A2;

        end;

      end;

    end

    registration

      let n;

      cluster ( TOP-REAL n) -> add-continuous Mult-continuous;

      coherence

      proof

        set T = ( TOP-REAL n), E = ( Euclid n), TE = ( TopSpaceMetr E);

        

         A1: the TopStruct of T = TE by EUCLID:def 8;

        thus T is add-continuous

        proof

          let x1,x2 be Point of T, V be Subset of T such that

           A2: V is open and

           A3: (x1 + x2) in V;

          reconsider X1 = x1, X2 = x2, X12 = (x1 + x2) as Point of E by A1, TOPMETR: 12;

          reconsider v = V as Subset of TE by A1;

          V in the topology of T by A2, PRE_TOPC:def 2;

          then v is open by A1, PRE_TOPC:def 2;

          then

          consider r be Real such that

           A4: r > 0 and

           A5: ( Ball (X12,r)) c= v by A3, TOPMETR: 15;

          set r2 = (r / 2);

          reconsider B1 = ( Ball (X1,r2)), B2 = ( Ball (X2,r2)) as Subset of T by A1, TOPMETR: 12;

          take B1, B2;

          thus B1 is open & B2 is open & x1 in B1 & x2 in B2 by A4, GOBOARD6: 1, GOBOARD6: 3, XREAL_1: 215;

          let x be object;

          assume x in (B1 + B2);

          then x in { (b1 + b2) where b1,b2 be Element of T : b1 in B1 & b2 in B2 } by RUSUB_4:def 9;

          then

          consider b1,b2 be Element of T such that

           A6: x = (b1 + b2) and

           A7: b1 in B1 and

           A8: b2 in B2;

          reconsider e1 = b1, e2 = b2, e12 = (b1 + b2) as Point of E by A1, TOPMETR: 12;

          reconsider y1 = x1, y2 = x2, c1 = b1, c2 = b2 as Element of ( REAL n) by EUCLID: 22;

          ( dist (X2,e2)) < r2 by A8, METRIC_1: 11;

          then

           A9: |.(y2 - c2).| < r2 by SPPOL_1: 5;

          ( dist (X1,e1)) < r2 by A7, METRIC_1: 11;

          then |.(y1 - c1).| < r2 by SPPOL_1: 5;

          then

           A10: ( |.(y1 - c1).| + |.(y2 - c2).|) < (r2 + r2) by A9, XREAL_1: 8;

          

           A11: ((y1 + y2) - (c1 + c2)) = ((y1 + y2) + ( - (c2 + c1))) by RVSUM_1: 31

          .= ((y1 + y2) + (( - c2) + ( - c1))) by RVSUM_1: 26

          .= (((y1 + y2) + ( - c2)) + ( - c1)) by RVSUM_1: 15

          .= (((y2 + ( - c2)) + y1) + ( - c1)) by RVSUM_1: 15

          .= ((y2 + ( - c2)) + (y1 + ( - c1))) by RVSUM_1: 15

          .= ((y2 - c2) + (y1 + ( - c1))) by RVSUM_1: 31

          .= ((y2 - c2) + (y1 - c1)) by RVSUM_1: 31;

          

           A12: ( dist (X12,e12)) = |.((y1 - c1) + (y2 - c2)).| by A11, SPPOL_1: 5;

           |.((y1 - c1) + (y2 - c2)).| <= ( |.(y1 - c1).| + |.(y2 - c2).|) by EUCLID: 12;

          then ( dist (X12,e12)) < r by A10, A12, XXREAL_0: 2;

          then e12 in ( Ball (X12,r)) by METRIC_1: 11;

          hence x in V by A5, A6;

        end;

        let a be Real, x be Point of T, V be Subset of T such that

         A13: V is open and

         A14: (a * x) in V;

        reconsider X = x, AX = (a * x) as Point of E by A1, TOPMETR: 12;

        reconsider v = V as Subset of TE by A1;

        V in the topology of T by A13, PRE_TOPC:def 2;

        then v is open by A1, PRE_TOPC:def 2;

        then

        consider r be Real such that

         A15: r > 0 and

         A16: ( Ball (AX,r)) c= v by A14, TOPMETR: 15;

        set r2 = (r / 2);

        

         A17: r2 > 0 by A15, XREAL_1: 215;

        then

         A18: (r2 / 2) > 0 by XREAL_1: 215;

        ex m be positive Real st ( |.a.| * m) < r2

        proof

          per cases by COMPLEX1: 46;

            suppose |.a.| = 0 ;

            then ( |.a.| * 1) < r2 by A15, XREAL_1: 215;

            hence thesis;

          end;

            suppose

             A19: |.a.| > 0 ;

            then

            reconsider m = ((r2 / 2) / |.a.|) as positive Real by A18, XREAL_1: 139;

            take m;

            (r2 / 2) < r2 by A15, XREAL_1: 215, XREAL_1: 216;

            hence thesis by A19, XCMPLX_1: 87;

          end;

        end;

        then

        consider m be positive Real such that

         A20: ( |.a.| * m) < r2;

        reconsider B = ( Ball (X,m)) as Subset of T by A1, TOPMETR: 12;

        reconsider nr = (r2 / ( |.x.| + m)) as positive Real by A17, XREAL_1: 139;

        take nr, B;

        thus B is open & x in B by GOBOARD6: 1, GOBOARD6: 3;

        let s be Real;

        assume

         A21: |.(s - a).| < nr;

        let z be object;

        assume z in (s * B);

        then z in { (s * b) where b be Element of T : b in B } by CONVEX1:def 1;

        then

        consider b be Element of T such that

         A22: z = (s * b) and

         A23: b in B;

        reconsider e = b, se = (s * b) as Point of E by A1, TOPMETR: 12;

        reconsider y = x, c = b as Element of ( REAL n) by EUCLID: 22;

        reconsider Y = y, C = c as Element of (n -tuples_on REAL ) by EUCLID:def 1;

        c = (C - (n |-> 0 )) by RVSUM_1: 32

        .= (C - (Y - Y)) by RVSUM_1: 37

        .= ((C - Y) + Y) by RVSUM_1: 41;

        then

         A24: |.c.| <= ( |.(c - y).| + |.y.|) by EUCLID: 12;

        

         A25: ( dist (X,e)) < m by A23, METRIC_1: 11;

        then |.(c - y).| < m by SPPOL_1: 5;

        then ( |.(c - y).| + |.y.|) <= (m + |.x.|) by XREAL_1: 6;

        then |.c.| <= (m + |.x.|) by A24, XXREAL_0: 2;

        then

         A26: (nr * |.c.|) <= (nr * (m + |.x.|)) by XREAL_1: 64;

        ((a * y) + ( - (a * c))) = ((a * y) + (( - 1) * (a * c))) by RVSUM_1: 54

        .= ((a * y) + ((( - 1) * a) * c)) by RVSUM_1: 49

        .= ((a * y) + (a * (( - 1) * c))) by RVSUM_1: 49

        .= (a * (y + (( - 1) * c))) by RVSUM_1: 51

        .= (a * (y + ( - c))) by RVSUM_1: 54

        .= (a * (y - c)) by RVSUM_1: 31;

        then

         A27: |.((a * y) + ( - (a * c))).| = ( |.a.| * |.(y - c).|) by EUCLID: 11;

         |.a.| >= 0 & |.(y - c).| = ( dist (X,e)) by COMPLEX1: 46, SPPOL_1: 5;

        then |.((a * y) + ( - (a * c))).| <= ( |.a.| * m) by A25, A27, XREAL_1: 64;

        then

         A28: |.((a * y) + ( - (a * c))).| < r2 by A20, XXREAL_0: 2;

        ((a * c) + ( - (s * c))) = ((a * c) + (( - 1) * (s * c))) by RVSUM_1: 54

        .= ((a * c) + ((( - 1) * s) * c)) by RVSUM_1: 49

        .= ((a + (( - 1) * s)) * c) by RVSUM_1: 50;

        

        then |.((a * c) + ( - (s * c))).| = ( |.(a - s).| * |.c.|) by EUCLID: 11

        .= ( |.( - (a - s)).| * |.c.|) by COMPLEX1: 52;

        then (nr * ( |.x.| + m)) = r2 & |.((a * c) + ( - (s * c))).| <= (nr * |.c.|) by A21, XCMPLX_1: 87, XREAL_1: 64;

        then |.((a * c) + ( - (s * c))).| <= r2 by A26, XXREAL_0: 2;

        then

         A29: |.(((a * y) + ( - (a * c))) + ((a * c) + ( - (s * c)))).| <= ( |.((a * y) + ( - (a * c))).| + |.((a * c) + ( - (s * c))).|) & ( |.((a * y) + ( - (a * c))).| + |.((a * c) + ( - (s * c))).|) < (r2 + r2) by A28, EUCLID: 12, XREAL_1: 8;

        ((a * y) - (s * c)) = (((a * Y) - (n |-> 0 )) - (s * C)) by RVSUM_1: 32

        .= (((a * y) - ((a * C) - (a * C))) - (s * c)) by RVSUM_1: 37

        .= ((((a * y) - (a * C)) + (a * C)) - (s * c)) by RVSUM_1: 41

        .= ((((a * y) - (a * C)) + (a * C)) + ( - (s * c))) by RVSUM_1: 31

        .= (((a * y) - (a * C)) + ((a * c) + ( - (s * c)))) by RVSUM_1: 15

        .= (((a * y) + ( - (a * c))) + ((a * c) + ( - (s * c)))) by RVSUM_1: 31;

        then ( dist (AX,se)) = |.(((a * y) + ( - (a * c))) + ((a * c) + ( - (s * c)))).| by SPPOL_1: 5;

        then ( dist (AX,se)) < r by A29, XXREAL_0: 2;

        then se in ( Ball (AX,r)) by METRIC_1: 11;

        hence z in V by A16, A22;

      end;

      cluster ( TOP-REAL n) -> finite-dimensional;

      coherence

      proof

         the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by EUCLID:def 8;

        then ( (Omega). ( TOP-REAL n)) = ( RealVectSpace ( Seg n)) by RLSUB_1:def 4;

        hence thesis by Th3;

      end;

    end

    reserve pn for Point of ( TOP-REAL n),

An for Subset of ( TOP-REAL n),

Affn for affinely-independent Subset of ( TOP-REAL n),

Ak for Subset of ( TOP-REAL k);

    theorem :: RLAFFIN3:4

    

     Th4: ( dim ( TOP-REAL n)) = n

    proof

       the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by EUCLID:def 8;

      then ( (Omega). ( TOP-REAL n)) = ( RealVectSpace ( Seg n)) by RLSUB_1:def 4;

      then ( dim ( (Omega). ( TOP-REAL n))) = n by EUCLID_7: 46;

      hence thesis by RLVECT_5: 30;

    end;

    theorem :: RLAFFIN3:5

    

     Th5: for V be finite-dimensional RealLinearSpace holds for A be affinely-independent Subset of V holds ( card A) <= (1 + ( dim V))

    proof

      let V be finite-dimensional RealLinearSpace;

      let A be affinely-independent Subset of V;

      per cases ;

        suppose A is empty;

        hence thesis;

      end;

        suppose A is non empty;

        then

        consider v be VECTOR of V such that v in A and

         A1: ((( - v) + A) \ {( 0. V)}) is linearly-independent by RLAFFIN1:def 4;

        set vA = (( - v) + A);

        (vA \ {( 0. V)}) misses {( 0. V)} by XBOOLE_1: 79;

        then

         A2: ( card {( 0. V)}) = 1 & ( card ((vA \ {( 0. V)}) \/ {( 0. V)})) = (( card (vA \ {( 0. V)})) + ( card {( 0. V)})) by CARD_2: 40, CARD_2: 42;

        

         A3: ( card vA) = ( card A) by RLAFFIN1: 7;

        reconsider vA as finite set;

        ( card (vA \ {( 0. V)})) = ( dim ( Lin ((( - v) + A) \ {( 0. V)}))) by A1, RLVECT_5: 29;

        then ( card (vA \ {( 0. V)})) <= ( dim V) by RLVECT_5: 28;

        then

         A4: ( card ((vA \ {( 0. V)}) \/ {( 0. V)})) <= (1 + ( dim V)) by A2, XREAL_1: 7;

        ((vA \ {( 0. V)}) \/ {( 0. V)}) = (vA \/ {( 0. V)}) by XBOOLE_1: 39;

        then ( card A) <= ( card ((vA \ {( 0. V)}) \/ {( 0. V)})) by A3, NAT_1: 43, XBOOLE_1: 7;

        hence thesis by A4, XXREAL_0: 2;

      end;

    end;

    theorem :: RLAFFIN3:6

    

     Th6: for V be finite-dimensional RealLinearSpace, A be affinely-independent Subset of V holds ( card A) = (( dim V) + 1) iff ( Affin A) = ( [#] V)

    proof

      let V be finite-dimensional RealLinearSpace;

      let A be affinely-independent Subset of V;

      

       A1: ( 0. V) in ( [#] V);

      

       A2: A c= ( Affin A) by RLAFFIN1: 49;

      hereby

        assume

         A3: ( card A) = (( dim V) + 1);

        then A is non empty;

        then

        consider v be VECTOR of V such that

         A4: v in A and

         A5: ((( - v) + A) \ {( 0. V)}) is linearly-independent by RLAFFIN1:def 4;

        set vA = (( - v) + A);

        reconsider vA as finite Subset of V;

        (( - v) + v) in { (( - v) + w) where w be Element of V : w in A } by A4;

        then

         A6: (( - v) + v) in vA by RUSUB_4:def 8;

        

         A7: ( card vA) = ( card A) & ( card {( 0. V)}) = 1 by CARD_2: 42, RLAFFIN1: 7;

        (( - v) + v) = ( 0. V) by RLVECT_1: 5;

        then vA = ((vA \ {( 0. V)}) \/ {( 0. V)}) by A6, ZFMISC_1: 116;

        then

         A8: ( card A) = (( card (vA \ {( 0. V)})) + 1) by A7, CARD_2: 40, XBOOLE_1: 79;

        ( dim ( Lin (vA \ {( 0. V)}))) = ( card (vA \ {( 0. V)})) by A5, RLVECT_5: 29;

        

        then ( (Omega). V) = ( (Omega). ( Lin (vA \ {( 0. V)}))) by A3, A8, RLVECT_5: 31

        .= ( Lin (vA \ {( 0. V)})) by RLSUB_1:def 4;

        then the RLSStruct of V = ( Lin (vA \ {( 0. V)})) by RLSUB_1:def 4;

        then

         A9: ( [#] V) = the carrier of ( Lin vA) by Lm2;

        then v in ( Lin vA);

        

        hence ( [#] V) = (v + ( Lin vA)) by A9, RLSUB_1: 48

        .= (v + ( Up ( Lin vA))) by RUSUB_4: 30

        .= ( Affin A) by A2, A4, RLAFFIN1: 57;

      end;

      assume

       A10: ( Affin A) = ( [#] V);

      then A is non empty;

      then

      consider v be VECTOR of V such that

       A11: v in A and

       A12: ((( - v) + A) \ {( 0. V)}) is linearly-independent by RLAFFIN1:def 4;

      set vA = (( - v) + A);

      reconsider vA as finite Subset of V;

      ( [#] V) = (v + ( Up ( Lin vA))) by A10, RLAFFIN1: 57

      .= (v + ( Lin vA)) by RUSUB_4: 30;

      

      then ( [#] ( Lin vA)) = the carrier of the RLSStruct of V by A1, RLSUB_1: 47

      .= the carrier of ( (Omega). V) by RLSUB_1:def 4;

      

      then ( Lin vA) = ( (Omega). V) by RLSUB_1: 30

      .= the RLSStruct of V by RLSUB_1:def 4;

      then the RLSStruct of V = ( Lin (vA \ {( 0. V)})) by Lm2;

      then

       A13: (vA \ {( 0. V)}) is Basis of V by A12, RLVECT_3:def 3;

      (( - v) + v) in { (( - v) + w) where w be Element of V : w in A } by A11;

      then

       A14: (( - v) + v) in vA by RUSUB_4:def 8;

      (( - v) + v) = ( 0. V) by RLVECT_1: 5;

      then

       A15: vA = ((vA \ {( 0. V)}) \/ {( 0. V)}) by A14, ZFMISC_1: 116;

      ( card vA) = ( card A) & ( card {( 0. V)}) = 1 by CARD_2: 42, RLAFFIN1: 7;

      

      hence ( card A) = (( card (vA \ {( 0. V)})) + 1) by A15, CARD_2: 40, XBOOLE_1: 79

      .= (( dim V) + 1) by A13, RLVECT_5:def 2;

    end;

    begin

    theorem :: RLAFFIN3:7

    

     Th7: k <= n & An = { v where v be Element of ( TOP-REAL n) : (v | k) in Ak } implies (An is open iff Ak is open)

    proof

      assume k <= n;

      then

      reconsider nk = (n - k) as Element of NAT by NAT_1: 21;

      

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

      then

      reconsider an = An as Subset of ( TopSpaceMetr ( Euclid n));

      

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

      then

      reconsider ak = Ak as Subset of ( TopSpaceMetr ( Euclid k));

      assume

       A3: An = { v where v be Element of ( TOP-REAL n) : (v | k) in Ak };

      hereby

        assume An is open;

        then an in the topology of ( TOP-REAL n) by PRE_TOPC:def 2;

        then

         A4: an is open by A1, PRE_TOPC:def 2;

        for e be Point of ( Euclid k) st e in ak holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= ak

        proof

          ( len (nk |-> 0 )) = nk & ( @ ( @ (nk |-> 0 ))) = (nk |-> 0 ) by CARD_1:def 7;

          then

          reconsider nk0 = (nk |-> 0 ) as Point of ( Euclid nk) by TOPREAL3: 45;

          let e be Point of ( Euclid k);

          

           A5: ( @ ( @ (e ^ (nk |-> 0 )))) = (e ^ (nk |-> 0 )) & ( len (e ^ nk0)) = n by CARD_1:def 7;

          then

          reconsider en = (e ^ nk0) as Point of ( Euclid n) by TOPREAL3: 45;

          reconsider En = (e ^ nk0) as Point of ( TOP-REAL n) by A5, TOPREAL3: 46;

          ( len e) = k by CARD_1:def 7;

          then ( dom e) = ( Seg k) by FINSEQ_1:def 3;

          then

           A6: e = (En | k) by FINSEQ_1: 21;

          assume e in ak;

          then en in an by A3, A6;

          then

          consider m be non zero Element of NAT such that

           A7: ( OpenHypercube (en,(1 / m))) c= an by A4, EUCLID_9: 23;

          take r = (1 / m);

          thus r > 0 by XREAL_1: 139;

          let y be object;

          assume

           A8: y in ( OpenHypercube (e,r));

          then

          reconsider p = y as Point of ( TopSpaceMetr ( Euclid k));

          

           A9: p in ( product ( Intervals (e,r))) by A8, EUCLID_9:def 4;

          reconsider P = p as Point of ( TOP-REAL k) by A2;

          nk0 in ( OpenHypercube (nk0,r)) by EUCLID_9: 11, XREAL_1: 139;

          then

           A10: nk0 in ( product ( Intervals (nk0,r))) by EUCLID_9:def 4;

          (( Intervals (e,r)) ^ ( Intervals (nk0,r))) = ( Intervals (en,r)) by Th1;

          then (P ^ nk0) in ( product ( Intervals (en,r))) by A10, A9, Th2;

          then (P ^ nk0) in ( OpenHypercube (en,r)) by EUCLID_9:def 4;

          then (P ^ nk0) in an by A7;

          then

          consider v be Element of ( TOP-REAL n) such that

           A11: v = (P ^ nk0) & (v | k) in Ak by A3;

          ( len P) = k by CARD_1:def 7;

          then ( dom P) = ( Seg k) by FINSEQ_1:def 3;

          hence y in ak by A11, FINSEQ_1: 21;

        end;

        then ak is open by EUCLID_9: 24;

        then ak in the topology of ( TOP-REAL k) by A2, PRE_TOPC:def 2;

        hence Ak is open by PRE_TOPC:def 2;

      end;

      assume Ak is open;

      then ak in the topology of ( TOP-REAL k) by PRE_TOPC:def 2;

      then

       A12: ak is open by A2, PRE_TOPC:def 2;

      for e be Point of ( Euclid n) st e in an holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= an

      proof

        let e be Point of ( Euclid n);

        assume e in an;

        then

        consider v be Element of ( TOP-REAL n) such that

         A13: e = v and

         A14: (v | k) in Ak by A3;

        reconsider vk = (v | k) as Point of ( TOP-REAL k) by A14;

        

         A15: ( len vk) = k by CARD_1:def 7;

        ( @ ( @ vk)) = vk;

        then

        reconsider Vk = vk as Point of ( Euclid k) by A15, TOPREAL3: 45;

        consider m be non zero Element of NAT such that

         A16: ( OpenHypercube (Vk,(1 / m))) c= ak by A12, A14, EUCLID_9: 23;

        take r = (1 / m);

        thus r > 0 by XREAL_1: 139;

        let y be object;

        assume

         A17: y in ( OpenHypercube (e,r));

        then

         A18: y in ( product ( Intervals (e,r))) by EUCLID_9:def 4;

        reconsider Y = y as Point of ( TOP-REAL n) by A1, A17;

        

         A19: ( len v) = n by CARD_1:def 7;

        consider q be FinSequence such that

         A20: ( @ ( @ v)) = (vk ^ q) by FINSEQ_1: 80;

        reconsider q as FinSequence of REAL by A20, FINSEQ_1: 36;

        ( len v) = (( len vk) + ( len q)) by A20, FINSEQ_1: 22;

        then

        reconsider Q = q as Point of ( Euclid nk) by A15, A19, TOPREAL3: 45;

        (( Intervals (Vk,r)) ^ ( Intervals (Q,r))) = ( Intervals (e,r)) by A13, A20, Th1;

        then

        consider p1,p2 be FinSequence such that

         A21: y = (p1 ^ p2) and

         A22: p1 in ( product ( Intervals (Vk,r))) and p2 in ( product ( Intervals (Q,r))) by A18, Th2;

        

         A23: p1 in ( OpenHypercube (Vk,(1 / m))) by A22, EUCLID_9:def 4;

        then ( len p1) = k by A2, CARD_1:def 7;

        

        then (Y | k) = (Y | ( dom p1)) by FINSEQ_1:def 3

        .= p1 by A21, FINSEQ_1: 21;

        hence thesis by A3, A16, A23;

      end;

      then an is open by EUCLID_9: 24;

      then an in the topology of ( TOP-REAL n) by A1, PRE_TOPC:def 2;

      hence thesis by PRE_TOPC:def 2;

    end;

    

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

    proof

      

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

      .= ( REAL n) by EUCLID:def 1, VECTSP_1:def 5

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

    end;

    theorem :: RLAFFIN3:8

    

     Th8: for A be Subset of ( TOP-REAL (k + n)) st A = the set of all (v ^ (n |-> 0 )) where v be Element of ( TOP-REAL k) holds for B be Subset of (( TOP-REAL (k + n)) | A) st B = { v where v be Point of ( TOP-REAL (k + n)) : (v | k) in Ak & v in A } holds Ak is open iff B is open

    proof

      set kn = (k + n);

      set TRn = ( TOP-REAL kn);

      set TRk = ( TOP-REAL k);

      let A be Subset of TRn such that

       A1: A = the set of all (v ^ (n |-> 0 )) where v be Element of TRk;

      

       A2: the TopStruct of TRk = ( TopSpaceMetr ( Euclid k)) by EUCLID:def 8;

      then

      reconsider p = Ak as Subset of ( TopSpaceMetr ( Euclid k));

      set TRA = (TRn | A);

      let B be Subset of (TRn | A) such that

       A3: B = { v where v be Element of TRn : (v | k) in Ak & v in A };

      

       A4: ( [#] TRA) = A by PRE_TOPC:def 5;

      

       A5: kn >= k by NAT_1: 11;

      hereby

        set PP = { v where v be Element of TRn : (v | k) in Ak };

        PP c= ( [#] TRn)

        proof

          let x be object;

          assume x in PP;

          then ex v be Element of TRn st x = v & (v | k) in Ak;

          hence thesis;

        end;

        then

        reconsider PP as Subset of TRn;

        

         A6: (PP /\ A) c= B

        proof

          let x be object;

          assume

           A7: x in (PP /\ A);

          then x in PP by XBOOLE_0:def 4;

          then

          consider v be Element of TRn such that

           A8: x = v & (v | k) in Ak;

          x in A by A7, XBOOLE_0:def 4;

          hence thesis by A3, A8;

        end;

        assume Ak is open;

        then PP is open by A5, Th7;

        then PP in the topology of TRn by PRE_TOPC:def 2;

        then

         A9: (PP /\ ( [#] TRA)) in the topology of TRA by PRE_TOPC:def 4;

        B c= (PP /\ A)

        proof

          let x be object;

          assume x in B;

          then

          consider v be Element of TRn such that

           A10: x = v and

           A11: (v | k) in Ak and

           A12: v in A by A3;

          v in PP by A11;

          hence thesis by A10, A12, XBOOLE_0:def 4;

        end;

        then B = (PP /\ A) by A6;

        hence B is open by A4, A9, PRE_TOPC:def 2;

      end;

      assume B is open;

      then B in the topology of TRA by PRE_TOPC:def 2;

      then

      consider Q be Subset of TRn such that

       A13: Q in the topology of TRn and

       A14: (Q /\ ( [#] TRA)) = B by PRE_TOPC:def 4;

      

       A15: the TopStruct of TRn = ( TopSpaceMetr ( Euclid kn)) by EUCLID:def 8;

      then

      reconsider q = Q as Subset of ( TopSpaceMetr ( Euclid kn));

      

       A16: q is open by A13, A15, PRE_TOPC:def 2;

      for e be Point of ( Euclid k) st e in p holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= p

      proof

        let e be Point of ( Euclid k);

        

         A17: ( len (n |-> 0 )) = n by CARD_1:def 7;

        

         A18: ( @ ( @ (e ^ (n |-> 0 )))) = (e ^ (n |-> 0 ));

        

         A19: ( len e) = k by CARD_1:def 7;

        then ( len (e ^ (n |-> 0 ))) = kn by A17, FINSEQ_1: 22;

        then

        reconsider e0 = (e ^ (n |-> 0 )) as Point of ( Euclid kn) by A18, TOPREAL3: 45;

        ( dom e) = ( Seg k) by A19, FINSEQ_1:def 3;

        then

         A20: e = (e0 | k) by FINSEQ_1: 21;

        (n |-> 0 ) = ( @ ( @ (n |-> 0 )));

        then

        reconsider N = (n |-> 0 ) as Element of ( Euclid n) by A17, TOPREAL3: 45;

        e is Element of TRk by Lm1;

        then

         A21: e0 in A by A1;

        assume e in p;

        then e0 in B by A3, A21, A20;

        then e0 in q by A14, XBOOLE_0:def 4;

        then

        consider m be non zero Element of NAT such that

         A22: ( OpenHypercube (e0,(1 / m))) c= q by A16, EUCLID_9: 23;

        set r = (1 / m);

        take r;

        thus r > 0 by XREAL_1: 139;

        let x be object;

        N in ( OpenHypercube (N,r)) by EUCLID_9: 11, XREAL_1: 139;

        then

         A23: N in ( product ( Intervals (N,r))) by EUCLID_9:def 4;

        assume

         A24: x in ( OpenHypercube (e,r));

        then

        reconsider w = x as Point of TRk by A2;

        

         A25: (( Intervals (e,r)) ^ ( Intervals (N,r))) = ( Intervals ((e ^ N),r)) by Th1;

        w in ( product ( Intervals (e,r))) by A24, EUCLID_9:def 4;

        then (w ^ N) in ( product ( Intervals (e0,r))) by A23, A25, Th2;

        then

         A26: (w ^ N) in ( OpenHypercube (e0,r)) by EUCLID_9:def 4;

        (w ^ N) in A by A1;

        then (w ^ N) in B by A4, A14, A22, A26, XBOOLE_0:def 4;

        then

         A27: ex v be Element of TRn st (w ^ N) = v & (v | k) in Ak & v in A by A3;

        ( len w) = k by CARD_1:def 7;

        

        then ((w ^ N) | k) = ((w ^ N) | ( dom w)) by FINSEQ_1:def 3

        .= w by FINSEQ_1: 21;

        hence thesis by A27;

      end;

      then p is open by EUCLID_9: 24;

      then Ak in the topology of ( TOP-REAL k) by A2, PRE_TOPC:def 2;

      hence thesis by PRE_TOPC:def 2;

    end;

    theorem :: RLAFFIN3:9

    

     Th9: for A be affinely-independent Subset of V, B be Subset of V st B c= A holds (( conv A) /\ ( Affin B)) = ( conv B)

    proof

      let A be affinely-independent Subset of V;

      let B be Subset of V;

      

       A1: ( conv B) c= ( Affin B) by RLAFFIN1: 65;

      assume

       A2: B c= A;

      thus (( conv A) /\ ( Affin B)) c= ( conv B)

      proof

        let x be object;

        assume

         A3: x in (( conv A) /\ ( Affin B));

        then

         A4: x in ( Affin B) by XBOOLE_0:def 4;

        

         A5: x in ( conv A) by A3, XBOOLE_0:def 4;

         A6:

        now

          let v be Element of V;

          (x |-- B) = (x |-- A) by A2, A4, RLAFFIN1: 77;

          hence v in B implies 0 <= ((x |-- B) . v) by A5, RLAFFIN1: 71;

        end;

        B is affinely-independent by A2, RLAFFIN1: 43;

        hence thesis by A4, A6, RLAFFIN1: 73;

      end;

      ( conv B) c= ( conv A) by A2, RLAFFIN1: 3;

      hence thesis by A1, XBOOLE_1: 19;

    end;

    theorem :: RLAFFIN3:10

    

     Th10: for V be non empty RLSStruct, A be non empty set holds for f be PartFunc of A, the carrier of V holds for X be set holds ((r (#) f) .: X) = (r * (f .: X))

    proof

      let V be non empty RLSStruct;

      let A be non empty set;

      let f be PartFunc of A, the carrier of V;

      let X be set;

      set rf = (r (#) f);

      

       A1: ( dom rf) = ( dom f) by VFUNCT_1:def 4;

      hereby

        let y be object;

        assume y in (rf .: X);

        then

        consider x be object such that

         A2: x in ( dom rf) and

         A3: x in X and

         A4: y = (rf . x) by FUNCT_1:def 6;

        (rf . x) = (rf /. x) by A2, PARTFUN1:def 6;

        then

         A5: y = (r * (f /. x)) by A2, A4, VFUNCT_1:def 4;

        (f . x) = (f /. x) by A1, A2, PARTFUN1:def 6;

        then (f /. x) in (f .: X) by A1, A2, A3, FUNCT_1:def 6;

        then y in { (r * v) where v be Element of V : v in (f .: X) } by A5;

        hence y in (r * (f .: X)) by CONVEX1:def 1;

      end;

      let y be object;

      assume y in (r * (f .: X));

      then y in { (r * v) where v be Element of V : v in (f .: X) } by CONVEX1:def 1;

      then

      consider v be Element of V such that

       A6: y = (r * v) and

       A7: v in (f .: X);

      consider x be object such that

       A8: x in ( dom f) and

       A9: x in X and

       A10: v = (f . x) by A7, FUNCT_1:def 6;

      v = (f /. x) by A8, A10, PARTFUN1:def 6;

      

      then y = (rf /. x) by A1, A6, A8, VFUNCT_1:def 4

      .= (rf . x) by A1, A8, PARTFUN1:def 6;

      hence thesis by A1, A8, A9, FUNCT_1:def 6;

    end;

    theorem :: RLAFFIN3:11

    

     Th11: ( 0* n) in An implies ( Affin An) = ( [#] ( Lin An))

    proof

      set TR = ( TOP-REAL n);

      set A = An;

      

       A1: ( 0* n) = ( 0. TR) & A c= ( Affin A) by EUCLID: 66, RLAFFIN1: 49;

      assume ( 0* n) in A;

      

      hence ( Affin A) = (( 0. TR) + ( Up ( Lin (( - ( 0. TR)) + A)))) by A1, RLAFFIN1: 57

      .= ( Up ( Lin (( - ( 0. TR)) + A))) by RLAFFIN1: 6

      .= ( Up ( Lin (( 0. TR) + A))) by RLVECT_1: 12

      .= ( Up ( Lin A)) by RLAFFIN1: 6

      .= ( [#] ( Lin A)) by RUSUB_4:def 5;

    end;

    registration

      let V be non empty addLoopStr;

      let A be finite Subset of V;

      let v be Element of V;

      cluster (v + A) -> finite;

      coherence

      proof

        deffunc F( Element of V) = (v + $1);

        ( card { F(w) where w be Element of V : w in A }) c= ( card A) from TREES_2:sch 2;

        then ( card (v + A)) is finite by RUSUB_4:def 8;

        hence thesis;

      end;

    end

    

     Lm4: for V be non empty RLSStruct, A be Subset of V, r be Real holds ( card (r * A)) c= ( card A)

    proof

      let V be non empty RLSStruct;

      let A be Subset of V;

      let r be Real;

      deffunc F( Element of V) = (r * $1);

      ( card { F(w) where w be Element of V : w in A }) c= ( card A) from TREES_2:sch 2;

      hence thesis by CONVEX1:def 1;

    end;

    registration

      let V be non empty RLSStruct;

      let A be finite Subset of V;

      let r;

      cluster (r * A) -> finite;

      coherence

      proof

        ( card (r * A)) c= ( card A) by Lm4;

        hence thesis;

      end;

    end

    theorem :: RLAFFIN3:12

    

     Th12: for A be Subset of V holds ( card A) = ( card (r * A)) iff r <> 0 or A is trivial

    proof

      let A be Subset of V;

      

       A1: ( card {( 0. V)}) = 1 by CARD_2: 42;

      hereby

        assume

         A2: ( card A) = ( card (r * A));

        assume

         A3: r = 0 ;

        then

         A4: (r * A) c= {( 0. V)} by RLAFFIN1: 12;

        then

        reconsider a = A as finite set by A2;

        reconsider rA = (r * A) as finite set by A4;

        ( card rA) <= ( card {( 0. V)}) by A3, NAT_1: 43, RLAFFIN1: 12;

        then ( card a) < (1 + 1) by A1, A2, NAT_1: 13;

        hence A is trivial by NAT_D: 60;

      end;

      assume

       A5: r <> 0 or A is trivial;

      per cases by A5;

        suppose

         A6: r <> 0 ;

        

         A7: (1 * A) = A & (((1 / r) * r) * A) = ((1 / r) * (r * A)) by RLAFFIN1: 10, RLAFFIN1: 11;

        

         A8: ( card (r * A)) c= ( card A) by Lm4;

        ((1 / r) * r) = 1 by A6, XCMPLX_1: 87;

        then ( card A) c= ( card (r * A)) by A7, Lm4;

        hence thesis by A8;

      end;

        suppose

         A9: A is empty;

        (r * A) is empty

        proof

          assume (r * A) is non empty;

          then

          consider x be object such that

           A10: x in (r * A);

          x in { (r * v) where v be Element of V : v in A } by A10, CONVEX1:def 1;

          then ex v be Element of V st x = (r * v) & v in A;

          hence contradiction by A9;

        end;

        hence thesis by A9;

      end;

        suppose

         A11: r = 0 & A is 1 -element;

        then

        consider x be object such that

         A12: A = {x} by ZFMISC_1: 131;

        (r * A) = {( 0. V)} by A11, CONVEX1: 34;

        hence thesis by A1, A12, CARD_2: 42;

      end;

    end;

    registration

      let V be non empty RLSStruct;

      let f be FinSequence of V;

      let r;

      cluster (r (#) f) -> FinSequence-like;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by VFUNCT_1:def 4

        .= ( Seg ( len f)) by FINSEQ_1:def 3;

        hence thesis;

      end;

    end

    begin

    definition

      let X be finite set;

      :: RLAFFIN3:def1

      mode Enumeration of X -> one-to-one FinSequence means

      : Def1: ( rng it ) = X;

      existence

      proof

        ex p be FinSequence st ( rng p) = X & p is one-to-one by FINSEQ_4: 58;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let A be finite Subset of X;

      :: original: Enumeration

      redefine

      mode Enumeration of A -> one-to-one FinSequence of X ;

      coherence

      proof

        let E be Enumeration of A;

        ( rng E) = A by Def1;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    reserve EV for Enumeration of Affv,

EN for Enumeration of Affn;

    theorem :: RLAFFIN3:13

    

     Th13: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr holds for A be finite Subset of V, E be Enumeration of A, v be Element of V holds (E + (( card A) |-> v)) is Enumeration of (v + A)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let A be finite Subset of V;

      let E be Enumeration of A;

      let v be Element of V;

      

       A1: ( rng E) = A by Def1;

      then

       A2: ( len E) = ( card A) by FINSEQ_4: 62;

      then

      reconsider e = E, cAv = (( card A) |-> v) as Element of (( card A) -tuples_on the carrier of V) by FINSEQ_2: 92;

      

       A3: ( len (e + cAv)) = ( card A) by CARD_1:def 7;

      then

       A4: ( dom (e + cAv)) = ( Seg ( card A)) by FINSEQ_1:def 3;

      

       A5: ( dom e) = ( Seg ( card A)) by A2, FINSEQ_1:def 3;

      

       A6: ( rng (e + cAv)) c= (v + A)

      proof

        let y be object;

        assume y in ( rng (e + cAv));

        then

        consider x be object such that

         A7: x in ( dom (e + cAv)) and

         A8: ((e + cAv) . x) = y by FUNCT_1:def 3;

        reconsider x as Element of NAT by A7;

        

         A9: (e . x) in ( rng e) by A5, A4, A7, FUNCT_1:def 3;

        then

        reconsider Ex = (e . x) as Element of V;

        (cAv . x) = v by A4, A7, FINSEQ_2: 57;

        then y = (Ex + v) by A7, A8, FVSUM_1: 17;

        then y = (v + Ex) by RLVECT_1:def 2;

        then y in { (v + w) where w be Element of V : w in A } by A1, A9;

        hence thesis by RUSUB_4:def 8;

      end;

      (v + A) c= ( rng (e + cAv))

      proof

        let vA be object;

        assume vA in (v + A);

        then vA in { (v + a) where a be Element of V : a in A } by RUSUB_4:def 8;

        then

        consider a be Element of V such that

         A10: vA = (v + a) and

         A11: a in A;

        consider x be object such that

         A12: x in ( dom E) and

         A13: (E . x) = a by A1, A11, FUNCT_1:def 3;

        reconsider x as Element of NAT by A12;

        (cAv . x) = v by A5, A12, FINSEQ_2: 57;

        

        then ((e + cAv) . x) = (a + v) by A5, A4, A12, A13, FVSUM_1: 17

        .= vA by A10, RLVECT_1:def 2;

        hence thesis by A5, A4, A12, FUNCT_1:def 3;

      end;

      then

       A14: (v + A) = ( rng (e + cAv)) by A6;

      ( card A) = ( card (v + A)) by RLAFFIN1: 7;

      then (e + cAv) is one-to-one by A3, A14, FINSEQ_4: 62;

      hence thesis by A14, Def1;

    end;

    theorem :: RLAFFIN3:14

    for E be Enumeration of Av holds (r (#) E) is Enumeration of (r * Av) iff r <> 0 or Av is trivial

    proof

      let EV be Enumeration of Av;

      set rE = (r (#) EV);

      

       A1: ( dom rE) = ( dom EV) by VFUNCT_1:def 4;

      then

       A2: ( len rE) = ( len EV) by FINSEQ_3: 29;

      

       A3: ( rng EV) = Av by Def1;

      then

       A4: ( card Av) = ( len EV) by FINSEQ_4: 62;

      

       A5: ( rng rE) = (rE .: ( dom EV)) by A1, RELAT_1: 113

      .= (r * (EV .: ( dom EV))) by Th10

      .= (r * Av) by A3, RELAT_1: 113;

      

       A6: ( card {( 0. V)}) = 1 by CARD_2: 42;

      hereby

        reconsider rA = (r * Av) as finite set;

        assume rE is Enumeration of (r * Av);

        then

         A7: ( card (r * Av)) = ( card Av) by A4, A2, A5, FINSEQ_4: 62;

        assume r = 0 ;

        then ( card Av) <= 1 by A6, A7, NAT_1: 43, RLAFFIN1: 12;

        then ( card Av) < (1 + 1) by NAT_1: 13;

        hence Av is trivial by NAT_D: 60;

      end;

      assume r <> 0 or Av is trivial;

      then ( card Av) = ( card (r * Av)) by Th12;

      then rE is one-to-one by A4, A2, A5, FINSEQ_4: 62;

      hence thesis by A5, Def1;

    end;

    theorem :: RLAFFIN3:15

    

     Th15: for M be Matrix of n, m, F_Real st ( the_rank_of M) = n holds for A be finite Subset of ( TOP-REAL n), E be Enumeration of A holds (( Mx2Tran M) * E) is Enumeration of (( Mx2Tran M) .: A)

    proof

      let M be Matrix of n, m, F_Real such that

       A1: ( the_rank_of M) = n;

      set MT = ( Mx2Tran M);

      

       A2: MT is one-to-one by A1, MATRTOP1: 39;

      set TRn = ( TOP-REAL n);

      let A be finite Subset of ( TOP-REAL n);

      let E be Enumeration of A;

      

       A3: ( rng E) = A by Def1;

      ( dom MT) = ( [#] TRn) by FUNCT_2:def 1;

      then ( len (MT * E)) = ( len E) by A3, FINSEQ_2: 29;

      then

       A4: ( dom (MT * E)) = ( dom E) by FINSEQ_3: 29;

      ( rng (MT * E)) = ((MT * E) .: ( dom (MT * E))) by RELAT_1: 113

      .= (MT .: (E .: ( dom E))) by A4, RELAT_1: 126

      .= (MT .: A) by A3, RELAT_1: 113;

      hence thesis by A2, Def1;

    end;

    definition

      let V, Av;

      let E be Enumeration of Av;

      let x be object;

      :: RLAFFIN3:def2

      func x |-- E -> FinSequence of REAL equals ((x |-- Av) * E);

      coherence ;

    end

    theorem :: RLAFFIN3:16

    

     Th16: for x be object holds for E be Enumeration of Av holds ( len (x |-- E)) = ( card Av)

    proof

      let x be object;

      let E be Enumeration of Av;

      ( rng E) = Av by Def1;

      then ( len E) = ( card Av) by FINSEQ_4: 62;

      hence thesis by FINSEQ_2: 33;

    end;

    theorem :: RLAFFIN3:17

    

     Th17: for E be Enumeration of (v + Affv) st w in ( Affin Affv) & E = (EV + (( card Affv) |-> v)) holds (w |-- EV) = ((v + w) |-- E)

    proof

      set E = EV;

      let Ev be Enumeration of (v + Affv) such that

       A1: w in ( Affin Affv) and

       A2: Ev = (E + (( card Affv) |-> v));

      set wA = (w |-- Affv);

      

       A3: ( sum wA) = 1 by A1, RLAFFIN1:def 7;

      (v + w) in { (v + u) : u in ( Affin Affv) } by A1;

      then

       A4: (v + w) in (v + ( Affin Affv)) by RUSUB_4:def 8;

      ( rng E) = Affv by Def1;

      then

       A5: ( len E) = ( card Affv) by FINSEQ_4: 62;

      then

      reconsider e = E, cAv = (( card Affv) |-> v) as Element of (( card Affv) -tuples_on the carrier of V) by FINSEQ_2: 92;

      

       A6: ( Affin (v + Affv)) = (v + ( Affin Affv)) & (1 * v) = v by RLAFFIN1: 53, RLVECT_1:def 8;

      ( Carrier (v + wA)) = (v + ( Carrier wA)) & ( Carrier wA) c= Affv by RLAFFIN1: 16, RLVECT_2:def 6;

      then ( Carrier (v + wA)) c= (v + Affv) by RLTOPSP1: 8;

      then

      reconsider vwA = (v + wA) as Linear_Combination of (v + Affv) by RLVECT_2:def 6;

      ( Sum wA) = w by A1, RLAFFIN1:def 7;

      then

       A7: ( Sum vwA) = ((1 * v) + w) by A3, RLAFFIN1: 39;

      

       A8: ( len (w |-- E)) = ( card Affv) by Th16;

      

       A9: ( card Affv) = ( card (v + Affv)) by RLAFFIN1: 7;

      then ( len ((v + w) |-- Ev)) = ( card Affv) by Th16;

      then

       A10: ( dom (w |-- E)) = ( dom ((v + w) |-- Ev)) by A8, FINSEQ_3: 29;

      ( rng Ev) = (v + Affv) by Def1;

      then

       A11: ( len Ev) = ( card Affv) by A9, FINSEQ_4: 62;

      ( sum vwA) = 1 by A3, RLAFFIN1: 37;

      then

       A12: vwA = ((v + w) |-- (v + Affv)) by A4, A7, A6, RLAFFIN1:def 7;

      now

        let i be Nat;

        assume

         A13: i in ( dom (w |-- E));

        then

         A14: ((w |-- E) . i) = ((w |-- Affv) . (E . i)) by FUNCT_1: 12;

        ( dom E) = ( dom (w |-- E)) by A8, A5, FINSEQ_3: 29;

        then

         A15: (E . i) = (E /. i) by A13, PARTFUN1:def 6;

        i in ( Seg ( card Affv)) by A8, A13, FINSEQ_1:def 3;

        then

         A16: (cAv . i) = v by FINSEQ_2: 57;

        

         A17: (((v + w) |-- Ev) . i) = (((v + w) |-- (v + Affv)) . (Ev . i)) by A10, A13, FUNCT_1: 12;

        ( dom Ev) = ( dom (w |-- E)) by A8, A11, FINSEQ_3: 29;

        then (Ev . i) = ((E /. i) + v) by A2, A13, A16, A15, FVSUM_1: 17;

        

        hence (((v + w) |-- Ev) . i) = ((w |-- Affv) . (((E /. i) + v) - v)) by A12, A17, RLAFFIN1:def 1

        .= ((w |-- Affv) . ((E /. i) + (v - v))) by RLVECT_1: 28

        .= ((w |-- Affv) . ((E /. i) + ( 0. V))) by RLVECT_1: 15

        .= ((w |-- E) . i) by A14, A15, RLVECT_1:def 4;

      end;

      hence thesis by A10, FINSEQ_1: 13;

    end;

    theorem :: RLAFFIN3:18

    for rE be Enumeration of (r * Affv) st v in ( Affin Affv) & rE = (r (#) EV) & r <> 0 holds (v |-- EV) = ((r * v) |-- rE)

    proof

      set E = EV;

      let rE be Enumeration of (r * Affv) such that

       A1: v in ( Affin Affv) and

       A2: rE = (r (#) E) and

       A3: r <> 0 ;

      set vA = (v |-- Affv);

      

       A4: ( Carrier vA) c= Affv by RLVECT_2:def 6;

      

       A5: (r * v) in { (r * u) : u in ( Affin Affv) } by A1;

      

       A6: ( dom rE) = ( dom E) by A2, VFUNCT_1:def 4;

      ( Carrier (r (*) vA)) = (r * ( Carrier vA)) by A3, RLAFFIN1: 23;

      then ( Carrier (r (*) vA)) c= (r * Affv) by A4, CONVEX1: 39;

      then

      reconsider rvA = (r (*) vA) as Linear_Combination of (r * Affv) by RLVECT_2:def 6;

      ( sum vA) = 1 by A1, RLAFFIN1:def 7;

      then

       A7: ( sum rvA) = 1 by A3, RLAFFIN1: 38;

      ( Sum vA) = v by A1, RLAFFIN1:def 7;

      then

       A8: ( Sum rvA) = (r * v) by RLAFFIN1: 40;

      

       A9: ( len ((r * v) |-- rE)) = ( card (r * Affv)) by Th16;

      

       A10: ( len (v |-- E)) = ( card Affv) by Th16;

      ( rng E) = Affv by Def1;

      then ( len E) = ( card Affv) by FINSEQ_4: 62;

      then

       A11: ( dom (v |-- E)) = ( dom E) by A10, FINSEQ_3: 29;

      ( card Affv) = ( card (r * Affv)) by A3, Th12;

      then

       A12: ( dom (v |-- E)) = ( dom ((r * v) |-- rE)) by A10, A9, FINSEQ_3: 29;

      ( Affin (r * Affv)) = (r * ( Affin Affv)) by A3, RLAFFIN1: 55;

      then (r * v) in ( Affin (r * Affv)) by A5, CONVEX1:def 1;

      then

       A13: rvA = ((r * v) |-- (r * Affv)) by A7, A8, RLAFFIN1:def 7;

      now

        let k be Nat;

        assume

         A14: k in ( dom (v |-- E));

        then

         A15: ((v |-- E) . k) = (vA . (E . k)) & (E /. k) = (E . k) by A11, FUNCT_1: 12, PARTFUN1:def 6;

        

         A16: (rE /. k) = (r * (E /. k)) by A2, A11, A6, A14, VFUNCT_1:def 4;

        (((r * v) |-- rE) . k) = (rvA . (rE . k)) & (rE /. k) = (rE . k) by A13, A12, A11, A6, A14, FUNCT_1: 12, PARTFUN1:def 6;

        

        hence (((r * v) |-- rE) . k) = (vA . ((r " ) * (r * (E /. k)))) by A3, A16, RLAFFIN1:def 2

        .= (vA . (((r " ) * r) * (E /. k))) by RLVECT_1:def 7

        .= (vA . (1 * (E /. k))) by A3, XCMPLX_0:def 7

        .= ((v |-- E) . k) by A15, RLVECT_1:def 8;

      end;

      hence thesis by A12, FINSEQ_1: 13;

    end;

    theorem :: RLAFFIN3:19

    

     Th19: for M be Matrix of n, m, F_Real st ( the_rank_of M) = n holds for ME be Enumeration of (( Mx2Tran M) .: Affn) st ME = (( Mx2Tran M) * EN) holds for pn st pn in ( Affin Affn) holds (pn |-- EN) = ((( Mx2Tran M) . pn) |-- ME)

    proof

      set TRn = ( TOP-REAL n);

      let M be Matrix of n, m, F_Real such that

       A1: ( the_rank_of M) = n;

      set MT = ( Mx2Tran M);

      

       A2: MT is one-to-one by A1, MATRTOP1: 39;

      set E = EN;

      set A = Affn;

      let ME be Enumeration of (( Mx2Tran M) .: A) such that

       A3: ME = (( Mx2Tran M) * E);

      ( dom MT) = the carrier of TRn by FUNCT_2:def 1;

      then (A,(MT .: A)) are_equipotent by A2, CARD_1: 33;

      then

       A4: ( card A) = ( card (MT .: A)) by CARD_1: 5;

      let v be Element of ( TOP-REAL n) such that

       A5: v in ( Affin A);

      set MTv = (MT . v);

      

       A6: ( len (v |-- E)) = ( card A) by Th16;

      

       A7: ( len (MTv |-- ME)) = ( card (MT .: A)) by Th16;

      now

        let i be Nat;

        assume

         A8: 1 <= i & i <= ( card A);

        then

         A9: i in ( dom (MTv |-- ME)) by A4, A7, FINSEQ_3: 25;

        then

         A10: i in ( dom ME) by FUNCT_1: 11;

        

         A11: i in ( dom (v |-- E)) by A6, A8, FINSEQ_3: 25;

        then i in ( dom E) by FUNCT_1: 11;

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

        then

        reconsider Ei = (E . i) as Element of TRn;

        

        thus ((v |-- E) . i) = ((v |-- A) . Ei) by A11, FUNCT_1: 12

        .= ((MTv |-- (MT .: A)) . (MT . Ei)) by A1, A5, MATRTOP2: 25

        .= ((MTv |-- (MT .: A)) . (ME . i)) by A3, A10, FUNCT_1: 12

        .= ((MTv |-- ME) . i) by A9, FUNCT_1: 12;

      end;

      hence thesis by A4, A7, A6;

    end;

    theorem :: RLAFFIN3:20

    

     Th20: for A be Subset of V st A c= Affv & x in ( Affin Affv) holds x in ( Affin A) iff for y be set st y in ( dom (x |-- EV)) & not (EV . y) in A holds ((x |-- EV) . y) = 0

    proof

      let B be Subset of V such that

       A1: B c= Affv;

      set xA = (x |-- Affv);

      set xB = (x |-- B);

      set cA = ( card Affv);

      set E = EV;

      assume

       A2: x in ( Affin Affv);

      set xE = (x |-- E);

      

       A3: ( len xE) = cA by Th16;

      

       A4: ( rng E) = Affv by Def1;

      then ( len E) = cA by FINSEQ_4: 62;

      then

       A5: ( dom xE) = ( dom E) by A3, FINSEQ_3: 29;

      

       A6: ( Carrier xB) c= B by RLVECT_2:def 6;

      hereby

        assume x in ( Affin B);

        then

         A7: xB = xA by A1, RLAFFIN1: 77;

        let y be set;

        assume that

         A8: y in ( dom xE) and

         A9: not (E . y) in B;

        y in ( dom E) by A8, FUNCT_1: 11;

        then (E . y) in Affv by A4, FUNCT_1:def 3;

        then

        reconsider Ey = (E . y) as Element of V;

        (xE . y) = ((x |-- Affv) . (E . y)) & not Ey in ( Carrier xB) by A6, A8, A9, FUNCT_1: 12;

        hence (xE . y) = 0 by A7, RLVECT_2: 19;

      end;

      assume

       A10: for y be set st y in ( dom xE) & not (E . y) in B holds (xE . y) = 0 ;

       A11:

      now

        let y be set;

        assume

         A12: y in (Affv \ B);

        then y in Affv by XBOOLE_0:def 5;

        then

        consider z be object such that

         A13: z in ( dom E) & (E . z) = y by A4, FUNCT_1:def 3;

         not y in B by A12, XBOOLE_0:def 5;

        then (xE . z) = 0 by A5, A10, A13;

        hence (xA . y) = 0 by A5, A13, FUNCT_1: 12;

      end;

      (Affv \ (Affv \ B)) = (Affv /\ B) by XBOOLE_1: 48

      .= B by A1, XBOOLE_1: 28;

      hence thesis by A2, A11, RLAFFIN1: 75;

    end;

    theorem :: RLAFFIN3:21

    for EV st x in ( Affin Affv) holds x in ( Affin (EV .: ( Seg k))) iff (x |-- EV) = (((x |-- EV) | k) ^ ((( card Affv) -' k) |-> 0 ))

    proof

      let E be Enumeration of Affv;

      set B = (E .: ( Seg k));

      set cA = ( card Affv);

      set cAk = (cA -' k);

      set xE = (x |-- E);

      set xEk = (xE | k);

      set cAk0 = (cAk |-> 0 );

      

       A1: B c= ( rng E) by RELAT_1: 111;

      assume

       A2: x in ( Affin Affv);

      then

      reconsider v = x as Element of V;

      

       A3: ( len xE) = cA by Th16;

      

       A4: ( rng E) = Affv by Def1;

      then

       A5: ( len E) = cA by FINSEQ_4: 62;

      per cases ;

        suppose

         A6: k > cA;

        then ( Seg cA) c= ( Seg k) by FINSEQ_1: 5;

        then ( dom E) c= ( Seg k) by A5, FINSEQ_1:def 3;

        then (( dom E) /\ ( Seg k)) = ( dom E) by XBOOLE_1: 28;

        then

         A7: B = (E .: ( dom E)) by RELAT_1: 112;

        (cA - k) < 0 by A6, XREAL_1: 49;

        then cAk = 0 by XREAL_0:def 2;

        then

         A8: cAk0 is empty;

        xEk = xE by A3, A6, FINSEQ_1: 58;

        hence thesis by A2, A4, A8, A7, FINSEQ_1: 34, RELAT_1: 113;

      end;

        suppose

         A9: k <= cA;

        

         A10: ( len cAk0) = cAk by CARD_1:def 7;

        

         A11: ( len xEk) = k by A3, A9, FINSEQ_1: 59;

        cAk = (cA - k) by A9, XREAL_1: 233;

        then

         A12: ( len (xEk ^ cAk0)) = (k + (cA - k)) by A11, A10, FINSEQ_1: 22;

        hereby

          assume

           A13: x in ( Affin B);

          now

            let i be Nat;

            assume

             A14: 1 <= i & i <= ( len xE);

            then

             A15: i in ( dom xE) by FINSEQ_3: 25;

            

             A16: i in ( dom E) by A3, A5, A14, FINSEQ_3: 25;

            

             A17: i in ( dom (xEk ^ cAk0)) by A3, A12, A14, FINSEQ_3: 25;

            per cases by A11, A17, FINSEQ_1: 25;

              suppose

               A18: i in ( dom xEk);

              

              hence ((xEk ^ cAk0) . i) = (xEk . i) by FINSEQ_1:def 7

              .= (xE . i) by A18, FUNCT_1: 47;

            end;

              suppose ex n be Nat st n in ( dom cAk0) & i = (k + n);

              then

              consider n be Nat such that

               A19: n in ( dom cAk0) and

               A20: i = (k + n);

              

               A21: not (E . i) in B

              proof

                assume (E . i) in B;

                then

                consider t be object such that

                 A22: t in ( dom E) & t in ( Seg k) & (E . t) = (E . i) by FUNCT_1:def 6;

                i in ( Seg k) by A16, A22, FUNCT_1:def 4;

                then

                 A23: i <= k by FINSEQ_1: 1;

                i >= k by A20, NAT_1: 11;

                then i = k by A23, XXREAL_0: 1;

                hence contradiction by A19, A20, FINSEQ_3: 25;

              end;

              (cAk0 . n) = 0 ;

              then ((xEk ^ cAk0) . i) = 0 by A11, A19, A20, FINSEQ_1:def 7;

              hence (xE . i) = ((xEk ^ cAk0) . i) by A2, A1, A4, A13, A15, A21, Th20;

            end;

          end;

          hence xE = (xEk ^ cAk0) by A12, Th16;

        end;

        assume

         A24: xE = (xEk ^ cAk0);

        

         A25: ( dom (xEk ^ cAk0)) = ( dom xE) by A3, A12, FINSEQ_3: 29;

        now

          let y be set;

          assume that

           A26: y in ( dom xE) and

           A27: not (E . y) in B;

          reconsider i = y as Nat by A26;

          i in ( dom E) by A3, A5, A26, FINSEQ_3: 29;

          then not i in ( Seg k) by A27, FUNCT_1:def 6;

          then not i in ( dom xEk) by A11, FINSEQ_1:def 3;

          then

          consider n be Nat such that

           A28: n in ( dom cAk0) & i = (k + n) by A11, A25, A26, FINSEQ_1: 25;

          (cAk0 . n) = 0 ;

          hence (xE . y) = 0 by A11, A24, A28, FINSEQ_1:def 7;

        end;

        hence x in ( Affin B) by A2, A1, A4, Th20;

      end;

    end;

    theorem :: RLAFFIN3:22

    

     Th22: for EV st k <= ( card Affv) & x in ( Affin Affv) holds x in ( Affin (Affv \ (EV .: ( Seg k)))) iff (x |-- EV) = ((k |-> 0 ) ^ ((x |-- EV) /^ k))

    proof

      let E be Enumeration of Affv;

      set cA = ( card Affv);

      set B = (E .: ( Seg k));

      set AB = (Affv \ B);

      set xE = (x |-- E);

      set xEk = (xE | k);

      set xA = (x |-- Affv);

      set k0 = (k |-> 0 );

      

       A1: AB c= Affv by XBOOLE_1: 36;

      

       A2: xE = ((xE | k) ^ (xE /^ k)) by RFINSEQ: 8;

      assume

       A3: k <= ( card Affv);

      then

       A4: ( Seg k) c= ( Seg cA) by FINSEQ_1: 5;

      

       A5: ( len xE) = cA by Th16;

      then

       A6: ( Seg cA) = ( dom xE) by FINSEQ_1:def 3;

      

       A7: ( rng E) = Affv by Def1;

      then ( len E) = cA by FINSEQ_4: 62;

      then

       A8: ( dom E) = ( dom xE) by A5, FINSEQ_3: 29;

      assume

       A9: x in ( Affin Affv);

      

       A10: ( len k0) = k & ( len xEk) = k by A3, A5, CARD_1:def 7, FINSEQ_1: 59;

      hereby

        assume

         A11: x in ( Affin AB);

        now

          let i be Nat;

          assume 1 <= i & i <= k;

          then

           A12: i in ( Seg k);

          then (E . i) in B by A8, A4, A6, FUNCT_1:def 6;

          then not (E . i) in AB by XBOOLE_0:def 5;

          then (xE . i) = 0 by A9, A1, A4, A6, A11, A12, Th20;

          hence (xEk . i) = (k0 . i) by A12, FUNCT_1: 49;

        end;

        hence xE = (k0 ^ (xE /^ k)) by A10, A2, FINSEQ_1: 14;

      end;

      assume xE = (k0 ^ (xE /^ k));

      then

       A13: xEk = k0 by A2, FINSEQ_1: 33;

      now

        let y be set;

        assume that

         A14: y in ( dom xE) and

         A15: not (E . y) in AB;

        (E . y) in Affv by A7, A8, A14, FUNCT_1:def 3;

        then (E . y) in (E .: ( Seg k)) by A15, XBOOLE_0:def 5;

        then

        consider z be object such that

         A16: z in ( dom E) and

         A17: z in ( Seg k) and

         A18: (E . z) = (E . y) by FUNCT_1:def 6;

        z = y by A8, A14, A16, A18, FUNCT_1:def 4;

        then (xEk . y) = (xE . y) by A17, FUNCT_1: 49;

        hence (xE . y) = 0 by A13;

      end;

      hence thesis by A9, A1, Th20;

    end;

    theorem :: RLAFFIN3:23

    

     Th23: ( 0* n) in Affn & (EN . ( len EN)) = ( 0* n) implies ( rng (EN | (( card Affn) -' 1))) = (Affn \ {( 0* n)}) & for A be Subset of (n -VectSp_over F_Real ) st Affn = A holds (EN | (( card Affn) -' 1)) is OrdBasis of ( Lin A)

    proof

      set A = Affn;

      set E = EN;

      assume that

       A1: ( 0* n) in A and

       A2: (E . ( len E)) = ( 0* n);

      

       A3: ( card A) >= 1 by A1, NAT_1: 14;

      set cA = (( card A) -' 1);

      

       A4: ( rng E) = A by Def1;

      cA = (( card A) - 1) by A1, NAT_1: 14, XREAL_1: 233;

      then

       A5: ( len E) = (cA + 1) by A4, FINSEQ_4: 62;

      

       A6: ( len E) = ( card A) by A4, FINSEQ_4: 62;

      

       A7: not ( 0* n) in ( rng (E | cA))

      proof

        

         A8: ( len E) in ( dom E) by A6, A3, FINSEQ_3: 25;

        assume ( 0* n) in ( rng (E | cA));

        then

        consider x be object such that

         A9: x in ( dom (E | cA)) and

         A10: ((E | cA) . x) = ( 0* n) by FUNCT_1:def 3;

        

         A11: x in ( Seg cA) by A9, RELAT_1: 57;

        x in ( dom E) & ((E | cA) . x) = (E . x) by A9, FUNCT_1: 47, RELAT_1: 57;

        then x = (cA + 1) by A2, A5, A10, A8, FUNCT_1:def 4;

        then (cA + 1) <= cA by A11, FINSEQ_1: 1;

        hence thesis by NAT_1: 13;

      end;

      E = ((E | cA) ^ <*(E . ( len E))*>) by A5, FINSEQ_3: 55;

      

      then

       A12: A = (( rng (E | cA)) \/ ( rng <*(E . ( len E))*>)) by A4, FINSEQ_1: 31

      .= (( rng (E | cA)) \/ {( 0* n)}) by A2, FINSEQ_1: 38;

      hence

       A13: (A \ {( 0* n)}) = ( rng (E | cA)) by A7, ZFMISC_1: 117;

      let A1 be Subset of (n -VectSp_over F_Real ) such that

       A14: A = A1;

      A1 c= ( [#] ( Lin A1))

      proof

        let x be object;

        assume x in A1;

        then x in ( Lin A1) by VECTSP_7: 8;

        hence thesis;

      end;

      then

      reconsider e = E as FinSequence of ( Lin A1) by A4, A14, FINSEQ_1:def 4;

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

      then (A \ {( 0* n)}) is linearly-independent by A1, RLAFFIN1: 46;

      then (A1 \ {( 0* n)}) is linearly-independent by A14, MATRTOP2: 7;

      then

       A15: ( rng (e | cA)) is linearly-independent by A14, A13, VECTSP_9: 12;

      ( [#] ( Lin A1)) = ( [#] ( Lin A)) by A14, MATRTOP2: 6

      .= ( [#] ( Lin (A \ {( 0. ( TOP-REAL n))}))) by Lm2

      .= ( [#] ( Lin (A \ {( 0* n)}))) by EUCLID: 66

      .= ( [#] ( Lin (A1 \ {( 0* n)}))) by A14, MATRTOP2: 6;

      

      then ( Lin A1) = ( Lin (A1 \ {( 0* n)})) by VECTSP_4: 29

      .= ( Lin ( rng (e | cA))) by A12, A7, A14, VECTSP_9: 17, ZFMISC_1: 117;

      then ((e | cA) is one-to-one) & ( rng (e | cA)) is Basis of ( Lin A1) by A15, FUNCT_1: 52, VECTSP_7:def 3;

      hence thesis by MATRLIN:def 2;

    end;

    

     Lm5: 0 in REAL by XREAL_0:def 1;

    theorem :: RLAFFIN3:24

    

     Th24: for A be Subset of (n -VectSp_over F_Real ) st Affn = A & ( 0* n) in Affn & (EN . ( len EN)) = ( 0* n) holds for B be OrdBasis of ( Lin A) st B = (EN | (( card Affn) -' 1)) holds for v be Element of ( Lin A) holds (v |-- B) = ((v |-- EN) | (( card Affn) -' 1))

    proof

      reconsider Z = 0 as Element of REAL by Lm5;

      set TR = ( TOP-REAL n);

      set A = Affn;

      set V = (n -VectSp_over F_Real );

      set E = EN;

      let A1 be Subset of V such that

       A1: A = A1 and

       A2: ( 0* n) in A and

       A3: (E . ( len E)) = ( 0* n);

      deffunc F( set) = Z;

      

       A4: ( Affin A) = ( [#] ( Lin A)) by A2, Th11;

      set cA = (( card A) -' 1);

      let B be OrdBasis of ( Lin A1) such that

       A5: B = (E | cA);

      

       A6: ( rng B) = (A \ {( 0* n)}) by A2, A3, A5, Th23;

      then

      reconsider rB = ( rng B) as Subset of TR;

      let v be Element of ( Lin A1);

      set vB = (v |-- B);

      consider KV be Linear_Combination of ( Lin A1) such that

       A7: v = ( Sum KV) and

       A8: ( Carrier KV) c= ( rng B) and

       A9: for k be Nat st 1 <= k & k <= ( len vB) holds (vB /. k) = (KV . (B /. k)) by MATRLIN:def 7;

      

       A10: ((v |-- E) | cA) = ((v |-- A) * (E | cA)) by RELAT_1: 83;

      ( dom (v |-- A)) = ( [#] TR) by FUNCT_2:def 1;

      then rB c= ( dom (v |-- A));

      then

       A11: ( len ((v |-- E) | cA)) = ( len B) by A5, A10, FINSEQ_2: 29;

      

       A12: ( [#] ( Lin A1)) = ( [#] ( Lin A)) by A1, MATRTOP2: 6;

      then

      reconsider RB = rB as Subset of ( Lin A);

      reconsider KR = KV as Linear_Combination of ( Lin A) by A12, MATRTOP2: 11;

      

       A13: ( Carrier KR) = ( Carrier KV) by MATRTOP2: 12;

      consider KR1 be Linear_Combination of TR such that

       A14: ( Carrier KR1) = ( Carrier KR) and

       A15: ( Sum KR1) = ( Sum KR) by RLVECT_5: 11;

      ( rng B) c= A by A6, XBOOLE_1: 36;

      then

       A16: ( Carrier KR1) c= A by A8, A13, A14;

      reconsider KR2 = (KR1 | ( [#] ( Lin A))) as Linear_Combination of ( Lin A) by MATRTOP2: 10;

      

       A17: ( Carrier KR2) = ( Carrier KR1) & ( Sum KR2) = ( Sum KR1) by A14, RLVECT_5: 10;

      reconsider KR1 as Linear_Combination of A by A16, RLVECT_2:def 6;

      reconsider ms = (1 - ( sum KR1)) as Element of REAL by XREAL_0:def 1;

      consider KR0 be Function of the carrier of TR, REAL such that

       A18: (KR0 . ( 0. TR)) = ms and

       A19: for u be Element of TR st u <> ( 0. TR) holds (KR0 . u) = F(u) from FUNCT_2:sch 6;

      reconsider KR0 as Element of ( Funcs (the carrier of TR, REAL )) by FUNCT_2: 8;

      now

        let u be VECTOR of TR;

        assume not u in {( 0. TR)};

        then u <> ( 0. TR) by TARSKI:def 1;

        hence (KR0 . u) = 0 by A19;

      end;

      then

      reconsider KR0 as Linear_Combination of TR by RLVECT_2:def 3;

      ( Carrier KR0) c= {( 0. TR)}

      proof

        let x be object;

        assume that

         A20: x in ( Carrier KR0) and

         A21: not x in {( 0. TR)};

        (KR0 . x) <> 0 & x <> ( 0. TR) by A20, A21, RLVECT_2: 19, TARSKI:def 1;

        hence thesis by A19, A20;

      end;

      then

      reconsider KR0 as Linear_Combination of {( 0. TR)} by RLVECT_2:def 6;

      

       A22: ( Carrier KR0) c= {( 0. TR)} by RLVECT_2:def 6;

      ( rng B) is Basis of ( Lin A1) by MATRLIN:def 2;

      then ( rng B) is linearly-independent by VECTSP_7:def 3;

      then ( rng B) is linearly-independent Subset of V by VECTSP_9: 11;

      then rB is linearly-independent by MATRTOP2: 7;

      then

       A23: RB is linearly-independent by RLVECT_5: 15;

      

       A24: ( len vB) = ( len B) by MATRLIN:def 7;

      

       A25: ( Sum KR0) = ((KR0 . ( 0. TR)) * ( 0. TR)) by RLVECT_2: 32

      .= ( 0. TR) by RLVECT_1: 10;

      

       A26: ( 0. TR) = ( 0* n) by EUCLID: 66;

      then {( 0. TR)} c= A by A2, ZFMISC_1: 31;

      then

      reconsider KR0 as Linear_Combination of A by RLVECT_2: 21;

      reconsider K = (KR1 + KR0) as Linear_Combination of A by RLVECT_2: 38;

      

       A27: ( sum K) = (( sum KR1) + ( sum KR0)) by RLAFFIN1: 34

      .= (( sum KR1) + (1 - ( sum KR1))) by A18, A22, RLAFFIN1: 32

      .= 1;

      ( Sum K) = (( Sum KR1) + ( Sum KR0)) by RLVECT_3: 1

      .= ( Sum KR1) by A25, RLVECT_1:def 4

      .= v by A7, A15, MATRTOP2: 12;

      then

       A28: (v |-- A) = K by A12, A4, A27, RLAFFIN1:def 7;

      now

        let k be Nat;

        reconsider Bk = (B /. k) as Element of TR by A12, RLSUB_1: 10;

        assume

         A29: 1 <= k & k <= ( len B);

        then

         A30: (vB /. k) = (KV . Bk) & k in ( dom ((v |-- E) | cA)) by A24, A9, A11, FINSEQ_3: 25;

        

         A31: k in ( dom B) by A29, FINSEQ_3: 25;

        then

         A32: Bk = (B . k) by PARTFUN1:def 6;

        then Bk in ( rng B) by A31, FUNCT_1:def 3;

        then Bk <> ( 0. TR) by A6, A26, ZFMISC_1: 56;

        then not Bk in ( Carrier KR0) by A22, TARSKI:def 1;

        then

         A33: (KR0 . Bk) = 0 by RLVECT_2: 19;

        k in ( dom vB) by A24, A29, FINSEQ_3: 25;

        then

         A34: (vB . k) = (vB /. k) by PARTFUN1:def 6;

        (K . Bk) = ((KR1 . Bk) + (KR0 . Bk)) by RLVECT_2:def 10;

        

        then (K . Bk) = (KR2 . Bk) by A12, A33, FUNCT_1: 49

        .= (KV . Bk) by A23, A8, A13, A14, A15, A17, RLVECT_5: 1;

        hence (((v |-- E) | cA) . k) = (vB . k) by A5, A28, A10, A30, A34, A32, FUNCT_1: 12;

      end;

      hence thesis by A24, A11;

    end;

    

     Lm6: for V be non empty LinearTopSpace holds for A be finite affinely-independent Subset of V holds for E be Enumeration of A holds for v be Point of V holds for Ev be Enumeration of (v + A) st Ev = (E + (( card A) |-> v)) holds for X be set holds (( transl (v,V)) .: { u where u be Point of V : u in ( Affin A) & ((u |-- E) | k) in X }) = { w where w be Point of V : w in ( Affin (v + A)) & ((w |-- Ev) | k) in X }

    proof

      let V be non empty LinearTopSpace;

      let A be finite affinely-independent Subset of V;

      let E be Enumeration of A;

      let v be Point of V;

      let Ev be Enumeration of (v + A) such that

       A1: Ev = (E + (( card A) |-> v));

      set T = ( transl (v,V));

      let X be set;

      set U = { u where u be Point of V : u in ( Affin A) & ((u |-- E) | k) in X };

      set W = { w where w be Point of V : w in ( Affin (v + A)) & ((w |-- Ev) | k) in X };

      

       A2: ( Affin (v + A)) = (v + ( Affin A)) by RLAFFIN1: 53;

      hereby

        let y be object;

        assume y in (T .: U);

        then

        consider x be object such that x in ( dom T) and

         A3: x in U and

         A4: (T . x) = y by FUNCT_1:def 6;

        consider u be Point of V such that

         A5: x = u and

         A6: u in ( Affin A) and

         A7: ((u |-- E) | k) in X by A3;

        (v + u) in { (v + t) where t be Point of V : t in ( Affin A) } by A6;

        then

         A8: (v + u) in ( Affin (v + A)) by A2, RUSUB_4:def 8;

        (u |-- E) = ((v + u) |-- Ev) by A1, A6, Th17;

        then (v + u) in W by A7, A8;

        hence y in W by A4, A5, RLTOPSP1:def 10;

      end;

      let y be object;

      assume y in W;

      then

      consider w be Point of V such that

       A9: y = w and

       A10: w in ( Affin (v + A)) and

       A11: ((w |-- Ev) | k) in X;

      w in { (v + t) where t be Point of V : t in ( Affin A) } by A2, A10, RUSUB_4:def 8;

      then

      consider u be Point of V such that

       A12: w = (v + u) and

       A13: u in ( Affin A);

      (w |-- Ev) = (u |-- E) by A1, A12, A13, Th17;

      then ( dom T) = the carrier of V & u in U by A11, A13, FUNCT_2: 52;

      then (T . u) in (T .: U) by FUNCT_1:def 6;

      hence thesis by A9, A12, RLTOPSP1:def 10;

    end;

    

     Lm7: for n, k st k <= n holds for A be non empty finite affinely-independent Subset of ( TOP-REAL n) st ( card A) = (n + 1) holds for E be Enumeration of A st (E . ( len E)) = ( 0* n) holds for P be Subset of ( TOP-REAL k), B be Subset of ( TOP-REAL n) st B = { pn : ((pn |-- E) | k) in P } holds P is open iff B is open

    proof

      let n,k be Nat such that

       A1: k <= n;

      set V = (n -VectSp_over F_Real );

      set TRn = ( TOP-REAL n);

      let A be non empty finite affinely-independent Subset of TRn;

      reconsider A1 = A as Subset of V by Lm3;

      set TRk = ( TOP-REAL k);

      set cA = (( card A) -' 1);

      assume

       A2: ( card A) = (n + 1);

      ( dim TRn) = n by Th4;

      then

       A3: ( Affin A) = ( [#] TRn) by A2, Th6;

      ( 0* n) = ( 0. TRn) by EUCLID: 66;

      then

       A4: ( Lin (A \ {( 0* n)})) = ( Lin A) by Lm2;

      let E be Enumeration of A;

      reconsider e = E as FinSequence of V by Lm3;

      

       A5: ( rng E) = A by Def1;

      then

       A6: ( len E) = ( card A) by FINSEQ_4: 62;

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

      then ( len ( FinS2MX (e | n))) = n by A2, A6, FINSEQ_1: 59;

      then

      reconsider M = ( FinS2MX (e | n)) as Matrix of n, F_Real ;

      

       A7: (( card A) - 1) = cA by NAT_1: 14, XREAL_1: 233;

      set MT = ( Mx2Tran M);

      assume

       A8: (E . ( len E)) = ( 0* n);

      let P be Subset of TRk, B be Subset of TRn;

      set PP = { v where v be Element of TRn : (v | k) in P };

      PP c= the carrier of TRn

      proof

        let x be object;

        assume x in PP;

        then ex v be Element of TRn st x = v & (v | k) in P;

        hence thesis;

      end;

      then

      reconsider PP as Subset of TRn;

      assume

       A9: B = { v where v be Element of TRn : ((v |-- E) | k) in P };

      ( card A) >= 1 by NAT_1: 14;

      then ( len E) in ( dom E) by A6, FINSEQ_3: 25;

      then

       A10: ( 0* n) in A by A8, A5, FUNCT_1:def 3;

      then

       A11: ( [#] ( Lin (A \ {( 0* n)}))) = ( [#] ( Lin (A1 \ {( 0* n)}))) & ( rng (E | cA)) = (A \ {( 0* n)}) by A8, Th23, MATRTOP2: 6;

      ( [#] ( Lin A)) = ( [#] ( Lin A1)) by MATRTOP2: 6;

      then

       A12: ( Lin ( lines M)) = ( Lin A1) by A2, A7, A4, A11, VECTSP_4: 29;

      then

      reconsider BE = (E | cA) as OrdBasis of ( Lin ( lines M)) by A8, A10, Th23;

      ( rng BE) is Basis of ( Lin ( lines M)) by MATRLIN:def 2;

      then ( rng BE) is linearly-independent by VECTSP_7:def 3;

      then

       A13: ( lines M) is linearly-independent by A2, A7, VECTSP_9: 11;

      BE = M by A2, A7;

      then M is one-to-one by MATRLIN:def 2;

      then

       A14: ( the_rank_of M) = n by A13, MATRIX13: 121;

      then ( Det M) <> ( 0. F_Real ) by MATRIX13: 83;

      then

       A15: M is invertible by LAPLACE: 34;

      MT is onto by A14, MATRTOP1: 41;

      then

       A16: ( rng MT) = the carrier of TRn by FUNCT_2:def 3;

      

       A17: B c= (MT .: PP)

      proof

        let x be object;

        assume x in B;

        then

        consider v be Element of TRn such that

         A18: x = v and

         A19: ((v |-- E) | k) in P by A9;

        consider f be object such that

         A20: f in ( dom MT) & (MT . f) = v by A16, FUNCT_1:def 3;

        ( len (v |-- E)) = (n + 1) by A2, Th16;

        then ( len ((v |-- E) | n)) = n by FINSEQ_1: 59, NAT_1: 11;

        then ((v |-- E) | n) is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

        then ((v |-- E) | n) in (n -tuples_on REAL );

        then ((v |-- E) | n) in ( REAL n) by EUCLID:def 1;

        then

         A21: ((v |-- E) | n) is Element of TRn by EUCLID: 22;

        reconsider w = v as Element of ( Lin ( lines M)) by A2, A7, A3, A10, A4, A11, Th11;

        

         A22: (((v |-- E) | n) | k) = ((v |-- E) | k) by A1, FINSEQ_1: 82;

        f = (w |-- BE) by A2, A7, A20, MATRTOP2: 17

        .= ((w |-- E) | cA) by A8, A10, A12, Th24;

        then f in PP by A2, A7, A19, A21, A22;

        hence thesis by A18, A20, FUNCT_1:def 6;

      end;

      (MT .: PP) c= B

      proof

        let y be object;

        assume y in (MT .: PP);

        then

        consider x be object such that x in ( dom MT) and

         A23: x in PP and

         A24: (MT . x) = y by FUNCT_1:def 6;

        consider f be Element of TRn such that

         A25: x = f & (f | k) in P by A23;

        reconsider MTf = (MT . f) as Element of ( Lin ( lines M)) by A2, A7, A3, A10, A4, A11, Th11;

        f = (MTf |-- BE) by A2, A7, MATRTOP2: 17

        .= ((MTf |-- E) | cA) by A8, A10, A12, Th24;

        then (f | k) = ((MTf |-- E) | k) by A1, A2, A7, FINSEQ_1: 82;

        hence thesis by A9, A24, A25;

      end;

      then

       A26: (MT .: PP) = B by A17;

      P is open iff PP is open by A1, Th7;

      hence thesis by A15, A26, TOPGRP_1: 25;

    end;

    

     Lm8: for n, k holds for A be non empty finite affinely-independent Subset of ( TOP-REAL n) st k < ( card A) holds for E be Enumeration of A st (E . ( len E)) = ( 0* n) holds for P be Subset of ( TOP-REAL k) holds for B be Subset of (( TOP-REAL n) | ( Affin A)) st B = { v where v be Element of (( TOP-REAL n) | ( Affin A)) : ((v |-- E) | k) in P } holds P is open iff B is open

    proof

      let n,k be Nat;

      set TRn = ( TOP-REAL n);

      let A be non empty finite affinely-independent Subset of TRn such that

       A1: k < ( card A);

      reconsider c1 = (( card A) - 1) as Element of NAT by NAT_1: 14, NAT_1: 21;

      set AA = ( Affin A);

      let E be Enumeration of A such that

       A2: (E . ( len E)) = ( 0* n);

      

       A3: ( rng E) = A by Def1;

      then

       A4: ( len E) = ( card A) by FINSEQ_4: 62;

      then

       A5: ( len E) >= 1 by NAT_1: 14;

      then

       A6: ( len E) in ( dom E) by FINSEQ_3: 25;

      then

       A7: ( 0* n) in ( rng E) by A2, FUNCT_1:def 3;

      

       A8: ( 0. TRn) = ( 0* n) by EUCLID: 66;

      then

       A9: ( 0. TRn) in A by A2, A3, A6, FUNCT_1:def 3;

      then

       A10: (A \ {( 0. TRn)}) is linearly-independent by RLAFFIN1: 46;

      ( card A) <= (1 + ( dim TRn)) by Th5;

      then (c1 + 1) <= (1 + n) by Th4;

      then

       A11: c1 <= n by XREAL_1: 6;

      set nc = (n -' c1);

      let P be Subset of ( TOP-REAL k);

      let B be Subset of (TRn | AA) such that

       A12: B = { v where v be Element of (TRn | AA) : ((v |-- E) | k) in P };

      

       A13: ( [#] (TRn | AA)) = AA by PRE_TOPC:def 5;

      consider F be FinSequence such that

       A14: ( rng F) = (A \ {( 0. TRn)}) and

       A15: F is one-to-one by FINSEQ_4: 58;

      set V = (n -VectSp_over F_Real );

      reconsider Bn = ( MX2FinS ( 1. ( F_Real ,n))) as OrdBasis of V by MATRLIN2: 45;

      ( len Bn) = n by MATRTOP1: 19;

      then ( len ( FinS2MX (Bn | c1))) = c1 by A11, FINSEQ_1: 59;

      then

      reconsider BnC = ( FinS2MX (Bn | c1)) as Matrix of c1, n, F_Real ;

      reconsider MBC = ( Mx2Tran BnC) as Function;

      

       A16: (c1 + 1) = ( card A);

      

       A17: ( len F) = ( card (A \ {( 0. TRn)})) by A14, A15, FINSEQ_4: 62

      .= c1 by A9, A16, STIRL2_1: 55;

      set MBc = ( Mx2Tran BnC);

      set TRc = ( TOP-REAL c1);

      

       A18: ( dom MBc) = ( [#] TRc) & (MBc . ( 0. TRc)) = ( 0. TRn) by FUNCT_2:def 1, MATRTOP1: 29;

      ( rng Bn) is Basis of V by MATRLIN:def 2;

      then ( rng Bn) is linearly-independent by VECTSP_7:def 3;

      then

       A19: ( rng (Bn | c1)) is linearly-independent by RELAT_1: 70, VECTSP_7: 1;

      reconsider F as FinSequence of TRn by A14, FINSEQ_1:def 4;

      ( [#] ( Lin ( rng (Bn | ( len F))))) c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider BF = ( [#] ( Lin ( rng (Bn | ( len F))))) as Subset of TRn by Lm3;

      

       A20: ( rng MBC) = BF by A17, MATRTOP2: 18;

      consider M be Matrix of n, F_Real such that

       A21: M is invertible and

       A22: (M | ( len F)) = F by A10, A14, A15, MATRTOP2: 19;

      set MTI = ( Mx2Tran (M ~ ));

      

       A23: ( [#] (TRn | BF)) = BF by PRE_TOPC:def 5;

      (M ~ ) is invertible by A21, MATRIX_6: 16;

      then

       A24: ( Det (M ~ )) <> ( 0. F_Real ) by LAPLACE: 34;

      then

       A25: ( the_rank_of (M ~ )) = n by MATRIX13: 83;

      then

      reconsider MTe = (MTI * E) as Enumeration of (MTI .: A) by Th15;

      

       A26: ( rng MTe) = (MTI .: A) by Def1;

      ( dom MTI) = ( [#] TRn) & MTI is one-to-one by A24, FUNCT_2:def 1, MATRTOP1: 40;

      then (A,(MTI .: A)) are_equipotent by CARD_1: 33;

      then

       A27: ( card A) = ( card (MTI .: A)) by CARD_1: 5;

      then ( len MTe) = ( len E) by A4, A26, FINSEQ_4: 62;

      then ( len E) in ( dom MTe) by A5, FINSEQ_3: 25;

      

      then

       A28: (MTe . ( len E)) = (MTI . ( 0. TRn)) by A2, A8, FUNCT_1: 12

      .= ( 0. TRn) by MATRTOP1: 29;

      set MT = ( Mx2Tran M);

      ( Affin A) = ( [#] ( Lin A)) by A3, A7, Th11

      .= ( [#] ( Lin ( rng F))) by A14, Lm2;

      then

       A29: (MT .: BF) = AA by A10, A14, A15, A21, A22, MATRTOP2: 21;

      then

       A30: ( rng (MT | BF)) = AA by RELAT_1: 115;

      

       A31: ( dom MT) = ( [#] TRn) by FUNCT_2:def 1;

      then ( dom (MT | BF)) = BF by RELAT_1: 62;

      then

      reconsider MT1 = (MT | BF) as Function of (TRn | BF), (TRn | AA) by A13, A23, A30, FUNCT_2: 1;

      reconsider MT as Function;

      

       A32: ( Det M) <> ( 0. F_Real ) by A21, LAPLACE: 34;

      then

       A33: (MT " ) = MTI by MATRTOP1: 43;

      MT1 is being_homeomorphism by A21, A29, METRIZTS: 2;

      then

       A34: (MT1 " B) is open iff B is open by TOPGRP_1: 26;

      set nc0 = (nc |-> 0 );

      set Vc1 = the set of all (v ^ nc0) where v be Element of TRc;

      

       A35: nc = (n - c1) by A11, XREAL_1: 233;

      then

       A36: n = (c1 + nc);

      

       A37: MT is one-to-one by A32, MATRTOP1: 40;

      then

       A38: (MT " AA) = BF by A29, A31, FUNCT_1: 94;

      

       A39: (MT " A) c= (MT " AA) by RELAT_1: 143, RLAFFIN1: 49;

      then

       A40: (MTI .: A) c= BF by A33, A37, A38, FUNCT_1: 85;

      Bn is one-to-one by MATRLIN:def 2;

      then (Bn | c1) is one-to-one by FUNCT_1: 52;

      then

       A41: ( the_rank_of BnC) = c1 by A19, MATRIX13: 121;

      then

       A42: MBC is one-to-one by MATRTOP1: 39;

      then

       A43: ( dom (MBC " )) = ( rng MBC) by FUNCT_1: 33;

      then

      reconsider MBCe = ((MBC " ) * MTe) as FinSequence by A20, A26, A40, FINSEQ_1: 16;

      

       A44: ( rng MBCe) = ((MBC " ) .: (MTI .: A)) by A26, RELAT_1: 127;

      (MTI .: A) is affinely-independent by A25, MATRTOP2: 24;

      then (MBc " (MTI .: A)) is affinely-independent by A41, MATRTOP2: 27;

      then

      reconsider R = ( rng MBCe) as finite affinely-independent Subset of TRc by A42, A44, FUNCT_1: 85;

      reconsider MBCe as Enumeration of R by A42, Def1;

      reconsider MBCeE = (MBc * MBCe) as Enumeration of (( Mx2Tran BnC) .: R) by A41, Th15;

      (MBC * (MBC " )) = ( id ( rng MBC)) by A42, FUNCT_1: 39;

      

      then

       A45: MBCeE = (( id ( rng MBC)) * MTe) by RELAT_1: 36

      .= MTe by A20, A26, A40, RELAT_1: 53;

      set PPP = { v where v be Element of TRc : ((v |-- MBCe) | k) in P };

      

       A46: PPP c= ( [#] TRc)

      proof

        let x be object;

        assume x in PPP;

        then ex v be Element of TRc st x = v & ((v |-- MBCe) | k) in P;

        hence thesis;

      end;

      

       A47: (MTI .: A) = (MT " A) by A33, A37, FUNCT_1: 85;

      

       A48: (MT " B) c= (MT " AA) by A13, RELAT_1: 143;

      

       A49: ((MTI .: A),R) are_equipotent by A20, A42, A43, A40, A44, CARD_1: 33;

      then

       A50: (c1 + 1) = ( card R) by A27, CARD_1: 5;

      then

       A51: k <= c1 & R is non empty by A1, NAT_1: 13;

      reconsider PPP as Subset of TRc by A46;

      set nPP = { v where v be Element of TRn : (v | c1) in PPP & v in BF };

      ( dim TRc) = c1 by Th4;

      then

       A52: ( Affin R) = ( [#] TRc) by A50, Th6;

      

       A53: (( Mx2Tran BnC) .: R) = (MBC .: ((MBC " ) .: (MTI .: A))) by A26, RELAT_1: 127

      .= ((MBC * (MBC " )) .: (MTI .: A)) by RELAT_1: 126

      .= (( id ( rng MBC)) .: (MTI .: A)) by A42, FUNCT_1: 39

      .= (MTI .: A) by A47, A38, A39, A20, FUNCT_1: 92;

      

       A54: (MT " B) c= nPP

      proof

        let x be object;

        assume

         A55: x in (MT " B);

        then

        reconsider w = x as Element of (TRn | BF) by A29, A23, A31, A37, A48, FUNCT_1: 94;

        (MT . x) in B by A55, FUNCT_1:def 7;

        then

        consider v be Element of (TRn | AA) such that

         A56: (MT . x) = v and

         A57: ((v |-- E) | k) in P by A12;

        x in ( dom MT) by A55, FUNCT_1:def 7;

        then

         A58: (MTI . v) = x by A33, A37, A56, FUNCT_1: 34;

        x in BF by A38, A48, A55;

        then

        reconsider W = x as Element of TRn;

        

         A59: v in AA by A13;

        consider u be object such that

         A60: u in ( dom MBc) and

         A61: (MBc . u) = w by A38, A48, A20, A55, FUNCT_1:def 3;

        

         A62: (W | c1) = u by A60, A61, MATRTOP1: 38;

        reconsider u as Element of TRc by A60;

        (u |-- MBCe) = (w |-- MTe) by A61, A53, A45, A41, A52, Th19

        .= (v |-- E) by A25, A58, A59, Th19;

        then u in PPP by A57;

        hence thesis by A38, A48, A55, A62;

      end;

      

       A63: BF c= Vc1

      proof

        let x be object;

        assume

         A64: x in BF;

        then

        reconsider f = x as Element of TRn;

        ( len f) = n by CARD_1:def 7;

        then ( len (f | c1)) = c1 by A11, FINSEQ_1: 59;

        then (f | c1) is c1 -element by CARD_1:def 7;

        then

         A65: (f | c1) is Element of TRc by Lm1;

        f in ( Lin ( rng (Bn | c1))) by A17, A64;

        then f = ((f | c1) ^ nc0) by MATRTOP2: 20;

        hence thesis by A65;

      end;

      Vc1 c= BF

      proof

        let x be object;

        assume x in Vc1;

        then

        consider v be Element of TRc such that

         A66: x = (v ^ nc0) and not contradiction;

        ( len v) = c1 by CARD_1:def 7;

        

        then ((v ^ (nc |-> 0 )) | c1) = ((v ^ (nc |-> 0 )) | ( dom v)) by FINSEQ_1:def 3

        .= v by FINSEQ_1: 21;

        then (v ^ (nc |-> 0 )) in ( Lin ( rng (Bn | c1))) by A35, MATRTOP2: 20;

        hence thesis by A17, A66;

      end;

      then

       A67: BF = Vc1 by A63;

      

       A68: nPP c= (MT " B)

      proof

        let x be object;

        assume x in nPP;

        then

        consider v be Element of TRn such that

         A69: x = v and

         A70: (v | c1) in PPP and

         A71: v in BF;

        consider v1 be Element of TRc such that

         A72: v = (v1 ^ nc0) by A67, A71;

        consider u be Element of TRc such that

         A73: u = (v | c1) and

         A74: ((u |-- MBCe) | k) in P by A70;

        set w = (MBc . u);

        

         A75: w = (MTI . (MT . w)) by A31, A33, A37, FUNCT_1: 34;

        ( dom MBc) = ( [#] TRc) by FUNCT_2:def 1;

        then

         A76: w in BF by A20, FUNCT_1:def 3;

        then

         A77: (MT . w) in AA by A29, A31, FUNCT_1:def 6;

        (u |-- MBCe) = (w |-- MBCeE) by A41, A52, Th19

        .= ((MT . w) |-- E) by A25, A75, A77, Th19, A53, A45;

        then

         A78: (MT . w) in B by A12, A13, A74, A77;

        consider w1 be Element of TRc such that

         A79: w = (w1 ^ nc0) by A67, A76;

        w1 = (w | ( dom w1)) by A79, FINSEQ_1: 21

        .= (w | ( Seg ( len w1))) by FINSEQ_1:def 3

        .= (w | c1) by CARD_1:def 7

        .= (v | c1) by A73, MATRTOP1: 38

        .= (v | ( Seg ( len v1))) by CARD_1:def 7

        .= (v | ( dom v1)) by FINSEQ_1:def 3

        .= v1 by A72, FINSEQ_1: 21;

        hence thesis by A31, A69, A79, A72, A78, FUNCT_1:def 7;

      end;

      

       A80: ( len MBCe) = ( len E) by A4, A50, FINSEQ_4: 62;

      then ( len E) in ( dom MBCe) by A5, FINSEQ_3: 25;

      

      then (MBCe . ( len E)) = ((MBC " ) . ( 0. TRn)) by A28, FUNCT_1: 12

      .= ( 0. TRc) by A42, A18, FUNCT_1: 34;

      then

       A81: (MBCe . ( len MBCe)) = ( 0* c1) by A80, EUCLID: 70;

      (MT1 " B) = (BF /\ (MT " B)) by FUNCT_1: 70

      .= (MT " B) by A13, A38, RELAT_1: 143, XBOOLE_1: 28;

      then (MT1 " B) = nPP by A54, A68;

      then

       A82: PPP is open iff B is open by A34, A67, A36, Th8;

      ( card R) = (c1 + 1) by A27, A49, CARD_1: 5;

      hence thesis by A81, A82, A51, Lm7;

    end;

    theorem :: RLAFFIN3:25

    

     Th25: for EN, An st k <= n & ( card Affn) = (n + 1) & An = { pn : ((pn |-- EN) | k) in Ak } holds Ak is open iff An is open

    proof

      set A = Affn;

      set AA = ( Affin A);

      set TRn = ( TOP-REAL n);

      let EN, An such that

       A1: k <= n and

       A2: ( card A) = (n + 1) and

       A3: An = { v where v be Element of TRn : ((v |-- EN) | k) in Ak };

      set E = EN;

      

       A4: ( rng E) = A by Def1;

      then

       A5: ( len E) = ( card A) by FINSEQ_4: 62;

      then

       A6: ( len E) >= 1 by A2, NAT_1: 14;

      then

       A7: ( len E) in ( dom E) by FINSEQ_3: 25;

      then (E . ( len E)) in A by A4, FUNCT_1:def 3;

      then

      reconsider EL = (E . ( len E)) as Element of TRn;

      

       A8: ( card (( - EL) + A)) = (n + 1) by A2, RLAFFIN1: 7;

      set BB = { u where u be Element of TRn : u in AA & ((u |-- E) | k) in Ak };

      

       A9: BB c= An

      proof

        let x be object;

        assume x in BB;

        then ex u be Element of TRn st x = u & u in AA & ((u |-- E) | k) in Ak;

        hence thesis by A3;

      end;

      reconsider Ev = (E + (( card A) |-> ( - EL))) as Enumeration of (( - EL) + A) by Th13;

      set TB = { w where w be Element of TRn : ((w |-- Ev) | k) in Ak };

      set T = ( transl (( - EL),TRn));

      

       A10: ( dim TRn) = n by Th4;

      then

       A11: ( [#] TRn) = AA by A2, Th6;

      An c= BB

      proof

        let x be object;

        assume x in An;

        then

        consider v be Element of TRn such that

         A12: x = v & ((v |-- E) | k) in Ak by A3;

        thus thesis by A11, A12;

      end;

      then BB = An by A9;

      then

       A13: (T .: An) = { w where w be Element of TRn : w in ( Affin (( - EL) + A)) & ((w |-- Ev) | k) in Ak } by Lm6;

      

       A14: (T .: An) c= TB

      proof

        let x be object;

        assume x in (T .: An);

        then ex w be Element of TRn st x = w & w in ( Affin (( - EL) + A)) & ((w |-- Ev) | k) in Ak by A13;

        hence thesis;

      end;

      

       A15: ( card (( - EL) + A)) = ( card A) by RLAFFIN1: 7;

      then

       A16: ( Affin (( - EL) + A)) = ( [#] TRn) by A2, A10, Th6;

      TB c= (T .: An)

      proof

        let x be object;

        assume x in TB;

        then

        consider w be Element of TRn such that

         A17: x = w & ((w |-- Ev) | k) in Ak;

        thus thesis by A16, A13, A17;

      end;

      then

       A18: (T .: An) = TB by A14;

      ( len E) in ( Seg ( card A)) by A5, A6;

      then

       A19: ((( card A) |-> ( - EL)) . ( len E)) = ( - EL) by FINSEQ_2: 57;

      

       A20: ( rng Ev) = (( - EL) + A) by Def1;

      then ( len Ev) = ( card A) by A15, FINSEQ_4: 62;

      then ( dom E) = ( dom Ev) by A5, FINSEQ_3: 29;

      

      then (Ev . ( len E)) = (EL + ( - EL)) by A7, A19, FVSUM_1: 17

      .= ( 0. TRn) by RLVECT_1: 5

      .= ( 0* n) by EUCLID: 70;

      then

       A21: (Ev . ( len Ev)) = ( 0* n) by A5, A15, A20, FINSEQ_4: 62;

      (( - EL) + A) is non empty by A2, A15;

      then (T .: An) is open iff Ak is open by A1, A21, A8, A18, Lm7;

      hence thesis by TOPGRP_1: 25;

      set TAA = (T .: AA);

      

       A22: ( rng (T | AA)) = (T .: AA) by RELAT_1: 115;

      ( dom T) = ( [#] TRn) by FUNCT_2: 52;

      then

       A23: ( dom (T | AA)) = AA by RELAT_1: 62;

      ( [#] (TRn | AA)) = AA & ( [#] (TRn | TAA)) = TAA by PRE_TOPC:def 5;

      then

      reconsider TA = (T | AA) as Function of (TRn | AA), (TRn | TAA) by A23, A22, FUNCT_2: 1;

      reconsider TAB = (TA .: An) as Subset of (TRn | TAA);

      reconsider TAB = (TA .: An) as Subset of (TRn | TAA);

    end;

    theorem :: RLAFFIN3:26

    

     Th26: for EN st k <= n & ( card Affn) = (n + 1) & An = { pn : ((pn |-- EN) | k) in Ak } holds Ak is closed iff An is closed

    proof

      set TRn = ( TOP-REAL n);

      set TRk = ( TOP-REAL k);

      set A = Affn;

      let E be Enumeration of A such that

       A1: k <= n & ( card A) = (n + 1) and

       A2: An = { v where v be Element of TRn : ((v |-- E) | k) in Ak };

      set B1 = { v where v be Element of TRn : ((v |-- E) | k) in (Ak ` ) };

      

       A3: k < ( card A) by A1, NAT_1: 13;

      

       A4: (An ` ) c= B1

      proof

        let x be object;

        assume

         A5: x in (An ` );

        then

        reconsider f = x as Element of TRn;

        set fE = (f |-- E);

        ( len fE) = ( card A) by Th16;

        then ( len (fE | k)) = k by A3, FINSEQ_1: 59;

        then

         A6: (fE | k) is Element of TRk by TOPREAL3: 46;

        assume not x in B1;

        then not (fE | k) in (Ak ` );

        then (fE | k) in Ak by A6, XBOOLE_0:def 5;

        then f in An by A2;

        hence contradiction by A5, XBOOLE_0:def 5;

      end;

      B1 c= (An ` )

      proof

        let x be object;

        assume x in B1;

        then

        consider v be Element of TRn such that

         A7: x = v and

         A8: ((v |-- E) | k) in (Ak ` );

        assume not x in (An ` );

        then v in An by A7, XBOOLE_0:def 5;

        then ex w be Element of TRn st v = w & ((w |-- E) | k) in Ak by A2;

        hence contradiction by A8, XBOOLE_0:def 5;

      end;

      then (An ` ) = B1 by A4;

      then (Ak ` ) is open iff (An ` ) is open by A1, Th25;

      hence thesis by TOPS_1: 3;

    end;

    registration

      let n;

      cluster Affine -> closed for Subset of ( TOP-REAL n);

      coherence

      proof

        set TRn = ( TOP-REAL n);

        let A be Subset of TRn;

        assume A is Affine;

        then

         A1: ( Affin A) = A by RLAFFIN1: 50;

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose

           A2: A is non empty;

          ( {} TRn) c= A;

          then

          consider Ia be affinely-independent Subset of TRn such that {} c= Ia and Ia c= A and

           A3: ( Affin Ia) = A by A1, RLAFFIN1: 60;

          consider IA be affinely-independent Subset of TRn such that

           A4: Ia c= IA and IA c= ( [#] TRn) and

           A5: ( Affin IA) = ( Affin ( [#] TRn)) by RLAFFIN1: 60;

          reconsider IB = (IA \ Ia) as affinely-independent Subset of TRn by RLAFFIN1: 43, XBOOLE_1: 36;

          set cIB = ( card IB);

          

           A6: ( dim TRn) = n by Th4;

          then

           A7: cIB <= (n + 1) by Th5;

          ( [#] TRn) is Affine by RUSUB_4: 22;

          then

           A8: ( Affin ( [#] TRn)) = ( [#] TRn) by RLAFFIN1: 50;

          then

           A9: ( card IA) = (n + 1) by A5, A6, Th6;

          Ia is non empty by A2, A3;

          then IA meets Ia by A4, XBOOLE_1: 67;

          then IA <> IB by XBOOLE_1: 83;

          then cIB <> (n + 1) by A9, CARD_2: 102, XBOOLE_1: 36;

          then

           A10: cIB < (n + 1) by A7, XXREAL_0: 1;

          then

           A11: cIB < ( card IA) by A5, A8, A6, Th6;

          set TRc = ( TOP-REAL cIB);

          

           A12: ( 0* cIB) = ( 0. TRc) by EUCLID: 66;

          then (cIB |-> 0 ) is Element of TRc by EUCLID:def 4;

          then

          reconsider P = {(cIB |-> 0 )} as Subset of TRc by ZFMISC_1: 31;

          ( 0* cIB) = (cIB |-> 0 ) by EUCLID:def 4;

          then

           A13: P is closed by A12, PCOMPS_1: 7;

          set P1 = the Enumeration of Ia;

          

           A14: ( rng P1) = Ia by Def1;

          set P2 = the Enumeration of IB;

          set P12 = (P2 ^ P1);

          

           A15: ( rng P2) = IB by Def1;

          Ia misses IB by XBOOLE_1: 79;

          then

           A16: P12 is one-to-one by A14, A15, FINSEQ_3: 91;

          (Ia \/ IB) = (Ia \/ IA) by XBOOLE_1: 39

          .= IA by A4, XBOOLE_1: 12;

          then ( rng P12) = IA by A14, A15, FINSEQ_1: 31;

          then

          reconsider P12 as Enumeration of IA by A16, Def1;

          ( len P2) = ( card IB) by A15, FINSEQ_4: 62;

          

          then

           A17: (P12 .: ( Seg cIB)) = (P12 .: ( dom P2)) by FINSEQ_1:def 3

          .= ( rng (P12 | ( dom P2))) by RELAT_1: 115

          .= ( rng P2) by FINSEQ_1: 21

          .= IB by Def1;

          set B = { v where v be Element of TRn : ((v |-- P12) | cIB) in P };

          

           A18: (IA \ IB) = (IA /\ Ia) by XBOOLE_1: 48

          .= Ia by A4, XBOOLE_1: 28;

          

           A19: ( Affin A) c= B

          proof

            let x be object;

            assume

             A20: x in ( Affin A);

            then

            reconsider v = x as Element of TRn;

            set vP = (v |-- P12);

            

             A21: vP = ((vP | cIB) ^ (vP /^ cIB)) by RFINSEQ: 8;

            vP = ((cIB |-> 0 ) ^ (vP /^ cIB)) by A1, A3, A5, A8, A18, A17, A11, A20, Th22;

            then (vP | cIB) = (cIB |-> 0 ) by A21, FINSEQ_1: 33;

            then (vP | cIB) in P by TARSKI:def 1;

            hence thesis;

          end;

          

           A22: cIB <= n by A10, NAT_1: 13;

          B c= ( Affin A)

          proof

            let x be object;

            assume x in B;

            then

            consider v be Element of TRn such that

             A23: x = v and

             A24: ((v |-- P12) | cIB) in P;

            set vP = (v |-- P12);

            (vP | cIB) = (cIB |-> 0 ) by A24, TARSKI:def 1;

            then vP = ((cIB |-> 0 ) ^ (vP /^ cIB)) by RFINSEQ: 8;

            hence thesis by A1, A3, A5, A8, A18, A17, A11, A23, Th22;

          end;

          then B = ( Affin A) by A19;

          hence thesis by A1, A9, A22, A13, Th26;

        end;

      end;

    end

    reserve pnA for Element of (( TOP-REAL n) | ( Affin Affn));

    theorem :: RLAFFIN3:27

    

     Th27: for EN holds for B be Subset of (( TOP-REAL n) | ( Affin Affn)) st k < ( card Affn) & B = { pnA : ((pnA |-- EN) | k) in Ak } holds Ak is open iff B is open

    proof

      let EN;

      set E = EN;

      set Tn = ( TOP-REAL n), Tk = ( TOP-REAL k);

      set A = Affn;

      set cA = (( card A) -' 1);

      set TcA = ( TOP-REAL cA);

      set AA = ( Affin A);

      let B be Subset of (Tn | AA) such that

       A1: k < ( card A) and

       A2: B = { v where v be Element of (Tn | AA) : ((v |-- E) | k) in Ak };

      set BB = { u where u be Element of Tn : u in AA & ((u |-- E) | k) in Ak };

      

       A3: ( [#] (Tn | AA)) = AA by PRE_TOPC:def 5;

      

       A4: BB c= B

      proof

        let x be object;

        assume x in BB;

        then

        consider u be Element of Tn such that

         A5: x = u & u in AA & ((u |-- E) | k) in Ak;

        thus thesis by A2, A3, A5;

      end;

      

       A6: A is non empty by A1;

      B c= BB

      proof

        let x be object;

        assume x in B;

        then

        consider u be Element of (Tn | AA) such that

         A7: x = u & ((u |-- E) | k) in Ak by A2;

        AA is non empty by A6;

        then u in AA by A3;

        hence thesis by A7;

      end;

      then

       A8: BB = B by A4;

      

       A9: ( rng E) = A by Def1;

      then

       A10: ( len E) = ( card A) by FINSEQ_4: 62;

      then

       A11: ( len E) >= 1 by A1, NAT_1: 14;

      then

       A12: ( len E) in ( dom E) by FINSEQ_3: 25;

      then (E . ( len E)) in A by A9, FUNCT_1:def 3;

      then

      reconsider EL = (E . ( len E)) as Element of Tn;

      ( len E) in ( Seg ( card A)) by A10, A11;

      then

       A13: ((( card A) |-> ( - EL)) . ( len E)) = ( - EL) by FINSEQ_2: 57;

      

       A14: k < ( card (( - EL) + A)) by A1, RLAFFIN1: 7;

      set T = ( transl (( - EL),Tn));

      set TAA = (T .: AA);

      

       A15: ( [#] (Tn | TAA)) = TAA by PRE_TOPC:def 5;

      

       A16: ( rng (T | AA)) = (T .: AA) by RELAT_1: 115;

      

       A17: ( dom T) = ( [#] Tn) by FUNCT_2: 52;

      then ( dom (T | AA)) = AA by RELAT_1: 62;

      then

      reconsider TA = (T | AA) as Function of (Tn | AA), (Tn | TAA) by A3, A15, A16, FUNCT_2: 1;

      reconsider TAB = (TA .: B) as Subset of (Tn | TAA);

      

       A18: TA is being_homeomorphism by METRIZTS: 2;

      reconsider Ev = (E + (( card A) |-> ( - EL))) as Enumeration of (( - EL) + A) by Th13;

      

       A19: ( card (( - EL) + A)) = ( card A) by RLAFFIN1: 7;

      then

       A20: (( - EL) + A) is non empty by A1;

      

       A21: ( rng Ev) = (( - EL) + A) by Def1;

      then ( len Ev) = ( card A) by A19, FINSEQ_4: 62;

      then ( dom E) = ( dom Ev) by A10, FINSEQ_3: 29;

      

      then (Ev . ( len E)) = (EL + ( - EL)) by A12, A13, FVSUM_1: 17

      .= ( 0. Tn) by RLVECT_1: 5

      .= ( 0* n) by EUCLID: 70;

      then

       A22: (Ev . ( len Ev)) = ( 0* n) by A10, A19, A21, FINSEQ_4: 62;

      set Tab = { w where w be Element of (Tn | TAA) : ((w |-- Ev) | k) in Ak };

      

       A23: (( - EL) + AA) = ( Affin (( - EL) + A)) by RLAFFIN1: 53;

      then

       A24: (T .: AA) = ( Affin (( - EL) + A)) by RLTOPSP1: 33;

      (TA .: B) = (T .: B) by A3, RELAT_1: 129;

      then

       A25: TAB = { w where w be Element of Tn : w in ( Affin (( - EL) + A)) & ((w |-- Ev) | k) in Ak } by A8, Lm6;

      

       A26: TAB c= Tab

      proof

        let x be object;

        assume x in TAB;

        then

        consider w be Element of Tn such that

         A27: x = w and

         A28: w in ( Affin (( - EL) + A)) and

         A29: ((w |-- Ev) | k) in Ak by A25;

        w in TAA by A23, A28, RLTOPSP1: 33;

        hence thesis by A15, A27, A29;

      end;

      

       A30: (T .: AA) is non empty by A6, A17, RELAT_1: 119;

      Tab c= TAB

      proof

        let x be object;

        assume x in Tab;

        then

        consider w be Element of (Tn | TAA) such that

         A31: x = w & ((w |-- Ev) | k) in Ak;

        w in TAA by A15, A30;

        hence thesis by A24, A25, A31;

      end;

      then TAB = Tab by A26;

      then TAB is open iff Ak is open by A24, A22, A14, A20, Lm8;

      hence thesis by A6, A18, A30, TOPGRP_1: 25;

    end;

    theorem :: RLAFFIN3:28

    

     Th28: for EN holds for B be Subset of (( TOP-REAL n) | ( Affin Affn)) st k < ( card Affn) & B = { pnA : ((pnA |-- EN) | k) in Ak } holds Ak is closed iff B is closed

    proof

      let E be Enumeration of Affn;

      set TRn = ( TOP-REAL n);

      set A = Affn;

      set AA = ( Affin A);

      let B be Subset of (TRn | AA) such that

       A1: k < ( card A) and

       A2: B = { v where v be Element of (TRn | AA) : ((v |-- E) | k) in Ak };

      set B1 = { v where v be Element of (TRn | AA) : ((v |-- E) | k) in (Ak ` ) };

      

       A3: (B ` ) c= B1

      proof

        let x be object;

        assume

         A4: x in (B ` );

        then

        reconsider v = x as Element of (TRn | AA);

        set vE = (v |-- E);

        ( len vE) = ( card A) by Th16;

        then ( len (vE | k)) = k by A1, FINSEQ_1: 59;

        then

         A5: (vE | k) in ( [#] ( TOP-REAL k)) by TOPREAL3: 46;

         not v in B by A4, XBOOLE_0:def 5;

        then not (vE | k) in Ak by A2;

        then (vE | k) in (Ak ` ) by A5, XBOOLE_0:def 5;

        hence thesis;

      end;

      

       A6: A is non empty by A1;

      B1 c= (B ` )

      proof

        let x be object;

        assume x in B1;

        then

        consider v be Element of (TRn | AA) such that

         A7: x = v and

         A8: ((v |-- E) | k) in (Ak ` );

        assume not x in (B ` );

        then v in B by A6, A7, XBOOLE_0:def 5;

        then ex w be Element of (TRn | AA) st w = v & ((w |-- E) | k) in Ak by A2;

        hence contradiction by A8, XBOOLE_0:def 5;

        set vE = (v |-- E);

      end;

      then B1 = (B ` ) by A3;

      then (Ak ` ) is open iff (B ` ) is open by A1, Th27;

      hence thesis by TOPS_1: 3;

    end;

    registration

      let n;

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

      cluster ( halfline (p,q)) -> closed;

      coherence

      proof

        set pq = {p, q};

        per cases ;

          suppose

           A1: p = q;

           {p} is closed by URYSOHN1: 19;

          hence thesis by A1, TOPREAL9: 29;

        end;

          suppose

           A2: p <> q;

          

           A3: ( rng <*p, q*>) = pq by FINSEQ_2: 127;

           <*p, q*> is one-to-one by A2, FINSEQ_3: 94;

          then

          reconsider E = <*p, q*> as Enumeration of pq by A3, Def1;

          set Apq = ( Affin pq);

          set TRn = ( TOP-REAL n), TR1 = ( TOP-REAL 1);

          set L = ]. -infty , 1.];

          

           A4: (E . 1) = p by FINSEQ_1: 44;

          reconsider L as Subset of R^1 by TOPMETR: 17;

          consider h be Function of TR1, R^1 such that

           A5: for p be Point of TR1 holds (h . p) = (p /. 1) by JORDAN2B: 1;

          set B = { w where w be Element of (TRn | Apq) : ((w |-- E) | 1) in (h " L) };

          B c= ( [#] (TRn | Apq))

          proof

            let x be object;

            assume x in B;

            then ex w be Element of (TRn | Apq) st x = w & ((w |-- E) | 1) in (h " L);

            hence thesis;

          end;

          then

          reconsider B as Subset of (TRn | Apq);

          

           A6: ( [#] (TRn | Apq)) = Apq by PRE_TOPC:def 5;

          

           A7: ( card pq) = 2 by A2, CARD_2: 57;

          

           A8: h is being_homeomorphism by A5, JORDAN2B: 28;

          then

           A9: ( dom h) = ( [#] TR1) by TOPGRP_1: 24;

          

           A10: ( halfline (p,q)) c= B

          proof

            ( Carrier (q |-- {q})) c= {q} by RLVECT_2:def 6;

            then not p in ( Carrier (q |-- {q})) by A2, TARSKI:def 1;

            then

             A11: ((q |-- {q}) . p) = 0 by RLVECT_2: 19;

             {q} is Affine by RUSUB_4: 23;

            then

             A12: ( Affin {q}) = {q} by RLAFFIN1: 50;

            let x be object;

            set W = (x |-- pq), wE = (x |-- E);

            

             A13: p in pq by TARSKI:def 2;

            assume x in ( halfline (p,q));

            then

            consider a be Real such that

             A14: x = (((1 - a) * p) + (a * q)) and

             A15: 0 <= a by TOPREAL9: 26;

            reconsider a as Real;

            q in {q} & {q} c= pq by TARSKI:def 1, ZFMISC_1: 36;

            then 0 = ((q |-- pq) . p) by A11, A12, RLAFFIN1: 77;

            

            then

             A16: ((a * (q |-- pq)) . p) = (a * 0 ) by RLVECT_2:def 11

            .= 0 ;

            pq c= ( conv pq) by CONVEX1: 41;

            then

             A17: ((p |-- pq) . p) = 1 by A13, RLAFFIN1: 72;

            

             A18: q in pq & pq c= ( Affin pq) by RLAFFIN1: 49, TARSKI:def 2;

            then W = (((1 - a) * (p |-- pq)) + (a * (q |-- pq))) by A14, A13, RLAFFIN1: 70;

            

            then (W . p) = ((((1 - a) * (p |-- pq)) . p) + ((a * (q |-- pq)) . p)) by RLVECT_2:def 10

            .= (((1 - a) * ((p |-- pq) . p)) + 0 ) by A16, RLVECT_2:def 11

            .= (1 - a) by A17;

            then (W . p) <= (1 - 0 ) by A15, XREAL_1: 10;

            then

             A19: (W . p) in L by XXREAL_1: 234;

            ((1 - a) + a) = 1;

            then

            reconsider w = x as Element of (TRn | Apq) by A6, A14, A13, A18, RLAFFIN1: 78;

            ( len wE) = 2 by A7, Th16;

            then

             A20: ( len (wE | 1)) = 1 by FINSEQ_1: 59;

            then

            reconsider wE1 = (wE | 1) as Point of ( TOP-REAL 1) by TOPREAL3: 46;

            

             A21: 1 in ( dom wE1) by A20, FINSEQ_3: 25;

            then

             A22: (wE1 /. 1) = (wE1 . 1) & (wE1 . 1) = (wE . 1) by FUNCT_1: 47, PARTFUN1:def 6;

            

             A23: 1 in ( dom wE) by A21, RELAT_1: 57;

            (h . wE1) = (wE1 /. 1) by A5;

            then (h . wE1) in L by A4, A19, A22, A23, FUNCT_1: 12;

            then wE1 in (h " L) by A9, FUNCT_1:def 7;

            then w in B;

            hence thesis;

          end;

          L is closed by BORSUK_5: 41;

          then (h " L) is closed by A8, TOPGRP_1: 24;

          then

           A24: B is closed by A7, Th28;

          B c= ( halfline (p,q))

          proof

            let x be object;

            assume x in B;

            then

            consider w be Element of (TRn | Apq) such that

             A25: x = w and

             A26: ((w |-- E) | 1) in (h " L);

            set W = (w |-- pq), wE = (w |-- E);

            reconsider wE1 = (wE | 1) as Point of TR1 by A26;

            

             A27: (h . wE1) = (wE1 /. 1) by A5;

            ( len wE1) = 1 by CARD_1:def 7;

            then

             A28: 1 in ( dom wE1) by FINSEQ_3: 25;

            then

             A29: (wE1 /. 1) = (wE1 . 1) & (wE1 . 1) = (wE . 1) by FUNCT_1: 47, PARTFUN1:def 6;

            

             A30: 1 in ( dom wE) by A28, RELAT_1: 57;

            (h . (wE | 1)) in L by A26, FUNCT_1:def 7;

            then (W . p) in L by A4, A27, A29, A30, FUNCT_1: 12;

            then (W . p) <= 1 by XXREAL_1: 234;

            then

             A31: ((W . p) - (W . p)) <= (1 - (W . p)) by XREAL_1: 9;

            

             A32: ( sum W) = 1 by A6, RLAFFIN1:def 7;

            ( Carrier W) c= pq by RLVECT_2:def 6;

            then

             A33: ( sum W) = ((W . p) + (W . q)) by A2, RLAFFIN1: 33;

            ( Sum W) = w by A6, RLAFFIN1:def 7;

            then w = (((1 - (W . q)) * p) + ((W . q) * q)) by A2, A33, A32, RLVECT_2: 33;

            hence thesis by A25, A33, A32, A31, TOPREAL9: 26;

          end;

          then ( halfline (p,q)) = B by A10;

          hence thesis by A6, A24, TSEP_1: 8;

        end;

      end;

    end

    begin

    definition

      let V;

      let A be Subset of V, x;

      :: RLAFFIN3:def3

      func |-- (A,x) -> Function of V, R^1 means

      : Def3: (it . v) = ((v |-- A) . x);

      existence

      proof

        deffunc F( object) = (($1 |-- A) . x);

        

         A1: for v be object st v in the carrier of V holds F(v) in the carrier of R^1

        proof

          let v be object such that v in the carrier of V;

          set vA = (v |-- A);

          per cases ;

            suppose x in ( dom vA);

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

            hence thesis by TOPMETR: 17;

          end;

            suppose not x in ( dom vA);

            then (vA . x) = 0 by FUNCT_1:def 2;

            hence thesis by Lm5, TOPMETR: 17;

          end;

        end;

        consider f be Function of V, R^1 such that

         A2: for v be object st v in the carrier of V holds (f . v) = F(v) from FUNCT_2:sch 2( A1);

        take f;

        let v be Element of V;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let F1,F2 be Function of V, R^1 such that

         A3: for v be Element of V holds (F1 . v) = ((v |-- A) . x) and

         A4: for v be Element of V holds (F2 . v) = ((v |-- A) . x);

        now

          let v be object;

          assume

           A5: v in the carrier of V;

          

          hence (F1 . v) = ((v |-- A) . x) by A3

          .= (F2 . v) by A4, A5;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: RLAFFIN3:29

    

     Th29: for A be Subset of V st not x in A holds ( |-- (A,x)) = (( [#] V) --> 0 )

    proof

      let A be Subset of V;

      set Ax = ( |-- (A,x));

      assume

       A1: not x in A;

       A2:

      now

        let y be object;

        assume y in ( dom Ax);

        then

         A3: (Ax . y) = ((y |-- A) . x) by Def3;

        ( Carrier (y |-- A)) c= A by RLVECT_2:def 6;

        then

         A4: not x in ( Carrier (y |-- A)) by A1;

        per cases ;

          suppose x in ( [#] V);

          hence (Ax . y) = 0 by A3, A4, RLVECT_2: 19;

        end;

          suppose not x in ( [#] V);

          then not x in ( dom (y |-- A));

          hence (Ax . y) = 0 by A3, FUNCT_1:def 2;

        end;

      end;

      ( dom Ax) = ( [#] V) by FUNCT_2:def 1;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    theorem :: RLAFFIN3:30

    for A be affinely-independent Subset of V st ( |-- (A,x)) = (( [#] V) --> 0 ) holds not x in A

    proof

      let A be affinely-independent Subset of V;

      set Ax = ( |-- (A,x));

      assume

       A1: ( |-- (A,x)) = (( [#] V) --> 0 );

      

       A2: A c= ( conv A) by RLAFFIN1: 2;

      assume

       A3: x in A;

      

      then 0 = (Ax . x) by A1, FUNCOP_1: 7

      .= ((x |-- A) . x) by A3, Def3

      .= 1 by A3, A2, RLAFFIN1: 72;

      hence contradiction;

    end;

    theorem :: RLAFFIN3:31

    

     Th31: (( |-- (Affn,x)) | ( Affin Affn)) is continuous Function of (( TOP-REAL n) | ( Affin Affn)), R^1

    proof

      reconsider Z = 0 as Element of R^1 by Lm5, TOPMETR: 17;

      set TRn = ( TOP-REAL n);

      set AA = ( Affin Affn);

      set Ax = ( |-- (Affn,x));

      set AxA = (Ax | AA);

      

       A1: (( [#] TRn) /\ AA) = AA by XBOOLE_1: 28;

      

       A2: AA = ( [#] (TRn | AA)) by PRE_TOPC:def 5;

      then

      reconsider AxA as Function of (TRn | AA), R^1 by FUNCT_2: 32;

      

       A3: ( dom AxA) = AA by A2, FUNCT_2:def 1;

      per cases ;

        suppose not x in Affn;

        then Ax = (( [#] TRn) --> Z) by Th29;

        then AxA = ((TRn | AA) --> Z) by A2, A1, FUNCOP_1: 12;

        hence thesis;

      end;

        suppose

         A4: x in Affn & ( card Affn) = 1;

        

         A5: ( rng AxA) c= the carrier of R^1 by RELAT_1:def 19;

        consider y be object such that

         A6: Affn = {y} by A4, CARD_2: 42;

        

         A7: x = y by A4, A6, TARSKI:def 1;

        then Affn is Affine by A4, A6, RUSUB_4: 23;

        then

         A8: AA = Affn by RLAFFIN1: 50;

        then (AxA . x) in ( rng AxA) by A3, A4, FUNCT_1:def 3;

        then

        reconsider b = (AxA . x) as Element of R^1 by A5;

        ( rng AxA) = {(AxA . x)} by A3, A6, A7, A8, FUNCT_1: 4;

        then AxA = ((TRn | AA) --> b) by A2, A3, FUNCOP_1: 9;

        hence thesis;

      end;

        suppose

         A9: x in Affn & ( card Affn) <> 1;

        set P2 = the Enumeration of (Affn \ {x});

        set P1 = <*x*>;

        set P12 = (P1 ^ P2);

        

         A10: ( rng P1) = {x} & ( rng P2) = (Affn \ {x}) by Def1, FINSEQ_1: 39;

        (P1 is one-to-one) & {x} misses (Affn \ {x}) by FINSEQ_3: 93, XBOOLE_1: 79;

        then

         A11: P12 is one-to-one by A10, FINSEQ_3: 91;

        ( rng P12) = (( rng P1) \/ ( rng P2)) by FINSEQ_1: 31;

        then ( rng P12) = Affn by A9, A10, ZFMISC_1: 116;

        then

        reconsider P12 as Enumeration of Affn by A11, Def1;

        set TR1 = ( TOP-REAL 1);

        consider Pro be Function of TR1, R^1 such that

         A12: for p be Element of TR1 holds (Pro . p) = (p /. 1) by JORDAN2B: 1;

        

         A13: Pro is being_homeomorphism by A12, JORDAN2B: 28;

        ( card Affn) >= 1 by A9, NAT_1: 14;

        then

         A14: ( card Affn) > 1 by A9, XXREAL_0: 1;

        now

          

           A15: ( dom P1) c= ( dom P12) by FINSEQ_1: 26;

          let P be Subset of R^1 ;

          set B = { v where v be Element of (TRn | AA) : ((v |-- P12) | 1) in (Pro " P) };

          

           A16: 1 in {1} by FINSEQ_1: 2;

          assume P is closed;

          then

           A17: (Pro " P) is closed by A13, TOPGRP_1: 24;

          

           A18: ( dom P1) = ( Seg 1) by FINSEQ_1: 38;

          

          then

           A19: (P12 . 1) = (P1 . 1) by A16, FINSEQ_1: 2, FINSEQ_1:def 7

          .= x by FINSEQ_1: 40;

          

           A20: AA is non empty by A9;

          

           A21: B c= (AxA " P)

          proof

            let y be object;

            assume y in B;

            then

            consider v be Element of (TRn | AA) such that

             A22: y = v and

             A23: ((v |-- P12) | 1) in (Pro " P);

            set vP = (v |-- P12);

            reconsider vP1 = (vP | 1) as Element of TR1 by A23;

            

             A24: v in AA by A2, A20;

            ( len vP1) = 1 by CARD_1:def 7;

            then ( dom vP1) = ( Seg 1) by FINSEQ_1:def 3;

            then

             A25: 1 in ( dom vP1);

            then

             A26: 1 in ( dom vP) by RELAT_1: 57;

            (Pro . vP1) = (vP1 /. 1) by A12

            .= (vP1 . 1) by A25, PARTFUN1:def 6

            .= (vP . 1) by A25, FUNCT_1: 47

            .= ((v |-- Affn) . x) by A19, A26, FUNCT_1: 12

            .= (Ax . v) by A24, Def3;

            then (Ax . v) in P by A23, FUNCT_1:def 7;

            then (AxA . v) in P by A2, A3, A9, FUNCT_1: 47;

            hence thesis by A2, A3, A9, A22, FUNCT_1:def 7;

          end;

          

           A27: ( dom Pro) = ( [#] TR1) by A13, TOPGRP_1: 24;

          (AxA " P) c= B

          proof

            let y be object;

            set yP = (y |-- P12);

            ( len yP) = ( card Affn) by Th16;

            then

             A28: ( len (yP | 1)) = 1 by A9, FINSEQ_1: 59, NAT_1: 14;

            then

            reconsider yP1 = (yP | 1) as Element of TR1 by TOPREAL3: 46;

            

             A29: ( dom yP1) = ( Seg 1) by A28, FINSEQ_1:def 3;

            assume

             A30: y in (AxA " P);

            then

             A31: y in ( dom AxA) by FUNCT_1:def 7;

            

            then (AxA . y) = (Ax . y) by FUNCT_1: 47

            .= ((y |-- Affn) . (P12 . 1)) by A19, A3, A31, Def3

            .= (yP . 1) by A18, A16, A15, FINSEQ_1: 2, FUNCT_1: 13

            .= (yP1 . 1) by A16, A29, FINSEQ_1: 2, FUNCT_1: 47

            .= (yP1 /. 1) by A16, A29, FINSEQ_1: 2, PARTFUN1:def 6

            .= (Pro . yP1) by A12;

            then (Pro . yP1) in P by A30, FUNCT_1:def 7;

            then yP1 in (Pro " P) by A27, FUNCT_1:def 7;

            hence thesis by A30;

          end;

          then B = (AxA " P) by A21;

          hence (AxA " P) is closed by A14, A17, Th28;

        end;

        hence thesis by PRE_TOPC:def 6;

      end;

    end;

    theorem :: RLAFFIN3:32

    

     Th32: ( card Affn) = (n + 1) implies ( |-- (Affn,x)) is continuous

    proof

      set TRn = ( TOP-REAL n);

      set AA = ( Affin Affn);

      set Ax = ( |-- (Affn,x));

      reconsider AxA = (Ax | AA) as continuous Function of (TRn | AA), R^1 by Th31;

      assume

       A1: ( card Affn) = (n + 1);

      ( dim TRn) = n by Th4;

      then

       A2: AA = ( [#] TRn) by A1, Th6;

      then

       A3: (TRn | AA) = the TopStruct of TRn by TSEP_1: 93;

      

       A4: ( dom Ax) = AA by A2, FUNCT_2:def 1;

      now

        let P be Subset of R^1 ;

        assume P is closed;

        then (AxA " P) is closed by PRE_TOPC:def 6;

        then

         A5: ((AxA " P) ` ) in the topology of the TopStruct of TRn by A3, PRE_TOPC:def 2;

        ((AxA " P) ` ) = ((Ax " P) ` ) by A4, A3, RELAT_1: 69;

        then ((Ax " P) ` ) is open by A5, PRE_TOPC:def 2;

        hence (Ax " P) is closed by TOPS_1: 3;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;

    

     Lm9: for A be affinely-independent Subset of ( TOP-REAL n) st ( card A) = (n + 1) holds ( conv A) is closed

    proof

      set L = [. 0 , 1.];

      set TRn = ( TOP-REAL n);

      let A be affinely-independent Subset of TRn;

      assume

       A1: ( card A) = (n + 1);

      reconsider L as Subset of R^1 by TOPMETR: 17;

      set E = the Enumeration of A;

      deffunc F( object) = (( |-- (A,(E . $1))) " L);

      consider f be FinSequence such that

       A2: ( len f) = (n + 1) and

       A3: for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

      

       A4: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      then

       A5: ( rng f) is non empty by A2, RELAT_1: 42;

      ( rng f) c= ( bool the carrier of TRn)

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A6: x in ( dom f) and

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

        (f . x) = F(x) by A3, A6;

        hence thesis by A7;

      end;

      then

      reconsider f as FinSequence of ( bool the carrier of TRn) by FINSEQ_1:def 4;

      

       A8: ( rng E) = A by Def1;

      then

       A9: ( len E) = ( card A) by FINSEQ_4: 62;

      

       A10: ( meet ( rng f)) c= ( conv A)

      proof

        let x be object;

        assume

         A11: x in ( meet ( rng f));

         A12:

        now

          let v be Element of TRn;

          assume v in A;

          then

          consider k be object such that

           A13: k in ( dom E) and

           A14: (E . k) = v by A8, FUNCT_1:def 3;

          

           A15: k in ( dom f) by A1, A2, A9, A4, A13, FINSEQ_1:def 3;

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

          then

           A16: ( meet ( rng f)) c= (f . k) by SETFAM_1: 3;

          

           A17: ((x |-- A) . v) = (( |-- (A,v)) . x) by A11, Def3;

          (f . k) = (( |-- (A,v)) " L) by A3, A14, A15;

          then ((x |-- A) . v) in L by A11, A17, A16, FUNCT_1:def 7;

          hence ((x |-- A) . v) >= 0 by XXREAL_1: 1;

        end;

        ( dim TRn) = n by Th4;

        then ( [#] TRn) = ( Affin A) by A1, Th6;

        hence thesis by A11, A12, RLAFFIN1: 73;

      end;

      

       A18: ( dom E) = ( Seg ( len E)) by FINSEQ_1:def 3;

      

       A19: ( conv A) c= ( meet ( rng f))

      proof

        let x be object;

        assume

         A20: x in ( conv A);

        now

          let Y be set;

          assume Y in ( rng f);

          then

          consider k be object such that

           A21: k in ( dom f) and

           A22: (f . k) = Y by FUNCT_1:def 3;

          (E . k) in A by A1, A2, A8, A9, A4, A18, A21, FUNCT_1:def 3;

          then

          reconsider Ek = (E . k) as Element of TRn;

          

           A23: ( dom ( |-- (A,Ek))) = ( [#] TRn) by FUNCT_2:def 1;

          

           A24: 0 <= ((x |-- A) . Ek) & ((x |-- A) . Ek) <= 1 by A20, RLAFFIN1: 71;

          ((x |-- A) . Ek) = (( |-- (A,Ek)) . x) by A20, Def3;

          then

           A25: (( |-- (A,Ek)) . x) in L by A24, XXREAL_1: 1;

          Y = (( |-- (A,(E . k))) " L) by A3, A21, A22;

          hence x in Y by A20, A25, A23, FUNCT_1:def 7;

        end;

        hence thesis by A5, SETFAM_1:def 1;

      end;

      now

        let B be Subset of TRn;

        assume B in ( rng f);

        then

        consider k be object such that

         A26: k in ( dom f) & (f . k) = B by FUNCT_1:def 3;

        (( |-- (A,(E . k))) is continuous) & L is closed by A1, Th32, TREAL_1: 1;

        then (( |-- (A,(E . k))) " L) is closed by PRE_TOPC:def 6;

        hence B is closed by A3, A26;

      end;

      then ( rng f) is closed by TOPS_2:def 2;

      then ( meet ( rng f)) is closed by TOPS_2: 22;

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

    end;

    registration

      let n, Affn;

      cluster ( conv Affn) -> closed;

      coherence

      proof

        set TRn = ( TOP-REAL n);

        consider I be affinely-independent Subset of TRn such that

         A1: Affn c= I and I c= ( [#] TRn) and

         A2: ( Affin I) = ( Affin ( [#] TRn)) by RLAFFIN1: 60;

        

         A3: ( dim TRn) = n by Th4;

        ( [#] TRn) is Affine by RUSUB_4: 22;

        then ( Affin I) = ( [#] TRn) by A2, RLAFFIN1: 50;

        then ( card I) = (n + 1) by A3, Th6;

        then ( conv I) is closed by Lm9;

        then (( conv I) /\ ( Affin Affn)) is closed;

        hence thesis by A1, Th9;

      end;

    end

    theorem :: RLAFFIN3:33

    ( card Affn) = (n + 1) implies ( Int Affn) is open

    proof

      set L = ]. 0 , 1.[;

      set TRn = ( TOP-REAL n);

      set A = Affn;

      assume that

       A1: ( card A) = (n + 1);

      per cases ;

        suppose

         A2: n <> 0 ;

        reconsider L as Subset of R^1 by TOPMETR: 17;

        set E = the Enumeration of A;

        deffunc F( object) = (( |-- (A,(E . $1))) " L);

        consider f be FinSequence such that

         A3: ( len f) = (n + 1) and

         A4: for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

        

         A5: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        then

         A6: ( rng f) is non empty by A3, RELAT_1: 42;

        ( rng f) c= ( bool the carrier of TRn)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A7: x in ( dom f) and

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

          (f . x) = F(x) by A4, A7;

          hence thesis by A8;

        end;

        then

        reconsider f as FinSequence of ( bool the carrier of TRn) by FINSEQ_1:def 4;

        

         A9: ( rng E) = A by Def1;

        then

         A10: ( len E) = ( card A) by FINSEQ_4: 62;

        

         A11: ( meet ( rng f)) c= ( Int A)

        proof

          let x be object;

          ( dim TRn) = n by Th4;

          then

           A12: ( [#] TRn) = ( Affin A) by A1, Th6;

          assume

           A13: x in ( meet ( rng f));

           A14:

          now

            let v be Element of TRn;

            assume v in A;

            then

            consider k be object such that

             A15: k in ( dom E) and

             A16: (E . k) = v by A9, FUNCT_1:def 3;

            

             A17: k in ( dom f) by A1, A3, A10, A5, A15, FINSEQ_1:def 3;

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

            then

             A18: ( meet ( rng f)) c= (f . k) by SETFAM_1: 3;

            

             A19: ((x |-- A) . v) = (( |-- (A,v)) . x) by A13, Def3;

            (f . k) = (( |-- (A,v)) " L) by A4, A16, A17;

            then ((x |-- A) . v) in L by A13, A19, A18, FUNCT_1:def 7;

            hence ((x |-- A) . v) > 0 by XXREAL_1: 4;

          end;

          

           A20: A c= ( Carrier (x |-- A))

          proof

            let y be object;

            assume

             A21: y in A;

            then ((x |-- A) . y) > 0 by A14;

            hence thesis by A21, RLVECT_2: 19;

          end;

          ( Carrier (x |-- A)) c= A by RLVECT_2:def 6;

          then

           A22: ( Carrier (x |-- A)) = A by A20;

          for v be Element of TRn st v in A holds ((x |-- A) . v) >= 0 by A14;

          then

           A23: x in ( conv A) by A13, A12, RLAFFIN1: 73;

          ( Sum (x |-- A)) = x by A13, A12, RLAFFIN1:def 7;

          hence thesis by A23, A22, RLAFFIN1: 71, RLAFFIN2: 12;

        end;

        

         A24: ( conv A) c= ( Affin A) by RLAFFIN1: 65;

        

         A25: ( Int A) c= ( conv A) by RLAFFIN2: 5;

        

         A26: ( dom E) = ( Seg ( len E)) by FINSEQ_1:def 3;

        

         A27: ( Int A) c= ( meet ( rng f))

        proof

          let x be object;

          assume

           A28: x in ( Int A);

          then

          consider K be Linear_Combination of A such that

           A29: K is convex and

           A30: x = ( Sum K) by RLAFFIN2: 10;

          

           A31: x in ( conv A) by A25, A28;

          ( sum K) = 1 by A29, RLAFFIN1: 62;

          then

           A32: K = (x |-- A) by A24, A30, A31, RLAFFIN1:def 7;

          

           A33: ( Carrier K) = A by A28, A29, A30, RLAFFIN2: 11;

          now

            let Y be set;

            assume Y in ( rng f);

            then

            consider k be object such that

             A34: k in ( dom f) and

             A35: (f . k) = Y by FUNCT_1:def 3;

            

             A36: (E . k) in A by A1, A3, A9, A10, A5, A26, A34, FUNCT_1:def 3;

            then

            reconsider Ek = (E . k) as Element of TRn;

            ((x |-- A) . Ek) <> 0 by A32, A33, A36, RLVECT_2: 19;

            then

             A37: 0 < ((x |-- A) . Ek) by A29, A32, RLAFFIN1: 62;

            

             A38: ((x |-- A) . Ek) < 1

            proof

              assume

               A39: ((x |-- A) . Ek) >= 1;

              ((x |-- A) . Ek) <= 1 by A29, A32, RLAFFIN1: 63;

              then A = {Ek} by A29, A32, A33, A39, RLAFFIN1: 64, XXREAL_0: 1;

              then ( card A) = 1 by CARD_2: 42;

              hence contradiction by A1, A2;

            end;

            ((x |-- A) . Ek) = (( |-- (A,Ek)) . x) by A30, Def3;

            then

             A40: (( |-- (A,Ek)) . x) in L by A38, A37, XXREAL_1: 4;

            

             A41: ( dom ( |-- (A,Ek))) = ( [#] TRn) by FUNCT_2:def 1;

            Y = (( |-- (A,(E . k))) " L) by A4, A34, A35;

            hence x in Y by A28, A40, A41, FUNCT_1:def 7;

          end;

          hence thesis by A6, SETFAM_1:def 1;

        end;

        now

          let B be Subset of TRn;

          

           A42: ( [#] R^1 ) is non empty;

          assume B in ( rng f);

          then

          consider k be object such that

           A43: k in ( dom f) & (f . k) = B by FUNCT_1:def 3;

          (( |-- (A,(E . k))) is continuous) & L is open by A1, Th32, JORDAN6: 35;

          then (( |-- (A,(E . k))) " L) is open by A42, TOPS_2: 43;

          hence B is open by A4, A43;

        end;

        then ( rng f) is open by TOPS_2:def 1;

        then ( meet ( rng f)) is open by TOPS_2: 20;

        hence thesis by A27, A11, XBOOLE_0:def 10;

      end;

        suppose

         A44: n = 0 ;

        Affn is non empty by A1;

        then

         A45: ( Int Affn) is non empty by RLAFFIN2: 20;

        the carrier of TRn = {( 0. TRn)} by A44, EUCLID: 22, EUCLID: 77;

        then ( Int Affn) = ( [#] TRn) by A45, ZFMISC_1: 33;

        hence thesis;

      end;

    end;