rlaffin1.miz



    begin

    reserve x,y for set,

r,s for Real,

S for non empty addLoopStr,

LS,LS1,LS2 for Linear_Combination of S,

G for Abelian add-associative right_zeroed right_complementable non empty addLoopStr,

LG,LG1,LG2 for Linear_Combination of G,

g,h for Element of G,

RLS for non empty RLSStruct,

R for vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct,

AR for Subset of R,

LR,LR1,LR2 for Linear_Combination of R,

V for RealLinearSpace,

v,v1,v2,w,p for VECTOR of V,

A,B for Subset of V,

F1,F2 for Subset-Family of V,

L,L1,L2 for Linear_Combination of V;

    registration

      let RLS;

      let A be empty Subset of RLS;

      cluster ( conv A) -> empty;

      coherence

      proof

        A = the empty convex Subset of RLS;

        then A in ( Convex-Family A) by CONVEX1:def 4;

        hence thesis by SETFAM_1: 4;

      end;

    end

    

     Lm1: for A be Subset of RLS holds A c= ( conv A)

    proof

      let A be Subset of RLS;

      let x be object;

      assume

       A1: x in A;

       A2:

      now

        let y;

        assume y in ( Convex-Family A);

        then A c= y by CONVEX1:def 4;

        hence x in y by A1;

      end;

      ( [#] RLS) is convex;

      then ( [#] RLS) in ( Convex-Family A) by CONVEX1:def 4;

      hence thesis by A2, SETFAM_1:def 1;

    end;

    registration

      let RLS;

      let A be non empty Subset of RLS;

      cluster ( conv A) -> non empty;

      coherence

      proof

        A c= ( conv A) by Lm1;

        hence thesis;

      end;

    end

    theorem :: RLAFFIN1:1

    for v be Element of R holds ( conv {v}) = {v}

    proof

      let v be Element of R;

       {v} is convex

      proof

        let u1,u2 be VECTOR of R, r;

        assume that 0 < r and r < 1;

        assume that

         A1: u1 in {v} and

         A2: u2 in {v};

        u1 = v & u2 = v by A1, A2, TARSKI:def 1;

        

        then ((r * u1) + ((1 - r) * u2)) = ((r + (1 - r)) * u1) by RLVECT_1:def 6

        .= u1 by RLVECT_1:def 8;

        hence thesis by A1;

      end;

      then ( conv {v}) c= {v} by CONVEX1: 30;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: RLAFFIN1:2

    for A be Subset of RLS holds A c= ( conv A) by Lm1;

    theorem :: RLAFFIN1:3

    

     Th3: for A,B be Subset of RLS st A c= B holds ( conv A) c= ( conv B)

    proof

      let A,B be Subset of RLS such that

       A1: A c= B;

      

       A2: ( Convex-Family B) c= ( Convex-Family A)

      proof

        let x be object;

        assume

         A3: x in ( Convex-Family B);

        then

        reconsider X = x as Subset of RLS;

        B c= X by A3, CONVEX1:def 4;

        then

         A4: A c= X by A1;

        X is convex by A3, CONVEX1:def 4;

        hence thesis by A4, CONVEX1:def 4;

      end;

      ( [#] RLS) is convex;

      then ( [#] RLS) in ( Convex-Family B) by CONVEX1:def 4;

      then

       A5: ( meet ( Convex-Family A)) c= ( meet ( Convex-Family B)) by A2, SETFAM_1: 6;

      let y be object;

      assume y in ( conv A);

      hence thesis by A5;

    end;

    theorem :: RLAFFIN1:4

    for S,A be Subset of RLS st A c= ( conv S) holds ( conv S) = ( conv (S \/ A))

    proof

      let S,A be Subset of RLS such that

       A1: A c= ( conv S);

      thus ( conv S) c= ( conv (S \/ A)) by Th3, XBOOLE_1: 7;

      S c= ( conv S) by Lm1;

      then (S \/ A) c= ( conv S) by A1, XBOOLE_1: 8;

      hence thesis by CONVEX1: 30;

    end;

    

     Lm2: for V be add-associative right_zeroed right_complementable non empty addLoopStr holds for A,B be Subset of V holds for v be Element of V holds ((v + A) \ (v + B)) = (v + (A \ B))

    proof

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

      let A,B be Subset of V;

      let v be Element of V;

      hereby

        let x be object;

        assume

         A1: x in ((v + A) \ (v + B));

        then x in (v + A) by XBOOLE_0:def 5;

        then

        consider w be Element of V such that

         A2: x = (v + w) and

         A3: w in A;

         not x in (v + B) by A1, XBOOLE_0:def 5;

        then not w in B by A2;

        then w in (A \ B) by A3, XBOOLE_0:def 5;

        hence x in (v + (A \ B)) by A2;

      end;

      let x be object;

      assume x in (v + (A \ B));

      then

      consider w be Element of V such that

       A4: x = (v + w) and

       A5: w in (A \ B);

      

       A6: not x in (v + B)

      proof

        assume x in (v + B);

        then

        consider s be Element of V such that

         A7: x = (v + s) and

         A8: s in B;

        s = w by A4, A7, RLVECT_1: 8;

        hence thesis by A5, A8, XBOOLE_0:def 5;

      end;

      w in A by A5, XBOOLE_0:def 5;

      then x in (v + A) by A4;

      hence thesis by A6, XBOOLE_0:def 5;

    end;

    

     Lm3: for v,w be Element of S holds {(v + w)} = (v + {w})

    proof

      let p,q be Element of S;

      hereby

        let x be object;

        assume x in {(p + q)};

        then

         A1: x = (p + q) by TARSKI:def 1;

        q in {q} by TARSKI:def 1;

        hence x in (p + {q}) by A1;

      end;

      let x be object;

      assume x in (p + {q});

      then

      consider v be Element of S such that

       A2: x = (p + v) and

       A3: v in {q};

      v = q by A3, TARSKI:def 1;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: RLAFFIN1:5

    

     Th5: for V be add-associative non empty addLoopStr holds for A be Subset of V holds for v,w be Element of V holds ((v + w) + A) = (v + (w + A))

    proof

      let V be add-associative non empty addLoopStr;

      let A be Subset of V;

      let v,w be Element of V;

      set vw = (v + w);

      thus (vw + A) c= (v + (w + A))

      proof

        let x be object;

        assume x in (vw + A);

        then

        consider s be Element of V such that

         A1: x = (vw + s) & s in A;

        (w + s) in (w + A) & x = (v + (w + s)) by A1, RLVECT_1:def 3;

        hence thesis;

      end;

      let x be object;

      assume x in (v + (w + A));

      then

      consider s be Element of V such that

       A2: x = (v + s) and

       A3: s in (w + A);

      consider r be Element of V such that

       A4: s = (w + r) and

       A5: r in A by A3;

      x = (vw + r) by A2, A4, RLVECT_1:def 3;

      hence thesis by A5;

    end;

    theorem :: RLAFFIN1:6

    

     Th6: for V be Abelian right_zeroed non empty addLoopStr holds for A be Subset of V holds (( 0. V) + A) = A

    proof

      let V be Abelian right_zeroed non empty addLoopStr;

      let A be Subset of V;

      thus (( 0. V) + A) c= A

      proof

        let x be object;

        assume x in (( 0. V) + A);

        then ex s be Element of V st x = (( 0. V) + s) & s in A;

        hence thesis by RLVECT_1:def 4;

      end;

      let x be object;

      assume

       A1: x in A;

      then

      reconsider v = x as Element of V;

      (( 0. V) + v) = v by RLVECT_1:def 4;

      hence thesis by A1;

    end;

    

     Lm4: for V be non empty addLoopStr holds for A be Subset of V holds for v be Element of V holds ( card (v + A)) c= ( card A)

    proof

      let V be non empty addLoopStr;

      let A be Subset of V;

      let v be Element of V;

      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;

      hence thesis;

    end;

    theorem :: RLAFFIN1:7

    

     Th7: for A be Subset of G holds ( card A) = ( card (g + A))

    proof

      let A be Subset of G;

      (( - g) + (g + A)) = ((( - g) + g) + A) by Th5

      .= (( 0. G) + A) by RLVECT_1: 5

      .= A by Th6;

      then

       A1: ( card A) c= ( card (g + A)) by Lm4;

      ( card (g + A)) c= ( card A) by Lm4;

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:8

    

     Th8: for v be Element of S holds (v + ( {} S)) = ( {} S)

    proof

      let v be Element of S;

      assume (v + ( {} S)) <> ( {} S);

      then

      consider x be object such that

       A1: x in (v + ( {} S)) by XBOOLE_0:def 1;

      ex w be Element of S st x = (v + w) & w in ( {} S) by A1;

      hence contradiction;

    end;

    theorem :: RLAFFIN1:9

    

     Th9: for A,B be Subset of RLS st A c= B holds (r * A) c= (r * B)

    proof

      let A,B be Subset of RLS such that

       A1: A c= B;

      let x be object;

      assume x in (r * A);

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

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:10

    

     Th10: ((r * s) * AR) = (r * (s * AR))

    proof

      set rs = (r * s);

      hereby

        let x be object;

        assume x in (rs * AR);

        then

        consider v be Element of R such that

         A1: x = (rs * v) & v in AR;

        (s * v) in (s * AR) & x = (r * (s * v)) by A1, RLVECT_1:def 7;

        hence x in (r * (s * AR));

      end;

      let x be object;

      assume x in (r * (s * AR));

      then

      consider v be Element of R such that

       A2: x = (r * v) and

       A3: v in (s * AR);

      consider w be Element of R such that

       A4: v = (s * w) and

       A5: w in AR by A3;

      (rs * w) = x by A2, A4, RLVECT_1:def 7;

      hence thesis by A5;

    end;

    theorem :: RLAFFIN1:11

    

     Th11: (1 * AR) = AR

    proof

      hereby

        let x be object;

        assume x in (1 * AR);

        then ex v be Element of R st x = (1 * v) & v in AR;

        hence x in AR by RLVECT_1:def 8;

      end;

      let x be object such that

       A1: x in AR;

      reconsider v = x as Element of R by A1;

      x = (1 * v) by RLVECT_1:def 8;

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:12

    

     Th12: ( 0 * A) c= {( 0. V)}

    proof

      let x be object;

      assume x in ( 0 * A);

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

      then x = ( 0. V) by RLVECT_1: 10;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: RLAFFIN1:13

    

     Th13: for F be FinSequence of S holds ((LS1 + LS2) * F) = ((LS1 * F) + (LS2 * F))

    proof

      let p be FinSequence of S;

      

       A1: ( len (LS1 * p)) = ( len p) by FINSEQ_2: 33;

      

       A2: ( len (LS2 * p)) = ( len p) by FINSEQ_2: 33;

      then

      reconsider L1p = (LS1 * p), L2p = (LS2 * p) as Element of (( len p) -tuples_on REAL ) by A1, FINSEQ_2: 92;

      

       A3: ( len ((LS1 + LS2) * p)) = ( len p) by FINSEQ_2: 33;

       A4:

      now

        let k be Nat;

        assume

         A5: 1 <= k & k <= ( len p);

        then k in ( dom ((LS1 + LS2) * p)) by A3, FINSEQ_3: 25;

        then

         A6: (((LS1 + LS2) * p) . k) = ((LS1 + LS2) . (p . k)) by FUNCT_1: 12;

        k in ( dom L1p) by A1, A5, FINSEQ_3: 25;

        then

         A7: (p . k) in ( dom LS1) & (L1p . k) = (LS1 . (p . k)) by FUNCT_1: 11, FUNCT_1: 12;

        k in ( dom L2p) by A2, A5, FINSEQ_3: 25;

        then

         A8: (L2p . k) = (LS2 . (p . k)) by FUNCT_1: 12;

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

        

        hence (((LS1 + LS2) * p) . k) = ((L1p . k) + (L2p . k)) by A6, A8, A7, RLVECT_2:def 10

        .= ((L1p + L2p) . k) by RVSUM_1: 11;

      end;

      ( len (L1p + L2p)) = ( len p) by CARD_1:def 7;

      hence thesis by A3, A4;

    end;

    theorem :: RLAFFIN1:14

    

     Th14: for F be FinSequence of V holds ((r * L) * F) = (r * (L * F))

    proof

      let p be FinSequence of V;

      

       A1: ( len ((r * L) * p)) = ( len p) by FINSEQ_2: 33;

      

       A2: ( len (L * p)) = ( len p) by FINSEQ_2: 33;

      then

      reconsider rLp = ((r * L) * p), Lp = (L * p) as Element of (( len p) -tuples_on REAL ) by A1, FINSEQ_2: 92;

       A3:

      now

        let k be Nat;

        assume

         A4: 1 <= k & k <= ( len p);

        then k in ( dom Lp) by A2, FINSEQ_3: 25;

        then

         A5: (Lp . k) = (L . (p . k)) & (p . k) in ( dom L) by FUNCT_1: 11, FUNCT_1: 12;

        k in ( dom rLp) by A1, A4, FINSEQ_3: 25;

        then

         A6: (rLp . k) = ((r * L) . (p . k)) by FUNCT_1: 12;

        ((r * Lp) . k) = (r * (Lp . k)) & ( dom L) = the carrier of V by FUNCT_2:def 1, RVSUM_1: 44;

        hence (rLp . k) = ((r * Lp) . k) by A5, A6, RLVECT_2:def 11;

      end;

      ( len (r * Lp)) = ( len p) by CARD_1:def 7;

      hence thesis by A1, A3;

    end;

    theorem :: RLAFFIN1:15

    

     Th15: A is linearly-independent & A c= B & ( Lin B) = V implies ex I be linearly-independent Subset of V st A c= I & I c= B & ( Lin I) = V

    proof

      assume that

       A1: A is linearly-independent & A c= B and

       A2: ( Lin B) = V;

      defpred P[ set] means (ex I be Subset of V st I = $1 & A c= I & I c= B & I is linearly-independent);

      consider Q be set such that

       A3: for Z be set holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A4:

      now

        let Z be set;

        assume that

         A5: Z <> {} and

         A6: Z c= Q and

         A7: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A8: x in X and

           A9: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A3, A6, A9;

          hence thesis by A8;

        end;

        then

        reconsider W as Subset of V;

        set y = the Element of Z;

        y in Q by A5, A6;

        then

         A10: ex I be Subset of V st I = y & A c= I & I c= B & I is linearly-independent by A3;

        

         A11: W is linearly-independent

        proof

          deffunc F( object) = { D where D be Subset of V : $1 in D & D in Z };

          let l be Linear_Combination of W;

          assume that

           A12: ( Sum l) = ( 0. V) and

           A13: ( Carrier l) <> {} ;

          consider f be Function such that

           A14: ( dom f) = ( Carrier l) and

           A15: for x be object st x in ( Carrier l) holds (f . x) = F(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A13, A14, RELAT_1: 42;

           A16:

          now

            assume {} in M;

            then

            consider x be object such that

             A17: x in ( dom f) and

             A18: (f . x) = {} by FUNCT_1:def 3;

            ( Carrier l) c= W by RLVECT_2:def 6;

            then

            consider X be set such that

             A19: x in X and

             A20: X in Z by A14, A17, TARSKI:def 4;

            reconsider X as Subset of V by A3, A6, A20;

            X in { D where D be Subset of V : x in D & D in Z } by A19, A20;

            hence contradiction by A14, A15, A17, A18;

          end;

          set F = the Choice_Function of M;

          set S = ( rng F);

          

           A21: F is Function of M, ( union M) by A16, ORDERS_1: 90;

           the Element of M in M;

          then

           A22: ( union M) <> {} by A16, ORDERS_1: 6;

          then

           A23: ( dom F) = M by FUNCT_2:def 1, A21;

           A24:

          now

            let X be set;

            assume X in S;

            then

            consider x be object such that

             A25: x in ( dom F) and

             A26: (F . x) = X by FUNCT_1:def 3;

            reconsider x as set by TARSKI: 1;

            consider y be object such that

             A27: y in ( dom f) & (f . y) = x by A23, A25, FUNCT_1:def 3;

            

             A28: x = { D where D be Subset of V : y in D & D in Z } by A14, A15, A27;

            X in x by A16, A23, A25, A26, ORDERS_1: 89;

            then ex D be Subset of V st D = X & y in D & D in Z by A28;

            hence X in Z;

          end;

           A29:

          now

            let X,Y be set;

            assume X in S & Y in S;

            then X in Z & Y in Z by A24;

            then (X,Y) are_c=-comparable by A7, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

          ( dom F) is finite by A14, A23, FINSET_1: 8;

          then S is finite by FINSET_1: 8;

          then ( union S) in S by A22, A29, CARD_2: 62, A21;

          then ( union S) in Z by A24;

          then

          consider I be Subset of V such that

           A30: I = ( union S) and A c= I and I c= B and

           A31: I is linearly-independent by A3, A6;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            assume

             A32: x in ( Carrier l);

            then

             A33: (f . x) = { D where D be Subset of V : x in D & D in Z } by A15;

            

             A34: (f . x) in M by A14, A32, FUNCT_1:def 3;

            then (F . (f . x)) in (f . x) by A16, ORDERS_1: 89;

            then

             A35: ex D be Subset of V st (F . (f . x)) = D & x in D & D in Z by A33;

            (F . (f . x)) in S by A23, A34, FUNCT_1:def 3;

            hence thesis by A35, TARSKI:def 4;

          end;

          then l is Linear_Combination of I by A30, RLVECT_2:def 6;

          hence thesis by A12, A13, A31;

        end;

        

         A36: W c= B

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A37: x in X and

           A38: X in Z by TARSKI:def 4;

          ex I be Subset of V st I = X & A c= I & I c= B & I is linearly-independent by A3, A6, A38;

          hence thesis by A37;

        end;

        y c= W by A5, ZFMISC_1: 74;

        then A c= W by A10;

        hence ( union Z) in Q by A3, A11, A36;

      end;

      Q <> {} by A1, A3;

      then

      consider X be set such that

       A39: X in Q and

       A40: for Z be set st Z in Q & Z <> X holds not X c= Z by A4, ORDERS_1: 67;

      consider I be Subset of V such that

       A41: I = X and

       A42: A c= I and

       A43: I c= B and

       A44: I is linearly-independent by A3, A39;

      reconsider I as linearly-independent Subset of V by A44;

      take I;

      thus A c= I & I c= B by A42, A43;

      assume

       A45: ( Lin I) <> V;

      now

        assume

         A46: for v st v in B holds v in ( Lin I);

        now

          let v;

          assume v in ( Lin B);

          then

          consider l be Linear_Combination of B such that

           A47: v = ( Sum l) by RLVECT_3: 14;

          ( Carrier l) c= the carrier of ( Lin I)

          proof

            let x be object;

            assume

             A48: x in ( Carrier l);

            then

            reconsider a = x as VECTOR of V;

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

            then a in ( Lin I) by A46, A48;

            hence thesis;

          end;

          then

          reconsider l as Linear_Combination of ( Up ( Lin I)) by RLVECT_2:def 6;

          ( Sum l) = v by A47;

          then v in ( Lin ( Up ( Lin I))) by RLVECT_3: 14;

          hence v in ( Lin I) by RLVECT_3: 18;

        end;

        then ( Lin B) is Subspace of ( Lin I) by RLSUB_1: 29;

        hence contradiction by A2, A45, RLSUB_1: 26;

      end;

      then

      consider v such that

       A49: v in B and

       A50: not v in ( Lin I);

      

       A51: not v in I by A50, RLVECT_3: 15;

       {v} c= B by A49, ZFMISC_1: 31;

      then

       A52: (I \/ {v}) c= B by A43, XBOOLE_1: 8;

      v in {v} by TARSKI:def 1;

      then

       A53: v in (I \/ {v}) by XBOOLE_0:def 3;

      

       A54: (I \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (I \/ {v});

        assume

         A55: ( Sum l) = ( 0. V);

        per cases ;

          suppose v in ( Carrier l);

          then

           A56: ( - (l . v)) <> 0 by RLVECT_2: 19;

          deffunc G( VECTOR of V) = ( In ( 0 , REAL ));

          deffunc F( VECTOR of V) = (l . $1);

          consider f be Function of the carrier of V, REAL such that

           A57: (f . v) = ( In ( 0 , REAL )) and

           A58: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

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

          now

            let u be Element of V;

            assume not u in (( Carrier l) \ {v});

            then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

            then (l . u) = 0 & u <> v or u = v by TARSKI:def 1;

            hence (f . u) = 0 by A57, A58;

          end;

          then

          reconsider f as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier f) c= I

          proof

            let x be object;

            assume x in ( Carrier f);

            then

            consider u be Element of V such that

             A59: u = x and

             A60: (f . u) <> 0 ;

            (f . u) = (l . u) by A57, A58, A60;

            then ( Carrier l) c= (I \/ {v}) & u in ( Carrier l) by A60, RLVECT_2:def 6;

            then u in I or u in {v} by XBOOLE_0:def 3;

            hence thesis by A57, A59, A60, TARSKI:def 1;

          end;

          then

          reconsider f as Linear_Combination of I by RLVECT_2:def 6;

          consider g be Function of the carrier of V, REAL such that

           A61: (g . v) = ( - (l . v)) and

           A62: for u be Element of V st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

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

          now

            let u be Element of V;

            assume not u in {v};

            then u <> v by TARSKI:def 1;

            hence (g . u) = 0 by A62;

          end;

          then

          reconsider g as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier g) c= {v}

          proof

            let x be object;

            assume x in ( Carrier g);

            then ex u be Element of V st x = u & (g . u) <> 0 ;

            then x = v by A62;

            hence thesis by TARSKI:def 1;

          end;

          then

          reconsider g as Linear_Combination of {v} by RLVECT_2:def 6;

          

           A63: ( Sum g) = (( - (l . v)) * v) by A61, RLVECT_2: 32;

          now

            let u be Element of V;

            now

              per cases ;

                suppose

                 A64: v = u;

                

                thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                .= (l . u) by A57, A61, A64;

              end;

                suppose

                 A65: v <> u;

                

                thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                .= ((l . u) - (g . u)) by A58, A65

                .= ((l . u) - 0 ) by A62, A65

                .= (l . u);

              end;

            end;

            hence ((f - g) . u) = (l . u);

          end;

          then (f - g) = l;

          then ( 0. V) = (( Sum f) - ( Sum g)) by A55, RLVECT_3: 4;

          

          then ( Sum f) = (( 0. V) + ( Sum g)) by RLSUB_2: 61

          .= (( - (l . v)) * v) by A63;

          then

           A66: (( - (l . v)) * v) in ( Lin I) by RLVECT_3: 14;

          ((( - (l . v)) " ) * (( - (l . v)) * v)) = (((( - (l . v)) " ) * ( - (l . v))) * v) by RLVECT_1:def 7

          .= (1 * v) by A56, XCMPLX_0:def 7

          .= v by RLVECT_1:def 8;

          hence thesis by A50, A66, RLSUB_1: 21;

        end;

          suppose

           A67: not v in ( Carrier l);

          ( Carrier l) c= I

          proof

            let x be object;

            assume

             A68: x in ( Carrier l);

            ( Carrier l) c= (I \/ {v}) by RLVECT_2:def 6;

            then x in I or x in {v} by A68, XBOOLE_0:def 3;

            hence thesis by A67, A68, TARSKI:def 1;

          end;

          then l is Linear_Combination of I by RLVECT_2:def 6;

          hence thesis by A55, RLVECT_3:def 1;

        end;

      end;

      A c= (I \/ {v}) by A42, XBOOLE_1: 10;

      then (I \/ {v}) in Q by A3, A52, A54;

      hence contradiction by A40, A41, A51, A53, XBOOLE_1: 7;

    end;

    begin

    definition

      let G, LG, g;

      :: RLAFFIN1:def1

      func g + LG -> Linear_Combination of G means

      : Def1: (it . h) = (LG . (h - g));

      existence

      proof

        deffunc G( Element of G) = (g + $1);

        set vC = { G(h) : h in ( Carrier LG) };

        

         A1: vC c= the carrier of G

        proof

          let x be object;

          assume x in vC;

          then ex h st x = G(h) & h in ( Carrier LG);

          hence thesis;

        end;

        

         A2: ( Carrier LG) is finite;

        vC is finite from FRAENKEL:sch 21( A2);

        then

        reconsider vC as finite Subset of G by A1;

        deffunc F( Element of G) = (LG . ($1 - g));

        consider f be Function of the carrier of G, REAL such that

         A3: for h holds (f . h) = F(h) from FUNCT_2:sch 4;

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

        now

          let h;

          assume

           A4: not h in vC;

          assume (f . h) <> 0 ;

          then (LG . (h - g)) <> 0 by A3;

          then

           A5: (h - g) in ( Carrier LG);

          (g + (h - g)) = ((h + ( - g)) + g) by RLVECT_1:def 11

          .= (h + (g + ( - g))) by RLVECT_1:def 3

          .= (h + ( 0. G)) by RLVECT_1:def 10

          .= h;

          hence contradiction by A4, A5;

        end;

        then

        reconsider f as Linear_Combination of G by RLVECT_2:def 3;

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let L1,L2 be Linear_Combination of G such that

         A6: for h holds (L1 . h) = (LG . (h - g)) and

         A7: for h holds (L2 . h) = (LG . (h - g));

        now

          let h;

          

          thus (L1 . h) = (LG . (h - g)) by A6

          .= (L2 . h) by A7;

        end;

        hence thesis;

      end;

    end

    theorem :: RLAFFIN1:16

    

     Th16: ( Carrier (g + LG)) = (g + ( Carrier LG))

    proof

      thus ( Carrier (g + LG)) c= (g + ( Carrier LG))

      proof

        let x be object such that

         A1: x in ( Carrier (g + LG));

        reconsider w = x as Element of G by A1;

        

         A2: ((g + LG) . w) <> 0 by A1, RLVECT_2: 19;

        

         A3: (g + (w - g)) = ((w + ( - g)) + g) by RLVECT_1:def 11

        .= (w + (g + ( - g))) by RLVECT_1:def 3

        .= (w + ( 0. G)) by RLVECT_1:def 10

        .= w;

        ((g + LG) . w) = (LG . (w - g)) by Def1;

        then (w - g) in ( Carrier LG) by A2;

        hence thesis by A3;

      end;

      let x be object;

      assume x in (g + ( Carrier LG));

      then

      consider w be Element of G such that

       A4: x = (g + w) and

       A5: w in ( Carrier LG);

      ((g + w) - g) = ((g + w) + ( - g)) by RLVECT_1:def 11

      .= ((( - g) + g) + w) by RLVECT_1:def 3

      .= (( 0. G) + w) by RLVECT_1: 5

      .= w;

      then

       A6: ((g + LG) . (g + w)) = (LG . w) by Def1;

      (LG . w) <> 0 by A5, RLVECT_2: 19;

      hence thesis by A4, A6;

    end;

    theorem :: RLAFFIN1:17

    

     Th17: (g + (LG1 + LG2)) = ((g + LG1) + (g + LG2))

    proof

      now

        let h;

        

        thus ((g + (LG1 + LG2)) . h) = ((LG1 + LG2) . (h - g)) by Def1

        .= ((LG1 . (h - g)) + (LG2 . (h - g))) by RLVECT_2:def 10

        .= (((g + LG1) . h) + (LG2 . (h - g))) by Def1

        .= (((g + LG1) . h) + ((g + LG2) . h)) by Def1

        .= (((g + LG1) + (g + LG2)) . h) by RLVECT_2:def 10;

      end;

      hence thesis;

    end;

    theorem :: RLAFFIN1:18

    (v + (r * L)) = (r * (v + L))

    proof

      now

        let w;

        

        thus ((v + (r * L)) . w) = ((r * L) . (w - v)) by Def1

        .= (r * (L . (w - v))) by RLVECT_2:def 11

        .= (r * ((v + L) . w)) by Def1

        .= ((r * (v + L)) . w) by RLVECT_2:def 11;

      end;

      hence thesis;

    end;

    theorem :: RLAFFIN1:19

    

     Th19: (g + (h + LG)) = ((g + h) + LG)

    proof

      now

        let s be Element of G;

        

        thus ((g + (h + LG)) . s) = ((h + LG) . (s - g)) by Def1

        .= (LG . ((s - g) - h)) by Def1

        .= (LG . (s - (g + h))) by RLVECT_1: 27

        .= (((g + h) + LG) . s) by Def1;

      end;

      hence thesis;

    end;

    theorem :: RLAFFIN1:20

    

     Th20: (g + ( ZeroLC G)) = ( ZeroLC G)

    proof

      ( Carrier ( ZeroLC G)) = ( {} G) by RLVECT_2:def 5;

      

      then ( {} G) = (g + ( Carrier ( ZeroLC G))) by Th8

      .= ( Carrier (g + ( ZeroLC G))) by Th16;

      hence thesis by RLVECT_2:def 5;

    end;

    theorem :: RLAFFIN1:21

    

     Th21: (( 0. G) + LG) = LG

    proof

      now

        let g;

        

        thus ((( 0. G) + LG) . g) = (LG . (g - ( 0. G))) by Def1

        .= (LG . g);

      end;

      hence thesis;

    end;

    definition

      let R, LR;

      let r be Real;

      :: RLAFFIN1:def2

      func r (*) LR -> Linear_Combination of R means

      : Def2: for v be Element of R holds (it . v) = (LR . ((r " ) * v)) if r <> 0

      otherwise it = ( ZeroLC R);

      existence

      proof

        now

          deffunc F( Element of R) = (LR . ((r " ) * $1));

          deffunc G( Element of R) = (r * $1);

          consider f be Function of the carrier of R, REAL such that

           A1: for v be Element of R holds (f . v) = F(v) from FUNCT_2:sch 4;

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

          assume

           A2: r <> 0 ;

           A3:

          now

            let v be Element of R;

            assume

             A4: not v in (r * ( Carrier LR));

            

             A5: (f . v) = (LR . ((r " ) * v)) by A1;

            

             A6: (r * ((r " ) * v)) = ((r * (r " )) * v) by RLVECT_1:def 7

            .= (1 * v) by A2, XCMPLX_0:def 7

            .= v by RLVECT_1:def 8;

            assume (f . v) <> 0 ;

            then ((r " ) * v) in ( Carrier LR) by A5;

            hence contradiction by A4, A6;

          end;

          

           A7: ( Carrier LR) is finite;

          { G(w) where w be Element of R : w in ( Carrier LR) } is finite from FRAENKEL:sch 21( A7);

          then

          reconsider f as Linear_Combination of R by A3, RLVECT_2:def 3;

          take f;

          let v be Element of R;

          (f . v) = (LR . ((r " ) * v)) by A1;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        now

          let L1,L2 be Linear_Combination of R such that

           A8: for v be Element of R holds (L1 . v) = (LR . ((r " ) * v)) and

           A9: for v be Element of R holds (L2 . v) = (LR . ((r " ) * v));

          now

            let v be Element of R;

            

            thus (L1 . v) = (LR . ((r " ) * v)) by A8

            .= (L2 . v) by A9;

          end;

          hence L1 = L2;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: RLAFFIN1:22

    

     Th22: ( Carrier (r (*) LR)) c= (r * ( Carrier LR))

    proof

      let x be object such that

       A1: x in ( Carrier (r (*) LR));

      reconsider v = x as Element of R by A1;

      

       A2: ((r (*) LR) . v) <> 0 by A1, RLVECT_2: 19;

      ( 0 qua Real (*) LR) = ( ZeroLC R) by Def2;

      then

       A3: r <> 0 by A1, RLVECT_2:def 5;

      then ((r (*) LR) . v) = (LR . ((r " ) * v)) by Def2;

      then

       A4: ((r " ) * v) in ( Carrier LR) by A2;

      (r * ((r " ) * v)) = ((r * (r " )) * v) by RLVECT_1:def 7

      .= (1 * v) by A3, XCMPLX_0:def 7

      .= v by RLVECT_1:def 8;

      hence thesis by A4;

    end;

    theorem :: RLAFFIN1:23

    

     Th23: r <> 0 implies ( Carrier (r (*) LR)) = (r * ( Carrier LR))

    proof

      assume

       A1: r <> 0 ;

      thus ( Carrier (r (*) LR)) c= (r * ( Carrier LR)) by Th22;

      let x be object;

      assume x in (r * ( Carrier LR));

      then

      consider v be Element of R such that

       A2: x = (r * v) and

       A3: v in ( Carrier LR);

      ((r " ) * (r * v)) = (((r " ) * r) * v) by RLVECT_1:def 7

      .= (1 * v) by A1, XCMPLX_0:def 7

      .= v by RLVECT_1:def 8;

      then

       A4: (LR . v) = ((r (*) LR) . x) by A1, A2, Def2;

      (LR . v) <> 0 by A3, RLVECT_2: 19;

      hence thesis by A2, A4;

    end;

    theorem :: RLAFFIN1:24

    

     Th24: (r (*) (LR1 + LR2)) = ((r (*) LR1) + (r (*) LR2))

    proof

      per cases ;

        suppose

         A1: r = 0 ;

        set Z = ( ZeroLC R);

         A2:

        now

          let v be Element of R;

          

          thus ((Z + Z) . v) = ((Z . v) + (Z . v)) by RLVECT_2:def 10

          .= ((Z . v) + 0 ) by RLVECT_2: 20

          .= (Z . v);

        end;

        

        thus (r (*) (LR1 + LR2)) = Z by A1, Def2

        .= (Z + Z) by A2

        .= ((r (*) LR1) + Z) by A1, Def2

        .= ((r (*) LR1) + (r (*) LR2)) by A1, Def2;

      end;

        suppose

         A3: r <> 0 ;

        now

          let v be Element of R;

          

          thus ((r (*) (LR1 + LR2)) . v) = ((LR1 + LR2) . ((r " ) * v)) by A3, Def2

          .= ((LR1 . ((r " ) * v)) + (LR2 . ((r " ) * v))) by RLVECT_2:def 10

          .= (((r (*) LR1) . v) + (LR2 . ((r " ) * v))) by A3, Def2

          .= (((r (*) LR1) . v) + ((r (*) LR2) . v)) by A3, Def2

          .= (((r (*) LR1) + (r (*) LR2)) . v) by RLVECT_2:def 10;

        end;

        hence thesis;

      end;

    end;

    theorem :: RLAFFIN1:25

    (r * (s (*) L)) = (s (*) (r * L))

    proof

      per cases ;

        suppose

         A1: s = 0 ;

        

        hence (r * (s (*) L)) = (r * ( ZeroLC V)) by Def2

        .= (r * ( 0 * L)) by RLVECT_2: 43

        .= ((r * 0 ) * L) by RLVECT_2: 47

        .= ( ZeroLC V) by RLVECT_2: 43

        .= (s (*) (r * L)) by A1, Def2;

      end;

        suppose

         A2: s <> 0 ;

        now

          let v;

          

          thus ((r * (s (*) L)) . v) = (r * ((s (*) L) . v)) by RLVECT_2:def 11

          .= (r * (L . ((s " ) * v))) by A2, Def2

          .= ((r * L) . ((s " ) * v)) by RLVECT_2:def 11

          .= ((s (*) (r * L)) . v) by A2, Def2;

        end;

        hence thesis;

      end;

    end;

    theorem :: RLAFFIN1:26

    

     Th26: (r (*) ( ZeroLC R)) = ( ZeroLC R)

    proof

      per cases ;

        suppose r = 0 ;

        hence thesis by Def2;

      end;

        suppose

         A1: r <> 0 ;

        now

          let v be Element of R;

          

          thus ((r (*) ( ZeroLC R)) . v) = (( ZeroLC R) . ((r " ) * v)) by A1, Def2

          .= 0 by RLVECT_2: 20

          .= (( ZeroLC R) . v) by RLVECT_2: 20;

        end;

        hence thesis;

      end;

    end;

    theorem :: RLAFFIN1:27

    

     Th27: (r (*) (s (*) LR)) = ((r * s) (*) LR)

    proof

      per cases ;

        suppose

         A1: r = 0 or s = 0 ;

        then ((r * s) (*) LR) = ( ZeroLC R) by Def2;

        hence thesis by A1, Def2, Th26;

      end;

        suppose

         A2: r <> 0 & s <> 0 ;

        now

          let v be Element of R;

          

          thus ((r (*) (s (*) LR)) . v) = ((s (*) LR) . ((r " ) * v)) by A2, Def2

          .= (LR . ((s " ) * ((r " ) * v))) by A2, Def2

          .= (LR . (((s " ) * (r " )) * v)) by RLVECT_1:def 7

          .= (LR . (((r * s) " ) * v)) by XCMPLX_1: 204

          .= (((r * s) (*) LR) . v) by A2, Def2;

        end;

        hence thesis;

      end;

    end;

    theorem :: RLAFFIN1:28

    

     Th28: (1 (*) LR) = LR

    proof

      now

        let v be Element of R;

        

        thus ((1 (*) LR) . v) = (LR . ((1 " ) * v)) by Def2

        .= (LR . v) by RLVECT_1:def 8;

      end;

      hence thesis;

    end;

    begin

    definition

      let S, LS;

      :: RLAFFIN1:def3

      func sum LS -> Real means

      : Def3: ex F be FinSequence of S st F is one-to-one & ( rng F) = ( Carrier LS) & it = ( Sum (LS * F));

      existence

      proof

        consider p be FinSequence such that

         A1: ( rng p) = ( Carrier LS) and

         A2: p is one-to-one by FINSEQ_4: 58;

        reconsider p as FinSequence of S by A1, FINSEQ_1:def 4;

        take ( Sum (LS * p));

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let S1,S2 be Real;

        given F1 be FinSequence of S such that

         A3: F1 is one-to-one and

         A4: ( rng F1) = ( Carrier LS) and

         A5: S1 = ( Sum (LS * F1));

        

         A6: ( dom (F1 " )) = ( Carrier LS) by A3, A4, FUNCT_1: 33;

        

         A7: ( len F1) = ( card ( Carrier LS)) by A3, A4, FINSEQ_4: 62;

        given F2 be FinSequence of S such that

         A8: F2 is one-to-one and

         A9: ( rng F2) = ( Carrier LS) and

         A10: S2 = ( Sum (LS * F2));

        set F12 = ((F1 " ) * F2);

        ( dom F2) = ( Seg ( len F2)) & ( len F2) = ( card ( Carrier LS)) by A8, A9, FINSEQ_1:def 3, FINSEQ_4: 62;

        then

         A11: ( dom F12) = ( Seg ( len F1)) by A6, A7, A9, RELAT_1: 27;

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

        then ( rng (F1 " )) = ( Seg ( len F1)) by A3, FUNCT_1: 33;

        then

         A12: ( rng F12) = ( Seg ( len F1)) by A6, A9, RELAT_1: 28;

        then

        reconsider F12 as Function of ( Seg ( len F1)), ( Seg ( len F1)) by A11, FUNCT_2: 1;

        

         A13: F12 is onto by A12, FUNCT_2:def 3;

        ( len (LS * F1)) = ( len F1) by FINSEQ_2: 33;

        then ( dom (LS * F1)) = ( Seg ( len F1)) by FINSEQ_1:def 3;

        then

        reconsider F12 as Permutation of ( dom (LS * F1)) by A3, A8, A13;

        ((LS * F1) * F12) = (LS * (F1 * F12)) by RELAT_1: 36

        .= (LS * ((F1 * (F1 " )) * F2)) by RELAT_1: 36

        .= (LS * (( id ( Carrier LS)) * F2)) by A3, A4, FUNCT_1: 39

        .= (LS * F2) by A9, RELAT_1: 53;

        hence S1 = S2 by A5, A10, FINSOP_1: 7;

      end;

    end

    theorem :: RLAFFIN1:29

    

     Th29: for F be FinSequence of S st ( Carrier LS) misses ( rng F) holds ( Sum (LS * F)) = 0

    proof

      let F be FinSequence of S such that

       A1: ( Carrier LS) misses ( rng F);

      set LF = (LS * F);

      set LF0 = (( len LF) |-> 0 qua Real);

       A2:

      now

        let k be Nat;

        assume

         A3: 1 <= k & k <= ( len LF);

        

         A4: k in ( dom LF) by A3, FINSEQ_3: 25;

        then k in ( dom F) by FUNCT_1: 11;

        then (F . k) in ( rng F) by FUNCT_1:def 3;

        then

         A5: ( dom LS) = the carrier of S & not (F . k) in ( Carrier LS) by A1, FUNCT_2:def 1, XBOOLE_0: 3;

        (LF . k) = (LS . (F . k)) & (F . k) in ( dom LS) by A4, FUNCT_1: 11, FUNCT_1: 12;

        hence (LF . k) = (LF0 . k) by A5;

      end;

      ( len LF0) = ( len LF) by CARD_1:def 7;

      then LF = LF0 by A2;

      hence thesis by RVSUM_1: 81;

    end;

    theorem :: RLAFFIN1:30

    

     Th30: for F be FinSequence of S st F is one-to-one & ( Carrier LS) c= ( rng F) holds ( sum LS) = ( Sum (LS * F))

    proof

      let F be FinSequence of S such that

       A1: F is one-to-one and

       A2: ( Carrier LS) c= ( rng F);

      consider G be FinSequence of S such that

       A3: G is one-to-one and

       A4: ( rng G) = ( Carrier LS) and

       A5: ( sum LS) = ( Sum (LS * G)) by Def3;

      reconsider R = ( rng G) as Subset of ( rng F) by A2, A4;

      reconsider FR = (F - R), FR1 = (F - (R ` )) as FinSequence of S by FINSEQ_3: 86;

      consider p be Permutation of ( dom F) such that

       A6: (F * p) = ((F - (R ` )) ^ (F - R)) by FINSEQ_3: 115;

      (( rng F) \ (R ` )) = ((R ` ) ` )

      .= R;

      then

       A7: ( rng FR1) = R by FINSEQ_3: 65;

      FR1 is one-to-one by A1, FINSEQ_3: 87;

      then (FR1,G) are_fiberwise_equipotent by A3, A7, RFINSEQ: 26;

      then

      consider q be Permutation of ( dom G) such that

       A8: FR1 = (G * q) by RFINSEQ: 4;

      ( len (LS * G)) = ( len G) by FINSEQ_2: 33;

      then

       A9: ( dom G) = ( dom (LS * G)) by FINSEQ_3: 29;

      ((LS * G) * q) = (LS * FR1) by A8, RELAT_1: 36;

      then

       A10: ( sum LS) = ( Sum (LS * FR1)) by A5, A9, FINSOP_1: 7;

      ( len (LS * F)) = ( len F) by FINSEQ_2: 33;

      then

       A11: ( dom F) = ( dom (LS * F)) by FINSEQ_3: 29;

      (( rng F) \ R) = ( rng FR) by FINSEQ_3: 65;

      then ( rng FR) misses ( Carrier LS) by A4, XBOOLE_1: 79;

      then

       A12: (LS * (FR1 ^ FR)) = ((LS * FR1) ^ (LS * FR)) & ( Sum (LS * FR)) = 0 by Th29, FINSEQOP: 9;

      ((LS * F) * p) = (LS * (FR1 ^ FR)) by A6, RELAT_1: 36;

      

      hence ( Sum (LS * F)) = ( Sum (LS * (FR1 ^ FR))) by A11, FINSOP_1: 7

      .= (( sum LS) + 0 ) by A10, A12, RVSUM_1: 75

      .= ( sum LS);

    end;

    theorem :: RLAFFIN1:31

    

     Th31: ( sum ( ZeroLC S)) = 0

    proof

      consider F be FinSequence of S such that F is one-to-one and

       A1: ( rng F) = ( Carrier ( ZeroLC S)) and

       A2: ( sum ( ZeroLC S)) = ( Sum (( ZeroLC S) * F)) by Def3;

      F = {} by A1, RLVECT_2:def 5;

      hence thesis by A2, RVSUM_1: 72;

    end;

    theorem :: RLAFFIN1:32

    

     Th32: for v be Element of S st ( Carrier LS) c= {v} holds ( sum LS) = (LS . v)

    proof

      let v be Element of S;

      consider p be FinSequence such that

       A1: ( rng p) = {v} and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of S by A1, FINSEQ_1:def 4;

      ( dom LS) = the carrier of S & p = <*v*> by A1, A2, FINSEQ_3: 97, FUNCT_2:def 1;

      then

       A3: (LS * p) = <*(LS . v)*> by FINSEQ_2: 34;

      assume ( Carrier LS) c= {v};

      

      hence ( sum LS) = ( Sum (LS * p)) by A1, A2, Th30

      .= (LS . v) by A3, RVSUM_1: 73;

    end;

    theorem :: RLAFFIN1:33

    for v1,v2 be Element of S st ( Carrier LS) c= {v1, v2} & v1 <> v2 holds ( sum LS) = ((LS . v1) + (LS . v2))

    proof

      let v1,v2 be Element of S;

      consider p be FinSequence such that

       A1: ( rng p) = {v1, v2} and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of S by A1, FINSEQ_1:def 4;

      assume that

       A3: ( Carrier LS) c= {v1, v2} and

       A4: v1 <> v2;

      

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

      

       A6: ( Sum <*(LS . v1)*>) = (LS . v1) by RVSUM_1: 73;

      p = <*v1, v2*> or p = <*v2, v1*> by A1, A2, A4, FINSEQ_3: 99;

      then (LS * p) = <*(LS . v1), (LS . v2)*> or (LS * p) = <*(LS . v2), (LS . v1)*> by A5, FINSEQ_2: 125;

      then ( Sum (LS * p)) = ((LS . v1) + (LS . v2)) or ( Sum (LS * p)) = ((LS . v2) + (LS . v1)) by A6, RVSUM_1: 74, RVSUM_1: 76;

      hence thesis by A1, A2, A3, Th30;

    end;

    theorem :: RLAFFIN1:34

    

     Th34: ( sum (LS1 + LS2)) = (( sum LS1) + ( sum LS2))

    proof

      set C1 = ( Carrier LS1);

      set C2 = ( Carrier LS2);

      consider p112 be FinSequence such that

       A1: ( rng p112) = (C1 \ C2) and

       A2: p112 is one-to-one by FINSEQ_4: 58;

      consider p12 be FinSequence such that

       A3: ( rng p12) = (C1 /\ C2) and

       A4: p12 is one-to-one by FINSEQ_4: 58;

      consider p211 be FinSequence such that

       A5: ( rng p211) = (C2 \ C1) and

       A6: p211 is one-to-one by FINSEQ_4: 58;

      reconsider p112, p12, p211 as FinSequence of S by A1, A3, A5, FINSEQ_1:def 4;

      (C1 \ C2) misses (C1 /\ C2) by XBOOLE_1: 89;

      then

       A7: (p112 ^ p12) is one-to-one by A1, A2, A3, A4, FINSEQ_3: 91;

      set p1 = (p112 ^ p12);

      

       A8: ( rng p1) = ((C1 \ C2) \/ (C1 /\ C2)) by A1, A3, FINSEQ_1: 31

      .= C1 by XBOOLE_1: 51;

      

      then

       A9: ( rng ((p112 ^ p12) ^ p211)) = (C1 \/ (C2 \ C1)) by A5, FINSEQ_1: 31

      .= (C1 \/ C2) by XBOOLE_1: 39;

      set p2 = (p12 ^ p211);

      

       A10: ( rng p2) = ((C1 /\ C2) \/ (C2 \ C1)) by A3, A5, FINSEQ_1: 31

      .= C2 by XBOOLE_1: 51;

      set pp = (p1 ^ p211);

      pp = (p112 ^ p2) by FINSEQ_1: 32;

      then

       A11: (LS2 * pp) = ((LS2 * p112) ^ (LS2 * p2)) by FINSEQOP: 9;

      (C2 \ C1) misses (C1 /\ C2) by XBOOLE_1: 89;

      then

       A12: (p12 ^ p211) is one-to-one by A3, A4, A5, A6, FINSEQ_3: 91;

      C2 misses (C1 \ C2) by XBOOLE_1: 79;

      then ( Sum (LS2 * p112)) = 0 by A1, Th29;

      

      then

       A13: ( Sum (LS2 * pp)) = ( 0 + ( Sum (LS2 * p2))) by A11, RVSUM_1: 75

      .= ( sum LS2) by A10, A12, Def3;

      ( len (LS1 * pp)) = ( len pp) & ( len (LS2 * pp)) = ( len pp) by FINSEQ_2: 33;

      then

      reconsider L1p = (LS1 * pp), L2p = (LS2 * pp) as Element of (( len pp) -tuples_on REAL ) by FINSEQ_2: 92;

      

       A14: ((LS1 + LS2) * pp) = (L1p + L2p) by Th13;

      

       A15: C1 misses (C2 \ C1) by XBOOLE_1: 79;

      then (LS1 * pp) = ((LS1 * p1) ^ (LS1 * p211)) & ( Sum (LS1 * p211)) = 0 by A5, Th29, FINSEQOP: 9;

      

      then

       A16: ( Sum (LS1 * pp)) = (( Sum (LS1 * p1)) + 0 ) by RVSUM_1: 75

      .= ( sum LS1) by A7, A8, Def3;

      

       A17: ( Carrier (LS1 + LS2)) c= (C1 \/ C2)

      proof

        let x be object;

        assume x in ( Carrier (LS1 + LS2));

        then

        consider u be Element of S such that

         A18: x = u and

         A19: ((LS1 + LS2) . u) <> 0 ;

        ((LS1 + LS2) . u) = ((LS1 . u) + (LS2 . u)) by RLVECT_2:def 10;

        then (LS1 . u) <> 0 or (LS2 . u) <> 0 by A19;

        then x in C1 or x in C2 by A18;

        hence thesis by XBOOLE_0:def 3;

      end;

      ((p112 ^ p12) ^ p211) is one-to-one by A5, A6, A7, A8, A15, FINSEQ_3: 91;

      

      hence ( sum (LS1 + LS2)) = ( Sum (L1p + L2p)) by A9, A14, A17, Th30

      .= (( sum LS1) + ( sum LS2)) by A13, A16, RVSUM_1: 89;

    end;

    theorem :: RLAFFIN1:35

    

     Th35: ( sum (r * L)) = (r * ( sum L))

    proof

      consider F be FinSequence of V such that

       A1: F is one-to-one and

       A2: ( rng F) = ( Carrier L) and

       A3: ( sum L) = ( Sum (L * F)) by Def3;

      L is Linear_Combination of ( Carrier L) by RLVECT_2:def 6;

      then (r * L) is Linear_Combination of ( Carrier L) by RLVECT_2: 44;

      then

       A4: ( Carrier (r * L)) c= ( rng F) by A2, RLVECT_2:def 6;

      

      thus (r * ( sum L)) = ( Sum (r * (L * F))) by A3, RVSUM_1: 87

      .= ( Sum ((r * L) * F)) by Th14

      .= ( sum (r * L)) by A1, A4, Th30;

    end;

    theorem :: RLAFFIN1:36

    

     Th36: ( sum (L1 - L2)) = (( sum L1) - ( sum L2))

    proof

      

      thus ( sum (L1 - L2)) = (( sum L1) + ( sum (( - 1) * L2))) by Th34

      .= (( sum L1) + (( - 1) * ( sum L2))) by Th35

      .= (( sum L1) - ( sum L2));

    end;

    theorem :: RLAFFIN1:37

    

     Th37: ( sum LG) = ( sum (g + LG))

    proof

      set gL = (g + LG);

      deffunc F( Element of G) = ($1 + g);

      consider f be Function of the carrier of G, the carrier of G such that

       A1: for h holds (f . h) = F(h) from FUNCT_2:sch 4;

      consider F be FinSequence of G such that

       A2: F is one-to-one and

       A3: ( rng F) = ( Carrier LG) and

       A4: ( sum LG) = ( Sum (LG * F)) by Def3;

      

       A5: ( len (f * F)) = ( len F) by FINSEQ_2: 33;

      

       A6: ( len (LG * F)) = ( len F) by FINSEQ_2: 33;

      

       A7: ( len (gL * (f * F))) = ( len (f * F)) by FINSEQ_2: 33;

       A8:

      now

        let k be Nat;

        assume

         A9: 1 <= k & k <= ( len F);

        then k in ( dom F) by FINSEQ_3: 25;

        then

         A10: (F /. k) = (F . k) by PARTFUN1:def 6;

        k in ( dom (LG * F)) by A6, A9, FINSEQ_3: 25;

        then

         A11: ((LG * F) . k) = (LG . (F . k)) by FUNCT_1: 12;

        k in ( dom (gL * (f * F))) by A5, A7, A9, FINSEQ_3: 25;

        then

         A12: ((gL * (f * F)) . k) = (gL . ((f * F) . k)) by FUNCT_1: 12;

        k in ( dom (f * F)) by A5, A9, FINSEQ_3: 25;

        then ((f * F) . k) = (f . (F . k)) by FUNCT_1: 12;

        then ((f * F) . k) = ((F /. k) + g) by A1, A10;

        

        hence ((gL * (f * F)) . k) = (LG . (((F /. k) + g) - g)) by A12, Def1

        .= (LG . (((F /. k) + g) + ( - g))) by RLVECT_1:def 11

        .= (LG . ((F /. k) + (g + ( - g)))) by RLVECT_1:def 3

        .= (LG . ((F /. k) + ( 0. G))) by RLVECT_1:def 10

        .= ((LG * F) . k) by A10, A11;

      end;

      now

        let x1,x2 be object such that

         A13: x1 in ( dom (f * F)) and

         A14: x2 in ( dom (f * F)) and

         A15: ((f * F) . x1) = ((f * F) . x2);

        

         A16: (f . (F /. x1)) = ((F /. x1) + g) by A1;

        

         A17: x1 in ( dom F) by A13, FUNCT_1: 11;

        then

         A18: (F . x1) = (F /. x1) by PARTFUN1:def 6;

        

         A19: x2 in ( dom F) by A14, FUNCT_1: 11;

        then

         A20: (F . x2) = (F /. x2) by PARTFUN1:def 6;

        ((f * F) . x1) = (f . (F . x1)) & ((f * F) . x2) = (f . (F . x2)) by A13, A14, FUNCT_1: 12;

        then ((F /. x1) + g) = ((F /. x2) + g) by A1, A15, A16, A18, A20;

        then (F /. x1) = (F /. x2) by RLVECT_1: 8;

        hence x1 = x2 by A2, A17, A18, A19, A20, FUNCT_1:def 4;

      end;

      then

       A21: (f * F) is one-to-one by FUNCT_1:def 4;

      ( Carrier gL) c= ( rng (f * F))

      proof

        let x be object;

        assume x in ( Carrier gL);

        then x in (g + ( Carrier LG)) by Th16;

        then

        consider h such that

         A22: x = (g + h) and

         A23: h in ( Carrier LG);

        consider y be object such that

         A24: y in ( dom F) and

         A25: (F . y) = h by A3, A23, FUNCT_1:def 3;

        

         A26: (f . (F . y)) = x by A1, A22, A25;

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

        then

         A27: y in ( dom (f * F)) by A24, A25, FUNCT_1: 11;

        then ((f * F) . y) in ( rng (f * F)) by FUNCT_1:def 3;

        hence thesis by A26, A27, FUNCT_1: 12;

      end;

      then ( sum gL) = ( Sum (gL * (f * F))) by A21, Th30;

      hence thesis by A4, A5, A6, A7, A8, FINSEQ_1: 14;

    end;

    theorem :: RLAFFIN1:38

    

     Th38: r <> 0 implies ( sum LR) = ( sum (r (*) LR))

    proof

      set rL = (r (*) LR);

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

      consider f be Function of the carrier of R, the carrier of R such that

       A1: for v be Element of R holds (f . v) = F(v) from FUNCT_2:sch 4;

      consider F be FinSequence of R such that

       A2: F is one-to-one and

       A3: ( rng F) = ( Carrier LR) and

       A4: ( sum LR) = ( Sum (LR * F)) by Def3;

      assume

       A5: r <> 0 ;

      now

        let x1,x2 be object such that

         A6: x1 in ( dom (f * F)) and

         A7: x2 in ( dom (f * F)) and

         A8: ((f * F) . x1) = ((f * F) . x2);

        

         A9: (f . (F /. x1)) = (r * (F /. x1)) by A1;

        

         A10: x1 in ( dom F) by A6, FUNCT_1: 11;

        then

         A11: (F . x1) = (F /. x1) by PARTFUN1:def 6;

        

         A12: x2 in ( dom F) by A7, FUNCT_1: 11;

        then

         A13: (F . x2) = (F /. x2) by PARTFUN1:def 6;

        ((f * F) . x1) = (f . (F . x1)) & ((f * F) . x2) = (f . (F . x2)) by A6, A7, FUNCT_1: 12;

        then

         A14: (r * (F /. x1)) = (r * (F /. x2)) by A1, A8, A9, A11, A13;

        (F /. x1) = (1 * (F /. x1)) by RLVECT_1:def 8

        .= (((r " ) * r) * (F /. x1)) by A5, XCMPLX_0:def 7

        .= ((r " ) * (r * (F /. x2))) by A14, RLVECT_1:def 7

        .= (((r " ) * r) * (F /. x2)) by RLVECT_1:def 7

        .= (1 * (F /. x2)) by A5, XCMPLX_0:def 7

        .= (F /. x2) by RLVECT_1:def 8;

        hence x1 = x2 by A2, A10, A11, A12, A13, FUNCT_1:def 4;

      end;

      then

       A15: (f * F) is one-to-one by FUNCT_1:def 4;

      

       A16: ( len (LR * F)) = ( len F) by FINSEQ_2: 33;

      

       A17: ( len (f * F)) = ( len F) by FINSEQ_2: 33;

      

       A18: ( len (rL * (f * F))) = ( len (f * F)) by FINSEQ_2: 33;

      now

        let k be Nat;

        assume

         A19: 1 <= k & k <= ( len F);

        then k in ( dom F) by FINSEQ_3: 25;

        then

         A20: (F /. k) = (F . k) by PARTFUN1:def 6;

        k in ( dom (LR * F)) by A16, A19, FINSEQ_3: 25;

        then

         A21: ((LR * F) . k) = (LR . (F . k)) by FUNCT_1: 12;

        k in ( dom (f * F)) by A17, A19, FINSEQ_3: 25;

        then

         A22: ((f * F) . k) = (f . (F . k)) by FUNCT_1: 12;

        k in ( dom (rL * (f * F))) by A17, A18, A19, FINSEQ_3: 25;

        then ((rL * (f * F)) . k) = (rL . ((f * F) . k)) by FUNCT_1: 12;

        

        hence ((rL * (f * F)) . k) = (rL . (r * (F /. k))) by A1, A20, A22

        .= (LR . ((r " ) * (r * (F /. k)))) by A5, Def2

        .= (LR . (((r " ) * r) * (F /. k))) by RLVECT_1:def 7

        .= (LR . (1 * (F /. k))) by A5, XCMPLX_0:def 7

        .= ((LR * F) . k) by A20, A21, RLVECT_1:def 8;

      end;

      then

       A23: (LR * F) = (rL * (f * F)) by A16, A17, A18;

      ( Carrier rL) c= ( rng (f * F))

      proof

        let x be object;

        assume x in ( Carrier rL);

        then x in (r * ( Carrier LR)) by A5, Th23;

        then

        consider v be Element of R such that

         A24: x = (r * v) and

         A25: v in ( Carrier LR);

        consider y be object such that

         A26: y in ( dom F) and

         A27: (F . y) = v by A3, A25, FUNCT_1:def 3;

        

         A28: (f . v) = x by A1, A24;

        

         A29: ( dom F) = ( dom (f * F)) by A17, FINSEQ_3: 29;

        then ((f * F) . y) = (f . v) by A26, A27, FUNCT_1: 12;

        hence thesis by A26, A28, A29, FUNCT_1:def 3;

      end;

      hence thesis by A4, A15, A23, Th30;

    end;

    theorem :: RLAFFIN1:39

    

     Th39: ( Sum (v + L)) = ((( sum L) * v) + ( Sum L))

    proof

      defpred P[ Nat] means for L be Linear_Combination of V st ( card ( Carrier L)) <= $1 holds ( Sum (v + L)) = ((( sum L) * v) + ( Sum L));

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: P[n];

        let L be Linear_Combination of V such that

         A3: ( card ( Carrier L)) <= (n + 1);

        per cases by A3, NAT_1: 8;

          suppose ( card ( Carrier L)) <= n;

          hence thesis by A2;

        end;

          suppose

           A4: ( card ( Carrier L)) = (n + 1);

          then ( Carrier L) is non empty;

          then

          consider w be object such that

           A5: w in ( Carrier L);

          reconsider w as Element of V by A5;

          

           A6: ( card (( Carrier L) \ {w})) = n by A4, A5, STIRL2_1: 55;

          consider Lw be Linear_Combination of {w} such that

           A7: (Lw . w) = (L . w) by RLVECT_4: 37;

          set LLw = (L - Lw);

          (LLw . w) = ((L . w) - (Lw . w)) by RLVECT_2: 54

          .= 0 by A7;

          then

           A8: not w in ( Carrier LLw) by RLVECT_2: 19;

          

           A9: ( Carrier Lw) c= {w} by RLVECT_2:def 6;

          then

           A10: ( Carrier LLw) c= (( Carrier L) \/ ( Carrier Lw)) & (( Carrier L) \/ ( Carrier Lw)) c= (( Carrier L) \/ {w}) by RLVECT_2: 55, XBOOLE_1: 9;

          (( Carrier L) \/ {w}) = ( Carrier L) by A5, ZFMISC_1: 40;

          then ( Carrier LLw) c= ( Carrier L) by A10;

          then ( card ( Carrier LLw)) <= n by A8, A6, NAT_1: 43, ZFMISC_1: 34;

          then

           A11: ( Sum (v + LLw)) = ((( sum LLw) * v) + ( Sum LLw)) by A2;

          

           A12: (LLw + Lw) = (L + (Lw - Lw)) by RLVECT_2: 40

          .= (L + ( ZeroLC V)) by RLVECT_2: 57

          .= L by RLVECT_2: 41;

          

          then

           A13: ( Sum L) = (( Sum LLw) + ( Sum Lw)) by RLVECT_3: 1

          .= (( Sum LLw) + ((Lw . w) * w)) by RLVECT_2: 32;

          (v + ( Carrier Lw)) c= (v + {w}) by A9, RLTOPSP1: 8;

          then (v + ( Carrier Lw)) c= {(v + w)} by Lm3;

          then ( Carrier (v + Lw)) c= {(v + w)} by Th16;

          then (v + Lw) is Linear_Combination of {(v + w)} by RLVECT_2:def 6;

          

          then

           A14: ( Sum (v + Lw)) = (((v + Lw) . (v + w)) * (v + w)) by RLVECT_2: 32

          .= ((Lw . ((v + w) - v)) * (v + w)) by Def1

          .= ((Lw . w) * (v + w)) by RLVECT_4: 1;

          

           A15: ( sum L) = (( sum LLw) + ( sum Lw)) by A12, Th34

          .= (( sum LLw) + (Lw . w)) by A9, Th32;

          (v + L) = ((v + LLw) + (v + Lw)) by A12, Th17;

          

          hence ( Sum (v + L)) = (( Sum (v + LLw)) + ( Sum (v + Lw))) by RLVECT_3: 1

          .= (((( sum LLw) * v) + ( Sum LLw)) + (((Lw . w) * v) + ((Lw . w) * w))) by A11, A14, RLVECT_1:def 5

          .= ((((( sum LLw) * v) + ( Sum LLw)) + ((Lw . w) * v)) + ((Lw . w) * w)) by RLVECT_1:def 3

          .= ((((( sum LLw) * v) + ((Lw . w) * v)) + ( Sum LLw)) + ((Lw . w) * w)) by RLVECT_1:def 3

          .= (((( sum L) * v) + ( Sum LLw)) + ((Lw . w) * w)) by A15, RLVECT_1:def 6

          .= ((( sum L) * v) + ( Sum L)) by A13, RLVECT_1:def 3;

        end;

      end;

      

       A16: P[ 0 qua Nat]

      proof

        let L be Linear_Combination of V;

        assume ( card ( Carrier L)) <= 0 ;

        then

         A17: ( Carrier L) = ( {} V);

        then

         A18: L = ( ZeroLC V) & ( Sum L) = ( 0. V) by RLVECT_2: 34, RLVECT_2:def 5;

        (v + ( Carrier L)) = {} by A17, Th8;

        then ( Carrier (v + L)) = {} by Th16;

        

        hence ( Sum (v + L)) = ( 0. V) by RLVECT_2: 34

        .= (( 0. V) + ( 0. V))

        .= ((( sum L) * v) + ( Sum L)) by A18, Th31, RLVECT_1: 10;

      end;

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

      then P[( card ( Carrier L))];

      hence thesis;

    end;

    theorem :: RLAFFIN1:40

    

     Th40: ( Sum (r (*) L)) = (r * ( Sum L))

    proof

      defpred P[ Nat] means for L be Linear_Combination of V st ( card ( Carrier L)) <= $1 holds ( Sum (r (*) L)) = (r * ( Sum L));

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: P[n];

        let L be Linear_Combination of V such that

         A3: ( card ( Carrier L)) <= (n + 1);

        per cases ;

          suppose r = 0 ;

          then (r (*) L) = ( ZeroLC V) & (r * ( Sum L)) = ( 0. V) by Def2, RLVECT_1: 10;

          hence thesis by RLVECT_2: 30;

        end;

          suppose

           A4: r <> 0 ;

          per cases by A3, NAT_1: 8;

            suppose ( card ( Carrier L)) <= n;

            hence thesis by A2;

          end;

            suppose

             A5: ( card ( Carrier L)) = (n + 1);

            then ( Carrier L) <> {} ;

            then

            consider p be object such that

             A6: p in ( Carrier L) by XBOOLE_0:def 1;

            reconsider p as Element of V by A6;

            

             A7: ( card (( Carrier L) \ {p})) = n by A5, A6, STIRL2_1: 55;

            consider Lp be Linear_Combination of {p} such that

             A8: (Lp . p) = (L . p) by RLVECT_4: 37;

            set LLp = (L - Lp);

            (LLp . p) = ((L . p) - (Lp . p)) by RLVECT_2: 54

            .= 0 by A8;

            then

             A9: not p in ( Carrier LLp) by RLVECT_2: 19;

            

             A10: ( Carrier Lp) c= {p} by RLVECT_2:def 6;

            then

             A11: ( Carrier LLp) c= (( Carrier L) \/ ( Carrier Lp)) & (( Carrier L) \/ ( Carrier Lp)) c= (( Carrier L) \/ {p}) by RLVECT_2: 55, XBOOLE_1: 9;

            (r * ( Carrier Lp)) c= {(r * p)}

            proof

              let x be object;

              assume x in (r * ( Carrier Lp));

              then

              consider w be Element of V such that

               A12: x = (r * w) and

               A13: w in ( Carrier Lp);

              w = p by A10, A13, TARSKI:def 1;

              hence thesis by A12, TARSKI:def 1;

            end;

            then ( Carrier (r (*) Lp)) c= {(r * p)} by A4, Th23;

            then (r (*) Lp) is Linear_Combination of {(r * p)} by RLVECT_2:def 6;

            

            then

             A14: ( Sum (r (*) Lp)) = (((r (*) Lp) . (r * p)) * (r * p)) by RLVECT_2: 32

            .= ((Lp . ((r " ) * (r * p))) * (r * p)) by A4, Def2

            .= ((Lp . (((r " ) * r) * p)) * (r * p)) by RLVECT_1:def 7

            .= ((Lp . (1 * p)) * (r * p)) by A4, XCMPLX_0:def 7

            .= ((Lp . p) * (r * p)) by RLVECT_1:def 8;

            

             A15: (LLp + Lp) = (L + (Lp - Lp)) by RLVECT_2: 40

            .= (L + ( ZeroLC V)) by RLVECT_2: 57

            .= L by RLVECT_2: 41;

            

            then

             A16: ( Sum L) = (( Sum LLp) + ( Sum Lp)) by RLVECT_3: 1

            .= (( Sum LLp) + ((Lp . p) * p)) by RLVECT_2: 32;

            (( Carrier L) \/ {p}) = ( Carrier L) by A6, ZFMISC_1: 40;

            then ( Carrier LLp) c= ( Carrier L) by A11;

            then ( card ( Carrier LLp)) <= n by A9, A7, NAT_1: 43, ZFMISC_1: 34;

            then

             A17: ( Sum (r (*) LLp)) = (r * ( Sum LLp)) by A2;

            (r (*) L) = ((r (*) LLp) + (r (*) Lp)) by A15, Th24;

            

            hence ( Sum (r (*) L)) = (( Sum (r (*) LLp)) + ( Sum (r (*) Lp))) by RLVECT_3: 1

            .= ((r * ( Sum LLp)) + (((Lp . p) * r) * p)) by A14, A17, RLVECT_1:def 7

            .= ((r * ( Sum LLp)) + (r * ((Lp . p) * p))) by RLVECT_1:def 7

            .= (r * ( Sum L)) by A16, RLVECT_1:def 5;

          end;

        end;

      end;

      

       A18: P[ 0 qua Nat]

      proof

        let L;

        assume ( card ( Carrier L)) <= 0 ;

        then ( Carrier L) = {} ;

        then

         A19: L = ( ZeroLC V) by RLVECT_2:def 5;

        then (r * ( 0. V)) = ( 0. V) & ( Sum L) = ( 0. V) by RLVECT_2: 30;

        hence thesis by A19, Th26;

      end;

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

      then P[( card ( Carrier L))];

      hence thesis;

    end;

    begin

    definition

      let V, A;

      :: RLAFFIN1:def4

      attr A is affinely-independent means A is empty or ex v st v in A & ((( - v) + A) \ {( 0. V)}) is linearly-independent;

    end

    registration

      let V;

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

      coherence ;

      let v;

      cluster {v} -> affinely-independent;

      coherence

      proof

         {v} is affinely-independent

        proof

          assume {v} is non empty;

          take v;

          thus v in {v} by TARSKI:def 1;

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

          then (( - v) + {v}) = {( 0. V)} by Lm3;

          then ((( - v) + {v}) \ {( 0. V)}) = ( {} the carrier of V) by XBOOLE_1: 37;

          hence thesis by RLVECT_3: 7;

        end;

        hence thesis;

      end;

      let w;

      cluster {v, w} -> affinely-independent;

      coherence

      proof

        per cases ;

          suppose v = w;

          then {v, w} = {w} by ENUMSET1: 29;

          hence thesis;

        end;

          suppose

           A1: v <> w;

          (( - v) + {v, w}) c= {(( - v) + w), ( 0. V)}

          proof

            let x be object;

            assume x in (( - v) + {v, w});

            then

            consider r be Element of V such that

             A2: x = (( - v) + r) and

             A3: r in {v, w};

            per cases by A3, TARSKI:def 2;

              suppose r = v;

              then x = ( 0. V) by A2, RLVECT_1: 5;

              hence thesis by TARSKI:def 2;

            end;

              suppose r = w;

              hence thesis by A2, TARSKI:def 2;

            end;

          end;

          then

           A4: ((( - v) + {v, w}) \ {( 0. V)}) c= ( {(( - v) + w), ( 0. V)} \ {( 0. V)}) by XBOOLE_1: 33;

          ( - ( - v)) = v;

          then

           A5: (w + ( - v)) <> ( 0. V) by A1, RLVECT_1: 6;

          then

           A6: {(( - v) + w)} is linearly-independent by RLVECT_3: 8;

           {v, w} is affinely-independent

          proof

            assume {v, w} is non empty;

            take v;

            thus v in {v, w} by TARSKI:def 2;

            ( 0. V) in {( 0. V)} & not (( - v) + w) in {( 0. V)} by A5, TARSKI:def 1;

            then ((( - v) + {v, w}) \ {( 0. V)}) c= {(( - v) + w)} by A4, ZFMISC_1: 62;

            hence thesis by A6, RLVECT_3: 5;

          end;

          hence thesis;

        end;

      end;

    end

    registration

      let V;

      cluster 1 -element affinely-independent for Subset of V;

      existence

      proof

        take { the Element of V};

        thus thesis;

      end;

    end

    

     Lm5: for A st A is affinely-independent holds for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {}

    proof

      let A;

      assume

       A1: A is affinely-independent;

      let L be Linear_Combination of A such that

       A2: ( Sum L) = ( 0. V) and

       A3: ( sum L) = 0 ;

      per cases ;

        suppose A is empty;

        then ( Carrier L) c= {} by RLVECT_2:def 6;

        hence thesis;

      end;

        suppose A is non empty;

        then

        consider p be VECTOR of V such that

         A4: p in A and

         A5: ((( - p) + A) \ {( 0. V)}) is linearly-independent by A1;

        

         A6: (A \/ {p}) = A by A4, ZFMISC_1: 40;

        consider Lp be Linear_Combination of {p} such that

         A7: (Lp . p) = (L . p) by RLVECT_4: 37;

        set LLp = (L - Lp);

        ((( - p) + LLp) . ( 0. V)) = (LLp . (( 0. V) - ( - p))) by Def1

        .= (LLp . ( - ( - p))) by RLVECT_1: 14

        .= (LLp . p)

        .= ((L . p) - (Lp . p)) by RLVECT_2: 54

        .= 0 by A7;

        then

         A8: not ( 0. V) in ( Carrier (( - p) + LLp)) by RLVECT_2: 19;

        

         A9: ( Carrier Lp) c= {p} by RLVECT_2:def 6;

        then

         A10: ( Carrier Lp) = {p} or ( Carrier Lp) = {} by ZFMISC_1: 33;

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

        then ( Carrier LLp) c= (( Carrier L) \/ ( Carrier Lp)) & (( Carrier L) \/ ( Carrier Lp)) c= (A \/ {p}) by A9, RLVECT_2: 55, XBOOLE_1: 13;

        then

         A11: ( Carrier LLp) c= A by A6;

        ( Carrier (( - p) + LLp)) = (( - p) + ( Carrier LLp)) by Th16;

        then ( Carrier (( - p) + LLp)) c= (( - p) + A) by A11, RLTOPSP1: 8;

        then ( Carrier (( - p) + LLp)) c= ((( - p) + A) \ {( 0. V)}) by A8, ZFMISC_1: 34;

        then

         A12: (( - p) + LLp) is Linear_Combination of ((( - p) + A) \ {( 0. V)}) by RLVECT_2:def 6;

        

         A13: (LLp + Lp) = (L + (Lp - Lp)) by RLVECT_2: 40

        .= (L + ( ZeroLC V)) by RLVECT_2: 57

        .= L by RLVECT_2: 41;

        

         A14: ( Sum (( - p) + Lp)) = ((( sum Lp) * ( - p)) + ( Sum Lp)) by Th39

        .= ((( sum Lp) * ( - p)) + ((Lp . p) * p)) by RLVECT_2: 32

        .= (((Lp . p) * ( - p)) + ((Lp . p) * p)) by A9, Th32

        .= ((Lp . p) * (( - p) + p)) by RLVECT_1:def 5

        .= ((Lp . p) * ( 0. V)) by RLVECT_1: 5

        .= ( 0. V);

        ( Sum (( - p) + L)) = ((( sum L) * ( - p)) + ( Sum L)) by Th39

        .= (( 0. V) + ( 0. V)) by A2, A3, RLVECT_1: 10

        .= ( 0. V);

        

        then ( 0. V) = ( Sum ((( - p) + LLp) + (( - p) + Lp))) by A13, Th17

        .= (( Sum (( - p) + LLp)) + ( 0. V)) by A14, RLVECT_3: 1

        .= ( Sum (( - p) + LLp));

        then {} = ( Carrier (( - p) + LLp)) by A5, A12;

        then

         A15: ( ZeroLC V) = (( - p) + LLp) by RLVECT_2:def 5;

        

         A16: LLp = (( 0. V) + LLp) by Th21

        .= ((p + ( - p)) + LLp) by RLVECT_1: 5

        .= (p + (( - p) + LLp)) by Th19

        .= ( ZeroLC V) by A15, Th20;

        then ( sum LLp) = 0 by Th31;

        

        then 0 = ( 0 + ( sum Lp)) by A3, A13, Th34

        .= ( 0 + (Lp . p)) by A9, Th32;

        then not p in ( Carrier Lp) by RLVECT_2: 19;

        then (( Carrier LLp) \/ ( Carrier Lp)) = {} by A10, A16, RLVECT_2:def 5, TARSKI:def 1;

        then ( Carrier L) c= {} by A13, RLVECT_2: 37;

        hence thesis;

      end;

    end;

    

     Lm6: for A st for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} holds for p be VECTOR of V st p in A holds ((( - p) + A) \ {( 0. V)}) is linearly-independent

    proof

      let A such that

       A1: for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} ;

      let p be Element of V such that

       A2: p in A;

      set pA = (( - p) + A), pA0 = ((( - p) + A) \ {( 0. V)});

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

      then ( 0. V) in pA by A2;

      then

       A3: (pA0 \/ {( 0. V)}) = pA by ZFMISC_1: 116;

      let L be Linear_Combination of pA0 such that

       A4: ( Sum L) = ( 0. V);

      reconsider sL = ( - ( sum L)) as Real;

      consider Lp be Linear_Combination of {( 0. V)} such that

       A5: (Lp . ( 0. V)) = sL by RLVECT_4: 37;

      set LLp = (L + Lp);

      set pLLp = (p + LLp);

      

       A6: ( Carrier Lp) c= {( 0. V)} by RLVECT_2:def 6;

      

       A7: (p + pA) = ((p + ( - p)) + A) by Th5

      .= (( 0. V) + A) by RLVECT_1: 5

      .= A by Th6;

      

       A8: ( Carrier pLLp) = (p + ( Carrier LLp)) by Th16;

      

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

      then ( Carrier LLp) c= (( Carrier L) \/ ( Carrier Lp)) & (( Carrier L) \/ ( Carrier Lp)) c= (pA0 \/ {( 0. V)}) by A6, RLVECT_2: 37, XBOOLE_1: 13;

      then ( Carrier LLp) c= pA by A3;

      then ( Carrier pLLp) c= A by A7, A8, RLTOPSP1: 8;

      then

       A10: pLLp is Linear_Combination of A by RLVECT_2:def 6;

      

       A11: ( sum pLLp) = ( sum LLp) by Th37;

      

       A12: ( sum LLp) = (( sum L) + ( sum Lp)) by Th34

      .= (( sum L) + sL) by A5, A6, Th32

      .= 0 ;

      

      then ( Sum pLLp) = (( 0 * p) + ( Sum LLp)) by Th39

      .= (( 0. V) + ( Sum LLp)) by RLVECT_1: 10

      .= ( Sum LLp)

      .= (( Sum L) + ( Sum Lp)) by RLVECT_3: 1

      .= ( Sum Lp) by A4

      .= ((Lp . ( 0. V)) * ( 0. V)) by RLVECT_2: 32

      .= ( 0. V);

      then ( Carrier pLLp) = {} by A1, A10, A11, A12;

      then

       A13: pLLp = ( ZeroLC V) by RLVECT_2:def 5;

      

       A14: LLp = (( 0. V) + LLp) by Th21

      .= ((( - p) + p) + LLp) by RLVECT_1: 5

      .= (( - p) + ( ZeroLC V)) by A13, Th19

      .= ( ZeroLC V) by Th20;

      assume ( Carrier L) <> {} ;

      then

      consider v be object such that

       A15: v in ( Carrier L) by XBOOLE_0:def 1;

      reconsider v as Element of V by A15;

       not v in ( Carrier Lp) by A6, A9, A15, XBOOLE_0:def 5;

      then (Lp . v) = 0 ;

      

      then ((L . v) + 0 ) = (LLp . v) by RLVECT_2:def 10

      .= 0 by A14, RLVECT_2: 20;

      hence contradiction by A15, RLVECT_2: 19;

    end;

    theorem :: RLAFFIN1:41

    

     Th41: A is affinely-independent iff for v st v in A holds ((( - v) + A) \ {( 0. V)}) is linearly-independent

    proof

      hereby

        assume A is affinely-independent;

        then for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} by Lm5;

        hence for v st v in A holds ((( - v) + A) \ {( 0. V)}) is linearly-independent by Lm6;

      end;

      assume

       A1: for v st v in A holds ((( - v) + A) \ {( 0. V)}) is linearly-independent;

      assume A is non empty;

      then

      consider v be object such that

       A2: v in A;

      reconsider v as Element of V by A2;

      take v;

      thus thesis by A1, A2;

    end;

    theorem :: RLAFFIN1:42

    

     Th42: A is affinely-independent iff for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {}

    proof

      thus A is affinely-independent implies for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} by Lm5;

      assume for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} ;

      then for p be VECTOR of V st p in A holds ((( - p) + A) \ {( 0. V)}) is linearly-independent by Lm6;

      hence thesis by Th41;

    end;

    theorem :: RLAFFIN1:43

    

     Th43: A is affinely-independent & B c= A implies B is affinely-independent

    proof

      assume that

       A1: A is affinely-independent and

       A2: B c= A;

      now

        let L be Linear_Combination of B such that

         A3: ( Sum L) = ( 0. V) & ( sum L) = 0 ;

        L is Linear_Combination of A by A2, RLVECT_2: 21;

        hence ( Carrier L) = {} by A1, A3, Th42;

      end;

      hence thesis by Th42;

    end;

    registration

      let V;

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

      coherence

      proof

        let A;

        assume A is linearly-independent;

        then for L be Linear_Combination of A st ( Sum L) = ( 0. V) & ( sum L) = 0 holds ( Carrier L) = {} ;

        hence thesis by Th42;

      end;

    end

    reserve I for affinely-independent Subset of V;

    registration

      let V, I, v;

      cluster (v + I) -> affinely-independent;

      coherence

      proof

        set vI = (v + I);

        now

          let L be Linear_Combination of vI such that

           A1: ( Sum L) = ( 0. V) and

           A2: ( sum L) = 0 ;

          set vL = (( - v) + L);

          

           A3: ( sum vL) = 0 by A2, Th37;

          

           A4: ( Carrier vL) = (( - v) + ( Carrier L)) & ( Carrier L) c= vI by Th16, RLVECT_2:def 6;

          (( - v) + vI) = ((( - v) + v) + I) by Th5

          .= (( 0. V) + I) by RLVECT_1: 5

          .= I by Th6;

          then ( Carrier vL) c= I by A4, RLTOPSP1: 8;

          then

           A5: vL is Linear_Combination of I by RLVECT_2:def 6;

          ( Sum vL) = (( 0 * ( - v)) + ( 0. V)) by A1, A2, Th39

          .= (( 0. V) + ( 0. V)) by RLVECT_1: 10

          .= ( 0. V);

          then ( Carrier vL) = {} by A3, A5, Th42;

          then

           A6: vL = ( ZeroLC V) by RLVECT_2:def 5;

          L = (( 0. V) + L) by Th21

          .= ((v + ( - v)) + L) by RLVECT_1: 5

          .= (v + ( ZeroLC V)) by A6, Th19

          .= ( ZeroLC V) by Th20;

          hence ( Carrier L) = {} by RLVECT_2:def 5;

        end;

        hence thesis by Th42;

      end;

    end

    theorem :: RLAFFIN1:44

    (v + A) is affinely-independent implies A is affinely-independent

    proof

      assume

       A1: (v + A) is affinely-independent;

      (( - v) + (v + A)) = ((( - v) + v) + A) by Th5

      .= (( 0. V) + A) by RLVECT_1: 5

      .= A by Th6;

      hence thesis by A1;

    end;

    registration

      let V, I, r;

      cluster (r * I) -> affinely-independent;

      coherence

      proof

        per cases ;

          suppose r = 0 ;

          then (r * I) c= {( 0. V)} by Th12;

          then (r * I) = ( {} V) or (r * I) = {( 0. V)} by ZFMISC_1: 33;

          hence thesis;

        end;

          suppose

           A1: r <> 0 ;

          now

            let L be Linear_Combination of (r * I) such that

             A2: ( Sum L) = ( 0. V) and

             A3: ( sum L) = 0 ;

            set rL = ((r " ) (*) L);

            

             A4: ( Sum rL) = ((r " ) * ( 0. V)) by A2, Th40

            .= ( 0. V);

            

             A5: ( Carrier rL) = ((r " ) * ( Carrier L)) & ( Carrier L) c= (r * I) by A1, Th23, RLVECT_2:def 6;

            ((r " ) * (r * I)) = (((r " ) * r) * I) by Th10

            .= (1 * I) by A1, XCMPLX_0:def 7

            .= I by Th11;

            then ( Carrier rL) c= I by A5, Th9;

            then

             A6: rL is Linear_Combination of I by RLVECT_2:def 6;

            ( sum rL) = 0 by A1, A3, Th38;

            then ( Carrier rL) = {} by A4, A6, Th42;

            then

             A7: rL = ( ZeroLC V) by RLVECT_2:def 5;

            L = (1 (*) L) by Th28

            .= ((r * (r " )) (*) L) by A1, XCMPLX_0:def 7

            .= (r (*) ( ZeroLC V)) by A7, Th27

            .= ( ZeroLC V) by Th26;

            hence ( Carrier L) = {} by RLVECT_2:def 5;

          end;

          hence thesis by Th42;

        end;

      end;

    end

    theorem :: RLAFFIN1:45

    (r * A) is affinely-independent & r <> 0 implies A is affinely-independent

    proof

      assume that

       A1: (r * A) is affinely-independent and

       A2: r <> 0 ;

      ((r " ) * (r * A)) = (((r " ) * r) * A) by Th10

      .= (1 * A) by A2, XCMPLX_0:def 7

      .= A by Th11;

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:46

    

     Th46: ( 0. V) in A implies (A is affinely-independent iff (A \ {( 0. V)}) is linearly-independent)

    proof

      assume

       A1: ( 0. V) in A;

      

       A2: (( - ( 0. V)) + A) = (( 0. V) + A)

      .= A by Th6;

      hence A is affinely-independent implies (A \ {( 0. V)}) is linearly-independent by A1, Th41;

      assume (A \ {( 0. V)}) is linearly-independent;

      hence thesis by A1, A2;

    end;

    definition

      let V;

      let F be Subset-Family of V;

      :: RLAFFIN1:def5

      attr F is affinely-independent means A in F implies A is affinely-independent;

    end

    registration

      let V;

      cluster empty -> affinely-independent for Subset-Family of V;

      coherence ;

      let I;

      cluster {I} -> affinely-independent;

      coherence by TARSKI:def 1;

    end

    registration

      let V;

      cluster empty affinely-independent for Subset-Family of V;

      existence

      proof

        take ( {} ( bool the carrier of V));

        thus thesis;

      end;

      cluster non empty affinely-independent for Subset-Family of V;

      existence

      proof

        take { the affinely-independent Subset of V};

        thus thesis;

      end;

    end

    theorem :: RLAFFIN1:47

    F1 is affinely-independent & F2 is affinely-independent implies (F1 \/ F2) is affinely-independent

    proof

      assume

       A1: F1 is affinely-independent & F2 is affinely-independent;

      let A;

      assume A in (F1 \/ F2);

      then A in F1 or A in F2 by XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:48

    F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent;

    begin

    definition

      let RLS;

      let A be Subset of RLS;

      :: RLAFFIN1:def6

      func Affin A -> Subset of RLS equals ( meet { B where B be Affine Subset of RLS : A c= B });

      coherence

      proof

        set BB = { B where B be Affine Subset of RLS : A c= B };

        BB c= ( bool ( [#] RLS))

        proof

          let x be object;

          assume x in BB;

          then ex B be Affine Subset of RLS st x = B & A c= B;

          hence thesis;

        end;

        then

        reconsider BB as Subset-Family of RLS;

        ( meet BB) is Subset of RLS;

        hence thesis;

      end;

    end

    registration

      let RLS;

      let A be Subset of RLS;

      cluster ( Affin A) -> Affine;

      coherence

      proof

        set BB = { B where B be Affine Subset of RLS : A c= B };

        let v1,v2 be Element of RLS;

        let r be Real;

        assume that

         A1: v1 in ( Affin A) and

         A2: v2 in ( Affin A);

         A3:

        now

          let Y be set;

          assume

           A4: Y in BB;

          then

          consider B be Affine Subset of RLS such that

           A5: Y = B and A c= B;

          v1 in B & v2 in B by A1, A2, A4, A5, SETFAM_1:def 1;

          hence (((1 - r) * v1) + (r * v2)) in Y by A5, RUSUB_4:def 4;

        end;

        BB <> {} by A1, SETFAM_1:def 1;

        hence thesis by A3, SETFAM_1:def 1;

      end;

    end

    

     Lm7: for V be non empty RLSStruct holds for A be Subset of V holds A c= ( Affin A)

    proof

      let V be non empty RLSStruct;

      let A be Subset of V;

      set BB = { B where B be Affine Subset of V : A c= B };

       A1:

      now

        let Y be set;

        assume Y in BB;

        then ex B be Affine Subset of V st Y = B & A c= B;

        hence A c= Y;

      end;

      ( [#] V) is Affine;

      then ( [#] V) in BB;

      hence thesis by A1, SETFAM_1: 5;

    end;

    

     Lm8: for V be non empty RLSStruct holds for A be Affine Subset of V holds A = ( Affin A)

    proof

      let V be non empty RLSStruct;

      let A be Affine Subset of V;

      set BB = { B where B be Affine Subset of V : A c= B };

      A in BB;

      then

       A1: ( Affin A) c= A by SETFAM_1: 3;

      A c= ( Affin A) by Lm7;

      hence thesis by A1;

    end;

    registration

      let RLS;

      let A be empty Subset of RLS;

      cluster ( Affin A) -> empty;

      coherence

      proof

        ( {} RLS) is Affine;

        hence thesis by Lm8;

      end;

    end

    registration

      let RLS;

      let A be non empty Subset of RLS;

      cluster ( Affin A) -> non empty;

      coherence

      proof

        A c= ( Affin A) by Lm7;

        hence thesis;

      end;

    end

    theorem :: RLAFFIN1:49

    for A be Subset of RLS holds A c= ( Affin A) by Lm7;

    theorem :: RLAFFIN1:50

    for A be Affine Subset of RLS holds A = ( Affin A) by Lm8;

    theorem :: RLAFFIN1:51

    

     Th51: for A,B be Subset of RLS st A c= B & B is Affine holds ( Affin A) c= B

    proof

      let A,B be Subset of RLS;

      assume A c= B & B is Affine;

      then B in { C where C be Affine Subset of RLS : A c= C };

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: RLAFFIN1:52

    

     Th52: for A,B be Subset of RLS st A c= B holds ( Affin A) c= ( Affin B)

    proof

      let A,B be Subset of RLS;

      assume

       A1: A c= B;

      B c= ( Affin B) by Lm7;

      then A c= ( Affin B) by A1;

      hence thesis by Th51;

    end;

    theorem :: RLAFFIN1:53

    

     Th53: ( Affin (v + A)) = (v + ( Affin A))

    proof

      (v + A) c= (v + ( Affin A)) by Lm7, RLTOPSP1: 8;

      then

       A1: ( Affin (v + A)) c= (v + ( Affin A)) by Th51, RUSUB_4: 31;

      (( - v) + (v + A)) = ((( - v) + v) + A) by Th5

      .= (( 0. V) + A) by RLVECT_1: 5

      .= A by Th6;

      then A c= (( - v) + ( Affin (v + A))) by Lm7, RLTOPSP1: 8;

      then

       A2: ( Affin A) c= (( - v) + ( Affin (v + A))) by Th51, RUSUB_4: 31;

      (v + (( - v) + ( Affin (v + A)))) = ((v + ( - v)) + ( Affin (v + A))) by Th5

      .= (( 0. V) + ( Affin (v + A))) by RLVECT_1: 5

      .= ( Affin (v + A)) by Th6;

      then (v + ( Affin A)) c= ( Affin (v + A)) by A2, RLTOPSP1: 8;

      hence thesis by A1;

    end;

    theorem :: RLAFFIN1:54

    

     Th54: AR is Affine implies (r * AR) is Affine

    proof

      assume

       A1: AR is Affine;

      let v1,v2 be VECTOR of R, s;

      assume v1 in (r * AR);

      then

      consider w1 be Element of R such that

       A2: v1 = (r * w1) and

       A3: w1 in AR;

      assume v2 in (r * AR);

      then

      consider w2 be Element of R such that

       A4: v2 = (r * w2) and

       A5: w2 in AR;

      

       A6: (((1 - s) * w1) + (s * w2)) in AR by A1, A3, A5;

      

       A7: ((1 - s) * (r * w1)) = (((1 - s) * r) * w1) by RLVECT_1:def 7

      .= (r * ((1 - s) * w1)) by RLVECT_1:def 7;

      (s * (r * w2)) = ((s * r) * w2) by RLVECT_1:def 7

      .= (r * (s * w2)) by RLVECT_1:def 7;

      then (((1 - s) * v1) + (s * v2)) = (r * (((1 - s) * w1) + (s * w2))) by A2, A4, A7, RLVECT_1:def 5;

      hence thesis by A6;

    end;

    theorem :: RLAFFIN1:55

    

     Th55: r <> 0 implies ( Affin (r * AR)) = (r * ( Affin AR))

    proof

      assume

       A1: r <> 0 ;

      ((r " ) * (r * AR)) = (((r " ) * r) * AR) by Th10

      .= (1 * AR) by A1, XCMPLX_0:def 7

      .= AR by Th11;

      then AR c= ((r " ) * ( Affin (r * AR))) by Lm7, Th9;

      then

       A2: ( Affin AR) c= ((r " ) * ( Affin (r * AR))) by Th51, Th54;

      (r * AR) c= (r * ( Affin AR)) by Lm7, Th9;

      then

       A3: ( Affin (r * AR)) c= (r * ( Affin AR)) by Th51, Th54;

      (r * ((r " ) * ( Affin (r * AR)))) = ((r * (r " )) * ( Affin (r * AR))) by Th10

      .= (1 * ( Affin (r * AR))) by A1, XCMPLX_0:def 7

      .= ( Affin (r * AR)) by Th11;

      then (r * ( Affin AR)) c= ( Affin (r * AR)) by A2, Th9;

      hence thesis by A3;

    end;

    theorem :: RLAFFIN1:56

    ( Affin (r * A)) = (r * ( Affin A))

    proof

      per cases ;

        suppose

         A1: r = 0 ;

        then

         A2: (r * ( Affin A)) c= {( 0. V)} by Th12;

        

         A3: (r * ( Affin A)) c= (r * A)

        proof

          let x be object;

          assume

           A4: x in (r * ( Affin A));

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

          then A is non empty;

          then

          consider v be object such that

           A5: v in A;

          reconsider v as Element of V by A5;

          

           A6: (r * v) in (r * A) by A5;

          x = ( 0. V) by A2, A4, TARSKI:def 1;

          hence thesis by A1, A6, RLVECT_1: 10;

        end;

        (r * A) c= {( 0. V)} by A1, Th12;

        then

         A7: (r * A) is empty or (r * A) = {( 0. V)} by ZFMISC_1: 33;

         {( 0. V)} is Affine by RUSUB_4: 23;

        then

         A8: ( Affin (r * A)) = (r * A) by A7, Lm8;

        (r * A) c= (r * ( Affin A)) by Lm7, Th9;

        hence thesis by A3, A8;

      end;

        suppose r <> 0 ;

        hence thesis by Th55;

      end;

    end;

    theorem :: RLAFFIN1:57

    

     Th57: v in ( Affin A) implies ( Affin A) = (v + ( Up ( Lin (( - v) + A))))

    proof

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

      set BB = { B where B be Affine Subset of V : vA c= B };

      

       A1: (( - v) + A) c= ( Up ( Lin (( - v) + A)))

      proof

        let x be object;

        assume x in (( - v) + A);

        then x in ( Lin (( - v) + A)) by RLVECT_3: 15;

        hence thesis;

      end;

      ( Up ( Lin vA)) is Affine by RUSUB_4: 24;

      then

       A2: ( Up ( Lin vA)) in BB by A1;

      then

       A3: ( Affin vA) c= ( Up ( Lin vA)) by SETFAM_1: 3;

      assume v in ( Affin A);

      then (( - v) + v) in (( - v) + ( Affin A));

      then

       A4: ( 0. V) in (( - v) + ( Affin A)) by RLVECT_1: 5;

      now

        let Y be set;

        

         A5: ( Affin vA) = (( - v) + ( Affin A)) by Th53;

        assume Y in BB;

        then

        consider B be Affine Subset of V such that

         A6: Y = B and

         A7: vA c= B;

        

         A8: ( Lin vA) is Subspace of ( Lin B) by A7, RLVECT_3: 20;

        ( Affin vA) c= B by A7, Th51;

        then B = the carrier of ( Lin B) by A4, A5, RUSUB_4: 26;

        hence ( Up ( Lin vA)) c= Y by A6, A8, RLSUB_1:def 2;

      end;

      then ( Up ( Lin (( - v) + A))) c= ( Affin vA) by A2, SETFAM_1: 5;

      then ( Up ( Lin (( - v) + A))) = ( Affin vA) by A3;

      

      hence (v + ( Up ( Lin (( - v) + A)))) = (v + (( - v) + ( Affin A))) by Th53

      .= ((v + ( - v)) + ( Affin A)) by Th5

      .= (( 0. V) + ( Affin A)) by RLVECT_1: 5

      .= ( Affin A) by Th6;

    end;

    

     Lm9: ( Lin (A \/ {( 0. V)})) = ( Lin A)

    proof

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

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

      

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

      .= ( Lin A) by RLSUB_2: 9;

    end;

    theorem :: RLAFFIN1:58

    

     Th58: A is affinely-independent iff for B st B c= A & ( Affin A) = ( Affin B) holds A = B

    proof

      hereby

        assume

         A1: A is affinely-independent;

        let B;

        assume that

         A2: B c= A and

         A3: ( Affin A) = ( Affin B);

        assume A <> B;

        then B c< A by A2;

        then

        consider p be object such that

         A4: p in A and

         A5: not p in B by XBOOLE_0: 6;

        reconsider p as Element of V by A4;

        

         A6: (A \ {p}) c= ( Affin (A \ {p})) by Lm7;

        B is non empty by A3, A4;

        then

        consider q be object such that

         A7: q in B;

        reconsider q as Element of V by A7;

        ( - ( - q)) = q;

        then

         A8: (( - q) + p) <> ( 0. V) by A5, A7, RLVECT_1:def 10;

        set qA0 = ((( - q) + A) \ {( 0. V)});

        (( - q) + p) in (( - q) + A) by A4;

        then

         A9: (( - q) + p) in qA0 by A8, ZFMISC_1: 56;

        qA0 is linearly-independent by A1, A2, A7, Th41;

        then

         A10: not (( - q) + p) in ( Lin (qA0 \ {(( - q) + p)})) by A9, RLVECT_5: 17;

        

         A11: (q + (( - q) + p)) = ((q + ( - q)) + p) by RLVECT_1:def 3

        .= (( 0. V) + p) by RLVECT_1: 5

        .= p;

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

        then ( 0. V) in (( - q) + A) by A2, A7;

        then

         A12: ( 0. V) in ((( - q) + A) \ {(( - q) + p)}) by A8, ZFMISC_1: 56;

        (((( - q) + A) \ {( 0. V)}) \ {(( - q) + p)}) = ((( - q) + A) \ ( {( 0. V)} \/ {(( - q) + p)})) by XBOOLE_1: 41

        .= (((( - q) + A) \ {(( - q) + p)}) \ {( 0. V)}) by XBOOLE_1: 41;

        

        then

         A13: ( Lin (qA0 \ {(( - q) + p)})) = ( Lin ((((( - q) + A) \ {(( - q) + p)}) \ {( 0. V)}) \/ {( 0. V)})) by Lm9

        .= ( Lin ((( - q) + A) \ {(( - q) + p)})) by A12, ZFMISC_1: 116

        .= ( Lin ((( - q) + A) \ (( - q) + {p}))) by Lm3

        .= ( Lin (( - q) + (A \ {p}))) by Lm2;

        q in (A \ {p}) by A2, A5, A7, ZFMISC_1: 56;

        then

         A14: ( Affin (A \ {p})) = (q + ( Up ( Lin (qA0 \ {(( - q) + p)})))) by A6, A13, Th57;

        

         A15: not p in ( Affin (A \ {p}))

        proof

          assume p in ( Affin (A \ {p}));

          then

          consider v be Element of V such that

           A16: p = (q + v) and

           A17: v in ( Up ( Lin (qA0 \ {(( - q) + p)}))) by A14;

          (( - q) + p) = v by A11, A16, RLVECT_1: 8;

          hence thesis by A10, A17;

        end;

        B c= (A \ {p}) by A2, A5, ZFMISC_1: 34;

        then

         A18: ( Affin B) c= ( Affin (A \ {p})) by Th52;

        ( Affin (A \ {p})) c= ( Affin A) by Th52, XBOOLE_1: 36;

        then

         A19: ( Affin A) = ( Affin (A \ {p})) by A3, A18;

        A c= ( Affin A) by Lm7;

        hence contradiction by A4, A15, A19;

      end;

      assume

       A20: for B st B c= A & ( Affin A) = ( Affin B) holds A = B;

      assume A is non affinely-independent;

      then

      consider p be Element of V such that

       A21: p in A and

       A22: ((( - p) + A) \ {( 0. V)}) is non linearly-independent by Th41;

      set L = ( Lin ((( - p) + A) \ {( 0. V)}));

      ((( - p) + A) \ {( 0. V)}) c= the carrier of L

      proof

        let x be object;

        assume x in ((( - p) + A) \ {( 0. V)});

        then x in L by RLVECT_3: 15;

        hence thesis;

      end;

      then

      reconsider pA0 = ((( - p) + A) \ {( 0. V)}) as Subset of L;

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

      then

       A23: ( 0. V) in (( - p) + A) by A21;

      then

       A24: (pA0 \/ {( 0. V)}) = (( - p) + A) by ZFMISC_1: 116;

      ( Lin pA0) = L by RLVECT_5: 20;

      then

      consider b be Subset of L such that

       A25: b c= pA0 and

       A26: b is linearly-independent and

       A27: ( Lin b) = L by RLVECT_3: 25;

      reconsider B = b as linearly-independent Subset of V by A26, RLVECT_5: 14;

      

       A28: (B \/ {( 0. V)}) c= (pA0 \/ {( 0. V)}) by A25, XBOOLE_1: 9;

      ( 0. V) in {( 0. V)} by TARSKI:def 1;

      then (p + ( 0. V)) = p & ( 0. V) in (B \/ {( 0. V)}) by XBOOLE_0:def 3;

      then

       A29: p in (p + (B \/ {( 0. V)}));

      

       A30: (p + (B \/ {( 0. V)})) c= ( Affin (p + (B \/ {( 0. V)}))) by Lm7;

      

       A31: (p + (( - p) + A)) = ((p + ( - p)) + A) by Th5

      .= (( 0. V) + A) by RLVECT_1: 5

      .= A by Th6;

      

       A32: (( - p) + (p + (B \/ {( 0. V)}))) = ((( - p) + p) + (B \/ {( 0. V)})) by Th5

      .= (( 0. V) + (B \/ {( 0. V)})) by RLVECT_1: 5

      .= (B \/ {( 0. V)}) by Th6;

      A c= ( Affin A) by Lm7;

      

      then ( Affin A) = (p + ( Up ( Lin (( - p) + A)))) by A21, Th57

      .= (p + ( Up ( Lin (((( - p) + A) \ {( 0. V)}) \/ {( 0. V)})))) by A23, ZFMISC_1: 116

      .= (p + ( Up L)) by Lm9

      .= (p + ( Up ( Lin B))) by A27, RLVECT_5: 20

      .= (p + ( Up ( Lin (( - p) + (p + (B \/ {( 0. V)})))))) by A32, Lm9

      .= ( Affin (p + (B \/ {( 0. V)}))) by A29, A30, Th57;

      

      then pA0 = ((B \/ {( 0. V)}) \ {( 0. V)}) by A20, A24, A28, A31, A32, RLTOPSP1: 8

      .= B by RLVECT_3: 6, ZFMISC_1: 117;

      hence contradiction by A22;

    end;

    theorem :: RLAFFIN1:59

    

     Th59: ( Affin A) = { ( Sum L) where L be Linear_Combination of A : ( sum L) = 1 }

    proof

      set S = { ( Sum L) where L be Linear_Combination of A : ( sum L) = 1 };

      per cases ;

        suppose

         A1: A is empty;

        assume ( Affin A) <> S;

        then S is non empty by A1;

        then

        consider x be object such that

         A2: x in S;

        consider L be Linear_Combination of A such that x = ( Sum L) and

         A3: ( sum L) = 1 by A2;

        A = ( {} the carrier of V) by A1;

        then L = ( ZeroLC V) by RLVECT_2: 23;

        hence thesis by A3, Th31;

      end;

        suppose A is non empty;

        then

        consider p be object such that

         A4: p in A;

        reconsider p as Element of V by A4;

        A c= ( Affin A) by Lm7;

        then

         A5: ( Affin A) = (p + ( Up ( Lin (( - p) + A)))) by A4, Th57;

        thus ( Affin A) c= S

        proof

          let x be object;

          assume x in ( Affin A);

          then

          consider v such that

           A6: x = (p + v) and

           A7: v in ( Up ( Lin (( - p) + A))) by A5;

          v in ( Lin (( - p) + A)) by A7;

          then

          consider L be Linear_Combination of (( - p) + A) such that

           A8: ( Sum L) = v by RLVECT_3: 14;

          set pL = (p + L);

          consider Lp be Linear_Combination of {( 0. V)} such that

           A9: (Lp . ( 0. V)) = (1 - ( sum L)) by RLVECT_4: 37;

          set pLL = (p + (L + Lp));

          set pLp = (p + Lp);

          

           A10: ( Carrier Lp) c= {( 0. V)} by RLVECT_2:def 6;

          then

           A11: (p + ( Carrier Lp)) c= (p + {( 0. V)}) by RLTOPSP1: 8;

          

           A12: ( Carrier pL) = (p + ( Carrier L)) & ( Carrier L) c= (( - p) + A) by Th16, RLVECT_2:def 6;

          (p + (( - p) + A)) = ((p + ( - p)) + A) by Th5

          .= (( 0. V) + A) by RLVECT_1: 5

          .= A by Th6;

          then

           A13: ( Carrier pL) c= A by A12, RLTOPSP1: 8;

          

           A14: ( Carrier (pL + pLp)) c= (( Carrier pL) \/ ( Carrier pLp)) & pLL = (pL + pLp) by Th17, RLVECT_2: 37;

          ( Carrier pLp) = (p + ( Carrier Lp)) & (p + {( 0. V)}) = {(p + ( 0. V))} by Lm3, Th16;

          then ( Carrier pLp) c= {p} by A11;

          then (( Carrier pL) \/ ( Carrier pLp)) c= (A \/ {p}) by A13, XBOOLE_1: 13;

          then ( Carrier pLL) c= (A \/ {p}) by A14;

          then ( Carrier pLL) c= A by A4, ZFMISC_1: 40;

          then

           A15: pLL is Linear_Combination of A by RLVECT_2:def 6;

          

           A16: ( sum pLL) = ( sum (L + Lp)) by Th37;

          

           A17: ( sum (L + Lp)) = (( sum L) + ( sum Lp)) by Th34

          .= (( sum L) + (1 - ( sum L))) by A9, A10, Th32

          .= 1;

          

          then ( Sum pLL) = ((1 * p) + ( Sum (L + Lp))) by Th39

          .= ((1 * p) + (v + ( Sum Lp))) by A8, RLVECT_3: 1

          .= ((1 * p) + (v + ((Lp . ( 0. V)) * ( 0. V)))) by RLVECT_2: 32

          .= ((1 * p) + (v + ( 0. V)))

          .= (p + (v + ( 0. V))) by RLVECT_1:def 8

          .= x by A6;

          hence thesis by A15, A16, A17;

        end;

        let x be object;

        assume x in S;

        then

        consider L be Linear_Combination of A such that

         A18: ( Sum L) = x and

         A19: ( sum L) = 1;

        set pL = (( - p) + L);

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

        then

         A20: (( - p) + ( Carrier L)) c= (( - p) + A) by RLTOPSP1: 8;

        (( - p) + ( Carrier L)) = ( Carrier pL) by Th16;

        then pL is Linear_Combination of (( - p) + A) by A20, RLVECT_2:def 6;

        then ( Sum pL) in ( Lin (( - p) + A)) by RLVECT_3: 14;

        then

         A21: ( Sum pL) in ( Up ( Lin (( - p) + A)));

        (p + ( Sum pL)) = (p + ((1 * ( - p)) + ( Sum L))) by A19, Th39

        .= (p + (( - p) + ( Sum L))) by RLVECT_1:def 8

        .= ((p + ( - p)) + ( Sum L)) by RLVECT_1:def 3

        .= (( 0. V) + ( Sum L)) by RLVECT_1: 5

        .= x by A18;

        hence thesis by A5, A21;

      end;

    end;

    theorem :: RLAFFIN1:60

    

     Th60: I c= A implies ex Ia be affinely-independent Subset of V st I c= Ia & Ia c= A & ( Affin Ia) = ( Affin A)

    proof

      assume

       A1: I c= A;

      

       A2: A c= ( Affin A) by Lm7;

      per cases ;

        suppose

         A3: I is empty;

        per cases ;

          suppose

           A4: A is empty;

          take I;

          thus thesis by A3, A4;

        end;

          suppose A is non empty;

          then

          consider p be object such that

           A5: p in A;

          reconsider p as Element of V by A5;

          set L = ( Lin (( - p) + A));

          (( - p) + A) c= ( [#] L)

          proof

            let x be object;

            assume x in (( - p) + A);

            then x in ( Lin (( - p) + A)) by RLVECT_3: 15;

            hence thesis;

          end;

          then

          reconsider pA = (( - p) + A) as Subset of L;

          L = ( Lin pA) by RLVECT_5: 20;

          then

          consider Ia be Subset of L such that

           A6: Ia c= pA and

           A7: Ia is linearly-independent and

           A8: ( Lin Ia) = L by RLVECT_3: 25;

          ( [#] L) c= ( [#] V) by RLSUB_1:def 2;

          then

          reconsider IA = Ia as Subset of V by XBOOLE_1: 1;

          set IA0 = (IA \/ {( 0. V)});

           not ( 0. V) in IA by A7, RLVECT_3: 6, RLVECT_5: 14;

          then

           A9: (IA0 \ {( 0. V)}) = IA by ZFMISC_1: 117;

          ( 0. V) in {( 0. V)} by TARSKI:def 1;

          then

           A10: ( 0. V) in IA0 by XBOOLE_0:def 3;

          IA is linearly-independent by A7, RLVECT_5: 14;

          then IA0 is affinely-independent by A9, A10, Th46;

          then

          reconsider pIA0 = (p + IA0) as affinely-independent Subset of V;

          take pIA0;

          thus I c= pIA0 by A3;

          thus pIA0 c= A

          proof

            let x be object;

            assume x in pIA0;

            then

            consider v such that

             A11: x = (p + v) and

             A12: v in IA0;

            per cases by A12, XBOOLE_0:def 3;

              suppose v in IA;

              then v in { (( - p) + w) : w in A } by A6;

              then

              consider w such that

               A13: v = (( - p) + w) and

               A14: w in A;

              x = ((p + ( - p)) + w) by A11, A13, RLVECT_1:def 3

              .= (( 0. V) + w) by RLVECT_1: 5

              .= w;

              hence thesis by A14;

            end;

              suppose v in {( 0. V)};

              then v = ( 0. V) by TARSKI:def 1;

              hence thesis by A5, A11;

            end;

          end;

          

           A15: pIA0 c= ( Affin pIA0) by Lm7;

          

           A16: (( - p) + pIA0) = ((( - p) + p) + IA0) by Th5

          .= (( 0. V) + IA0) by RLVECT_1: 5

          .= IA0 by Th6;

          (p + ( 0. V)) = p;

          then p in pIA0 by A10;

          

          hence ( Affin pIA0) = (p + ( Up ( Lin IA0))) by A15, A16, Th57

          .= (p + ( Up ( Lin IA))) by Lm9

          .= (p + ( Up L)) by A8, RLVECT_5: 20

          .= ( Affin A) by A2, A5, Th57;

        end;

      end;

        suppose I is non empty;

        then

        consider p be object such that

         A17: p in I;

        reconsider p as Element of V by A17;

        

         A18: ((( - p) + I) \ {( 0. V)}) is linearly-independent by A17, Th41;

        

         A19: (( - p) + I) c= (( - p) + A) by A1, RLTOPSP1: 8;

        set L = ( Lin (( - p) + A));

        

         A20: ((( - p) + I) \ {( 0. V)}) c= (( - p) + I) by XBOOLE_1: 36;

        

         A21: (( - p) + A) c= ( Up L)

        proof

          let x be object;

          assume x in (( - p) + A);

          then x in L by RLVECT_3: 15;

          hence thesis;

        end;

        then (( - p) + I) c= ( Up L) by A19;

        then

        reconsider pI0 = ((( - p) + I) \ {( 0. V)}), pA = (( - p) + A) as Subset of L by A20, A21, XBOOLE_1: 1;

        L = ( Lin pA) & pI0 c= pA by A19, A20, RLVECT_5: 20;

        then

        consider i be linearly-independent Subset of L such that

         A22: pI0 c= i and

         A23: i c= pA and

         A24: ( Lin i) = L by A18, Th15, RLVECT_5: 15;

        reconsider Ia = i as linearly-independent Subset of V by RLVECT_5: 14;

        set I0 = (Ia \/ {( 0. V)});

        

         A25: ( 0. V) in {( 0. V)} by TARSKI:def 1;

         not ( 0. V) in Ia by RLVECT_3: 6;

        then (I0 \ {( 0. V)}) = Ia & ( 0. V) in I0 by A25, XBOOLE_0:def 3, ZFMISC_1: 117;

        then I0 is affinely-independent by Th46;

        then

        reconsider pI0 = (p + I0) as affinely-independent Subset of V;

        take pI0;

        

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

        

        then

         A27: (p + (( - p) + I)) = (( 0. V) + I) by Th5

        .= I by Th6;

        ( 0. V) in { (( - p) + v) where v be Element of V : v in I } by A17, A26;

        then (((( - p) + I) \ {( 0. V)}) \/ {( 0. V)}) = (( - p) + I) by ZFMISC_1: 116;

        then

         A28: (( - p) + I) c= I0 by A22, XBOOLE_1: 9;

        hence I c= pI0 by A27, RLTOPSP1: 8;

        (p + (( - p) + I)) c= pI0 by A28, RLTOPSP1: 8;

        then

         A29: p in pI0 by A17, A27;

        thus pI0 c= A

        proof

          let x be object;

          assume x in pI0;

          then

          consider v such that

           A30: x = (p + v) and

           A31: v in I0;

          per cases by A31, XBOOLE_0:def 3;

            suppose v in Ia;

            then v in { (( - p) + w) : w in A } by A23;

            then

            consider w such that

             A32: v = (( - p) + w) and

             A33: w in A;

            x = ((p + ( - p)) + w) by A30, A32, RLVECT_1:def 3

            .= (( 0. V) + w) by RLVECT_1: 5

            .= w;

            hence thesis by A33;

          end;

            suppose v in {( 0. V)};

            then v = ( 0. V) by TARSKI:def 1;

            then x = p by A30;

            hence thesis by A1, A17;

          end;

        end;

        

         A34: pI0 c= ( Affin pI0) by Lm7;

        

         A35: p in A by A1, A17;

        (( - p) + pI0) = (( 0. V) + I0) by A26, Th5

        .= I0 by Th6;

        

        hence ( Affin pI0) = (p + ( Up ( Lin I0))) by A29, A34, Th57

        .= (p + ( Up ( Lin Ia))) by Lm9

        .= (p + ( Up L)) by A24, RLVECT_5: 20

        .= ( Affin A) by A2, A35, Th57;

      end;

    end;

    theorem :: RLAFFIN1:61

    for A,B be finite Subset of V st A is affinely-independent & ( Affin A) = ( Affin B) & ( card B) <= ( card A) holds B is affinely-independent

    proof

      let A,B be finite Subset of V;

      assume that

       A1: A is affinely-independent and

       A2: ( Affin A) = ( Affin B) and

       A3: ( card B) <= ( card A);

      per cases ;

        suppose A is empty;

        then B is empty by A3, XXREAL_0: 1;

        hence thesis;

      end;

        suppose A is non empty;

        then

        consider p be object such that

         A4: p in A;

        ( card A) > 0 by A4;

        then

        reconsider n = (( card A) - 1) as Element of NAT by NAT_1: 20;

        

         A5: A c= ( Affin A) by Lm7;

        reconsider p as Element of V by A4;

        set L = ( Lin (( - p) + A));

        ( {} V) c= B;

        then

        consider Ia be affinely-independent Subset of V such that ( {} V) c= Ia and

         A6: Ia c= B and

         A7: ( Affin Ia) = ( Affin B) by Th60;

        Ia is non empty by A2, A4, A7;

        then

        consider q be object such that

         A8: q in Ia;

        (( - p) + A) c= ( [#] L)

        proof

          let x be object;

          assume x in (( - p) + A);

          then x in ( Lin (( - p) + A)) by RLVECT_3: 15;

          hence thesis;

        end;

        then

        reconsider pA = (( - p) + A) as Subset of L;

        ((( - p) + A) \ {( 0. V)}) is linearly-independent by A1, A4, Th41;

        then

         A9: (pA \ {( 0. V)}) is linearly-independent by RLVECT_5: 15;

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

        then

         A10: ( 0. V) in pA by A4;

        

        then L = ( Lin (((( - p) + A) \ {( 0. V)}) \/ {( 0. V)})) by ZFMISC_1: 116

        .= ( Lin ((( - p) + A) \ {( 0. V)})) by Lm9

        .= ( Lin (pA \ {( 0. V)})) by RLVECT_5: 20;

        then

         A11: (pA \ {( 0. V)}) is Basis of L by A9, RLVECT_3:def 3;

        reconsider IA = Ia as finite set by A6;

        

         A12: Ia c= ( Affin Ia) by Lm7;

        reconsider q as Element of V by A8;

        (p + L) = (p + ( Up L)) by RUSUB_4: 30

        .= ( Affin A) by A4, A5, Th57

        .= (q + ( Up ( Lin (( - q) + Ia)))) by A2, A7, A8, A12, Th57

        .= (q + ( Lin (( - q) + Ia))) by RUSUB_4: 30;

        then

         A13: L = ( Lin (( - q) + Ia)) by RLSUB_1: 69;

        set qI = (( - q) + Ia);

        

         A14: qI c= ( [#] ( Lin (( - q) + Ia)))

        proof

          let x be object;

          assume x in qI;

          then x in ( Lin (( - q) + Ia)) by RLVECT_3: 15;

          hence thesis;

        end;

        ( card pA) = (n + 1) by Th7;

        then

         A15: ( card (pA \ {( 0. V)})) = n by A10, STIRL2_1: 55;

        then (pA \ {( 0. V)}) is finite;

        then

         A16: L is finite-dimensional by A11, RLVECT_5:def 1;

        reconsider qI as Subset of ( Lin (( - q) + Ia)) by A14;

        ((( - q) + Ia) \ {( 0. V)}) is linearly-independent by A8, Th41;

        then

         A17: (qI \ {( 0. V)}) is linearly-independent by RLVECT_5: 15;

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

        then

         A18: ( 0. V) in qI by A8;

        

        then ( Lin (( - q) + Ia)) = ( Lin (((( - q) + Ia) \ {( 0. V)}) \/ {( 0. V)})) by ZFMISC_1: 116

        .= ( Lin ((( - q) + Ia) \ {( 0. V)})) by Lm9

        .= ( Lin (qI \ {( 0. V)})) by RLVECT_5: 20;

        then (qI \ {( 0. V)}) is Basis of ( Lin (( - q) + Ia)) by A17, RLVECT_3:def 3;

        then

         A19: ( card (qI \ {( 0. V)})) = n by A11, A13, A15, A16, RLVECT_5: 25;

        then ( not ( 0. V) in (qI \ {( 0. V)})) & (qI \ {( 0. V)}) is finite by ZFMISC_1: 56;

        

        then

         A20: (n + 1) = ( card ((qI \ {( 0. V)}) \/ {( 0. V)})) by A19, CARD_2: 41

        .= ( card qI) by A18, ZFMISC_1: 116

        .= ( card Ia) by Th7;

        ( card IA) <= ( card B) by A6, NAT_1: 43;

        hence thesis by A3, A6, A20, CARD_2: 102, XXREAL_0: 1;

      end;

    end;

    theorem :: RLAFFIN1:62

    

     Th62: L is convex iff ( sum L) = 1 & for v holds 0 <= (L . v)

    proof

      hereby

        assume L is convex;

        then

        consider F be FinSequence of the carrier of V such that

         A1: F is one-to-one and

         A2: ( rng F) = ( Carrier L) and

         A3: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 ;

        consider f be FinSequence of REAL such that

         A4: ( len f) = ( len F) and

         A5: ( Sum f) = 1 and

         A6: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A3;

        

         A7: ( len (L * F)) = ( len F) by FINSEQ_2: 33;

        now

          let k be Nat;

          assume

           A8: 1 <= k & k <= ( len F);

          then k in ( dom f) by A4, FINSEQ_3: 25;

          then

           A9: (f . k) = (L . (F . k)) by A6;

          k in ( dom (L * F)) by A7, A8, FINSEQ_3: 25;

          hence ((L * F) . k) = (f . k) by A9, FUNCT_1: 12;

        end;

        then (L * F) = f by A4, A7;

        hence ( sum L) = 1 by A1, A2, A5, Def3;

        let v be Element of V;

        per cases ;

          suppose v in ( Carrier L);

          then

          consider n be object such that

           A10: n in ( dom F) and

           A11: (F . n) = v by A2, FUNCT_1:def 3;

          

           A12: ( dom f) = ( dom F) by A4, FINSEQ_3: 29;

          then (f . n) = (L . (F . n)) by A6, A10;

          hence (L . v) >= 0 by A6, A10, A11, A12;

        end;

          suppose not v in ( Carrier L);

          hence (L . v) >= 0 ;

        end;

      end;

      assume ( sum L) = 1;

      then

      consider F be FinSequence of V such that

       A13: F is one-to-one & ( rng F) = ( Carrier L) and

       A14: 1 = ( Sum (L * F)) by Def3;

      assume

       A15: for v be Element of V holds (L . v) >= 0 ;

      now

        take F;

        thus F is one-to-one & ( rng F) = ( Carrier L) by A13;

        take f = (L * F);

        thus ( len f) = ( len F) & ( Sum f) = 1 by A14, FINSEQ_2: 33;

        then

         A16: ( dom F) = ( dom f) by FINSEQ_3: 29;

        let n be Nat;

        assume

         A17: n in ( dom f);

        then

         A18: (f . n) = (L . (F . n)) by FUNCT_1: 12;

        (F . n) = (F /. n) by A16, A17, PARTFUN1:def 6;

        hence (f . n) = (L . (F . n)) & (f . n) >= 0 by A15, A18;

      end;

      hence thesis;

    end;

    theorem :: RLAFFIN1:63

    

     Th63: L is convex implies (L . x) <= 1

    proof

      assume

       A1: L is convex;

      then ( sum L) = 1 by Th62;

      then

      consider F be FinSequence of V such that F is one-to-one and

       A2: ( rng F) = ( Carrier L) and

       A3: 1 = ( Sum (L * F)) by Def3;

      assume

       A4: (L . x) > 1;

      then x in ( dom L) by FUNCT_1:def 2;

      then

      reconsider v = x as Element of V by FUNCT_2:def 1;

      v in ( Carrier L) by A4;

      then

      consider n be object such that

       A5: n in ( dom F) and

       A6: (F . n) = v by A2, FUNCT_1:def 3;

      ( len (L * F)) = ( len F) by FINSEQ_2: 33;

      then

       A7: ( dom (L * F)) = ( dom F) by FINSEQ_3: 29;

       A8:

      now

        let i be Nat;

        assume i in ( dom (L * F));

        then ((L * F) . i) = (L . (F . i)) & (F . i) = (F /. i) by A7, FUNCT_1: 12, PARTFUN1:def 6;

        hence ((L * F) . i) >= 0 by A1, Th62;

      end;

      reconsider n as Nat by A5;

      ((L * F) . n) = (L . x) by A5, A6, A7, FUNCT_1: 12;

      hence contradiction by A3, A4, A5, A7, A8, MATRPROB: 5;

    end;

    reconsider jj = 1 as Real;

    theorem :: RLAFFIN1:64

    

     Th64: L is convex & (L . x) = 1 implies ( Carrier L) = {x}

    proof

      assume that

       A1: L is convex and

       A2: (L . x) = 1;

      x in ( dom L) by A2, FUNCT_1:def 2;

      then

      reconsider v = x as Element of V by FUNCT_2:def 1;

      consider K be Linear_Combination of {v} such that

       A3: (K . v) = jj by RLVECT_4: 37;

      set LK = (L - K);

      

       A4: ( Carrier K) c= {v} by RLVECT_2:def 6;

      ( sum LK) = (( sum L) - ( sum K)) by Th36

      .= (( sum L) - 1) by A3, A4, Th32

      .= (1 - 1) by A1, Th62

      .= 0 ;

      then

      consider F be FinSequence of V such that F is one-to-one and

       A5: ( rng F) = ( Carrier LK) and

       A6: 0 = ( Sum (LK * F)) by Def3;

      ( len (LK * F)) = ( len F) by FINSEQ_2: 33;

      then

       A7: ( dom (LK * F)) = ( dom F) by FINSEQ_3: 29;

      

       A8: for i be Nat st i in ( dom (LK * F)) holds 0 <= ((LK * F) . i)

      proof

        let i be Nat;

        assume

         A9: i in ( dom (LK * F));

        then

         A10: ((LK * F) . i) = (LK . (F . i)) by FUNCT_1: 12;

        

         A11: (F . i) in ( Carrier LK) by A5, A7, A9, FUNCT_1:def 3;

        then

         A12: (LK . (F . i)) = ((L . (F . i)) - (K . (F . i))) by RLVECT_2: 54;

        per cases ;

          suppose (F . i) = v;

          hence thesis by A2, A3, A9, A12, FUNCT_1: 12;

        end;

          suppose (F . i) <> v;

          then not (F . i) in ( Carrier K) by A4, TARSKI:def 1;

          then (K . (F . i)) = 0 by A11;

          hence thesis by A1, A10, A11, A12, Th62;

        end;

      end;

      ( Carrier LK) = {}

      proof

        assume ( Carrier LK) <> {} ;

        then

        consider p be object such that

         A13: p in ( Carrier LK) by XBOOLE_0:def 1;

        reconsider p as Element of V by A13;

        consider i be object such that

         A14: i in ( dom F) and

         A15: (F . i) = p by A5, A13, FUNCT_1:def 3;

        reconsider i as Nat by A14;

        ((LK * F) . i) > 0

        proof

          

           A16: (LK . p) = ((L . p) - (K . p)) by RLVECT_2: 54;

          per cases ;

            suppose p = v;

            then (LK . p) = (1 - 1) by A2, A3, RLVECT_2: 54;

            hence thesis by A13, RLVECT_2: 19;

          end;

            suppose p <> v;

            then not p in ( Carrier K) by A4, TARSKI:def 1;

            then (K . p) = 0 ;

            then

             A17: (LK . p) >= 0 by A1, A16, Th62;

            (LK . p) <> 0 by A13, RLVECT_2: 19;

            hence thesis by A7, A14, A15, A17, FUNCT_1: 12;

          end;

        end;

        hence thesis by A6, A7, A8, A14, RVSUM_1: 85;

      end;

      then ( ZeroLC V) = (L + ( - K)) by RLVECT_2:def 5;

      then

       A18: ( - K) = ( - L) by RLVECT_2: 50;

      

       A19: v in ( Carrier L) by A2;

      ( - ( - L)) = L by RLVECT_2: 53;

      then K = L by A18, RLVECT_2: 53;

      hence thesis by A4, A19, ZFMISC_1: 33;

    end;

    theorem :: RLAFFIN1:65

    

     Th65: ( conv A) c= ( Affin A)

    proof

      let x be object;

      assume

       A1: x in ( conv A);

      then

      reconsider A1 = A as non empty Subset of V;

      ( conv A1) = { ( Sum L) where L be Convex_Combination of A1 : L in ( ConvexComb V) } by CONVEX3: 5;

      then

      consider L be Convex_Combination of A1 such that

       A2: ( Sum L) = x and L in ( ConvexComb V) by A1;

      ( sum L) = 1 by Th62;

      then x in { ( Sum K) where K be Linear_Combination of A : ( sum K) = 1 } by A2;

      hence thesis by Th59;

    end;

    theorem :: RLAFFIN1:66

    x in ( conv A) & (( conv A) \ {x}) is convex implies x in A

    proof

      assume that

       A1: x in ( conv A) and

       A2: (( conv A) \ {x}) is convex;

      reconsider A1 = A as non empty Subset of V by A1;

      

       A3: ( conv A1) = { ( Sum L) where L be Convex_Combination of A1 : L in ( ConvexComb V) } by CONVEX3: 5;

      assume

       A4: not x in A;

      consider L be Convex_Combination of A1 such that

       A5: ( Sum L) = x and L in ( ConvexComb V) by A1, A3;

      set C = ( Carrier L);

      

       A6: C c= A1 by RLVECT_2:def 6;

      C <> {} by CONVEX1: 21;

      then

      consider p be object such that

       A7: p in C by XBOOLE_0:def 1;

      reconsider p as Element of V by A7;

      

       A8: ( sum L) = 1 by Th62;

      (C \ {p}) <> {}

      proof

        assume

         A9: (C \ {p}) = {} ;

        then C = {p} by A7, ZFMISC_1: 58;

        then

         A10: (L . p) = 1 by A8, Th32;

        ( Sum L) = ((L . p) * p) by A7, A9, RLVECT_2: 35, ZFMISC_1: 58;

        then x = p by A5, A10, RLVECT_1:def 8;

        hence thesis by A4, A6, A7;

      end;

      then

      consider q be object such that

       A11: q in (C \ {p}) by XBOOLE_0:def 1;

      reconsider q as Element of V by A11;

      

       A12: q in C by A11, XBOOLE_0:def 5;

      then (L . q) <> 0 by RLVECT_2: 19;

      then

       A13: (L . q) > 0 by Th62;

      reconsider mm = ( min ((L . p),(L . q))) as Real;

      consider Lq be Linear_Combination of {q} such that

       A14: (Lq . q) = mm by RLVECT_4: 37;

      

       A15: p <> q by A11, ZFMISC_1: 56;

      then

       A16: (p - q) <> ( 0. V) by RLVECT_1: 21;

      

       A17: ( Carrier Lq) c= {q} by RLVECT_2:def 6;

       {q} c= A by A6, A12, ZFMISC_1: 31;

      then ( Carrier Lq) c= A by A17;

      then

       A18: Lq is Linear_Combination of A by RLVECT_2:def 6;

      consider Lp be Linear_Combination of {p} such that

       A19: (Lp . p) = mm by RLVECT_4: 37;

      

       A20: ( Carrier Lp) c= {p} by RLVECT_2:def 6;

       {p} c= A by A6, A7, ZFMISC_1: 31;

      then ( Carrier Lp) c= A by A20;

      then Lp is Linear_Combination of A by RLVECT_2:def 6;

      then

       A21: (Lp - Lq) is Linear_Combination of A by A18, RLVECT_2: 56;

      then ( - (Lp - Lq)) is Linear_Combination of A by RLVECT_2: 52;

      then

      reconsider Lpq = (L + (Lp - Lq)), L1pq = (L - (Lp - Lq)) as Linear_Combination of A1 by A21, RLVECT_2: 38;

      

       A22: ( Sum L1pq) = (( Sum L) - ( Sum (Lp - Lq))) by RLVECT_3: 4

      .= (( Sum L) + ( - ( Sum (Lp - Lq)))) by RLVECT_1:def 11;

      (L . p) <> 0 by A7, RLVECT_2: 19;

      then (L . p) > 0 by Th62;

      then

       A23: mm > 0 by A13, XXREAL_0: 15;

      

       A24: for v holds (L1pq . v) >= 0

      proof

        let v;

        

         A25: (L1pq . v) = ((L . v) - ((Lp - Lq) . v)) by RLVECT_2: 54

        .= ((L . v) - ((Lp . v) - (Lq . v))) by RLVECT_2: 54;

        

         A26: (L . v) >= 0 by Th62;

        per cases ;

          suppose

           A27: v = q;

          then not v in ( Carrier Lp) by A15, A20, TARSKI:def 1;

          then (Lp . v) = 0 ;

          hence thesis by A23, A14, A25, A26, A27;

        end;

          suppose

           A28: v = p;

          (L . p) >= mm by XXREAL_0: 17;

          then

           A29: ((L . p) - mm) >= (mm - mm) by XREAL_1: 9;

           not v in ( Carrier Lq) by A15, A17, A28, TARSKI:def 1;

          then (Lq . v) = 0 ;

          hence thesis by A19, A25, A28, A29;

        end;

          suppose

           A30: v <> p & v <> q;

          then not v in ( Carrier Lq) by A17, TARSKI:def 1;

          then

           A31: (Lq . v) = 0 ;

           not v in ( Carrier Lp) by A20, A30, TARSKI:def 1;

          then (Lp . v) = 0 ;

          hence thesis by A25, A31, Th62;

        end;

      end;

      ( Sum (Lp - Lq)) = (( Sum Lp) - ( Sum Lq)) by RLVECT_3: 4

      .= ((mm * p) - ( Sum Lq)) by A19, RLVECT_2: 32

      .= ((mm * p) - (mm * q)) by A14, RLVECT_2: 32

      .= (mm * (p - q)) by RLVECT_1: 34;

      then

       A32: ( Sum (Lp - Lq)) <> ( 0. V) by A23, A16, RLVECT_1: 11;

      

       A33: ( sum (Lp - Lq)) = (( sum Lp) - ( sum Lq)) by Th36

      .= (mm - ( sum Lq)) by A19, A20, Th32

      .= (mm - mm) by A14, A17, Th32

      .= 0 ;

      

       A34: for v holds (Lpq . v) >= 0

      proof

        let v;

        

         A35: (Lpq . v) = ((L . v) + ((Lp - Lq) . v)) by RLVECT_2:def 10

        .= ((L . v) + ((Lp . v) - (Lq . v))) by RLVECT_2: 54;

        

         A36: (L . v) >= 0 by Th62;

        per cases ;

          suppose

           A37: v = p;

          then not v in ( Carrier Lq) by A15, A17, TARSKI:def 1;

          then (Lpq . v) = ((L . v) + (mm - 0 )) by A19, A35, A37;

          hence thesis by A23, A36;

        end;

          suppose

           A38: v = q;

          (L . q) >= mm by XXREAL_0: 17;

          then

           A39: ((L . q) - mm) >= (mm - mm) by XREAL_1: 9;

           not v in ( Carrier Lp) by A15, A20, A38, TARSKI:def 1;

          then (Lp . v) = 0 ;

          hence thesis by A14, A35, A38, A39;

        end;

          suppose

           A40: v <> p & v <> q;

          then not v in ( Carrier Lq) by A17, TARSKI:def 1;

          then

           A41: (Lq . v) = 0 ;

           not v in ( Carrier Lp) by A20, A40, TARSKI:def 1;

          then (Lp . v) = 0 ;

          hence thesis by A35, A41, Th62;

        end;

      end;

      ( sum L1pq) = (( sum L) - ( sum (Lp - Lq))) by Th36

      .= (1 + 0 ) by A33, Th62;

      then

       A42: L1pq is convex by A24, Th62;

      then L1pq in ( ConvexComb V) by CONVEX3:def 1;

      then

       A43: ( Sum L1pq) in ( conv A1) by A3, A42;

      ( sum Lpq) = (( sum L) + ( sum (Lp - Lq))) by Th34

      .= (1 + 0 ) by A33, Th62;

      then

       A44: Lpq is convex by A34, Th62;

      then Lpq in ( ConvexComb V) by CONVEX3:def 1;

      then

       A45: ( Sum Lpq) in ( conv A) by A3, A44;

      ( 0. V) = ( - ( 0. V));

      then ( - ( Sum (Lp - Lq))) <> ( 0. V) by A32;

      then ( Sum L1pq) <> x by A5, A22, RLVECT_1: 9;

      then

       A46: ( Sum L1pq) in (( conv A) \ {x}) by A43, ZFMISC_1: 56;

      ( Sum Lpq) = (( Sum L) + ( Sum (Lp - Lq))) by RLVECT_3: 1;

      then ( Sum Lpq) <> x by A5, A32, RLVECT_1: 9;

      then

       A47: ( Sum Lpq) in (( conv A) \ {x}) by A45, ZFMISC_1: 56;

      (((1 / 2) * ( Sum Lpq)) + ((1 - (1 / 2)) * ( Sum L1pq))) = (((1 / 2) * (( Sum L) + ( Sum (Lp - Lq)))) + ((1 / 2) * (( Sum L) + ( - ( Sum (Lp - Lq)))))) by A22, RLVECT_3: 1

      .= ((((1 / 2) * ( Sum L)) + ((1 / 2) * ( Sum (Lp - Lq)))) + ((1 / 2) * (( Sum L) + ( - ( Sum (Lp - Lq)))))) by RLVECT_1:def 5

      .= ((((1 / 2) * ( Sum L)) + ((1 / 2) * ( Sum (Lp - Lq)))) + (((1 / 2) * ( Sum L)) + ((1 / 2) * ( - ( Sum (Lp - Lq)))))) by RLVECT_1:def 5

      .= (((1 / 2) * ( Sum L)) + (((1 / 2) * ( Sum (Lp - Lq))) + (((1 / 2) * ( - ( Sum (Lp - Lq)))) + ((1 / 2) * ( Sum L))))) by RLVECT_1:def 3

      .= (((1 / 2) * ( Sum L)) + ((((1 / 2) * ( Sum (Lp - Lq))) + ((1 / 2) * ( - ( Sum (Lp - Lq))))) + ((1 / 2) * ( Sum L)))) by RLVECT_1:def 3

      .= (((1 / 2) * ( Sum L)) + (((1 / 2) * (( Sum (Lp - Lq)) + ( - ( Sum (Lp - Lq))))) + ((1 / 2) * ( Sum L)))) by RLVECT_1:def 5

      .= (((1 / 2) * ( Sum L)) + (((1 / 2) * ( 0. V)) + ((1 / 2) * ( Sum L)))) by RLVECT_1: 5

      .= (((1 / 2) * ( Sum L)) + (( 0. V) + ((1 / 2) * ( Sum L))))

      .= (((1 / 2) * ( Sum L)) + ((1 / 2) * ( Sum L)))

      .= (((1 / 2) + (1 / 2)) * ( Sum L)) by RLVECT_1:def 6

      .= ( Sum L) by RLVECT_1:def 8;

      then ( Sum L) in (( conv A) \ {x}) by A2, A46, A47;

      hence contradiction by A5, ZFMISC_1: 56;

    end;

    theorem :: RLAFFIN1:67

    

     Th67: ( Affin ( conv A)) = ( Affin A)

    proof

      thus ( Affin ( conv A)) c= ( Affin A) by Th51, Th65;

      let x be object;

      assume x in ( Affin A);

      then x in { ( Sum L) where L be Linear_Combination of A : ( sum L) = 1 } by Th59;

      then

      consider L be Linear_Combination of A such that

       A1: x = ( Sum L) and

       A2: ( sum L) = 1;

      reconsider K = L as Linear_Combination of ( conv A) by Lm1, RLVECT_2: 21;

      ( Sum K) in { ( Sum M) where M be Linear_Combination of ( conv A) : ( sum M) = 1 } by A2;

      hence thesis by A1, Th59;

    end;

    theorem :: RLAFFIN1:68

    ( conv A) c= ( conv B) implies ( Affin A) c= ( Affin B)

    proof

      ( Affin ( conv A)) = ( Affin A) & ( Affin ( conv B)) = ( Affin B) by Th67;

      hence thesis by Th52;

    end;

    theorem :: RLAFFIN1:69

    

     Th69: for A,B be Subset of RLS st A c= ( Affin B) holds ( Affin (A \/ B)) = ( Affin B)

    proof

      let A,B be Subset of RLS such that

       A1: A c= ( Affin B);

      set AB = { C where C be Affine Subset of RLS : (A \/ B) c= C };

      B c= ( Affin B) by Lm7;

      then (A \/ B) c= ( Affin B) by A1, XBOOLE_1: 8;

      then ( Affin B) in AB;

      then

       A2: ( Affin (A \/ B)) c= ( Affin B) by SETFAM_1: 3;

      ( Affin B) c= ( Affin (A \/ B)) by Th52, XBOOLE_1: 7;

      hence thesis by A2;

    end;

    begin

    definition

      let V;

      let A;

      let x be object;

      :: RLAFFIN1:def7

      func x |-- A -> Linear_Combination of A means

      : Def7: ( Sum it ) = x & ( sum it ) = 1;

      existence

      proof

        ( Affin A) = { ( Sum L) where L be Linear_Combination of A : ( sum L) = 1 } by Th59;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let L1,L2 be Linear_Combination of A such that

         A3: ( Sum L1) = x and

         A4: ( sum L1) = 1 and

         A5: ( Sum L2) = x and

         A6: ( sum L2) = 1;

        

         A7: ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L1)) by A3, A5, RLVECT_3: 4

        .= ( 0. V) by RLVECT_1: 15;

        

         A8: (L1 - L2) is Linear_Combination of A by RLVECT_2: 56;

        ( sum (L1 - L2)) = (1 - 1) by A4, A6, Th36

        .= 0 ;

        then ( Carrier (L1 - L2)) = {} by A1, A7, A8, Th42;

        then ( ZeroLC V) = (L1 + ( - L2)) by RLVECT_2:def 5;

        then

         A9: ( - L2) = ( - L1) by RLVECT_2: 50;

        L1 = ( - ( - L1)) by RLVECT_2: 53;

        hence thesis by A9, RLVECT_2: 53;

      end;

    end

    theorem :: RLAFFIN1:70

    

     Th70: v1 in ( Affin I) & v2 in ( Affin I) implies ((((1 - r) * v1) + (r * v2)) |-- I) = (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)))

    proof

      assume that

       A1: v1 in ( Affin I) and

       A2: v2 in ( Affin I);

      set rv12 = (((1 - r) * v1) + (r * v2));

      

       A3: rv12 in ( Affin I) by A1, A2, RUSUB_4:def 4;

      ((1 - r) * (v1 |-- I)) is Linear_Combination of I & (r * (v2 |-- I)) is Linear_Combination of I by RLVECT_2: 44;

      then

       A4: (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))) is Linear_Combination of I by RLVECT_2: 38;

      

       A5: ( Sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)))) = (( Sum ((1 - r) * (v1 |-- I))) + ( Sum (r * (v2 |-- I)))) by RLVECT_3: 1

      .= (((1 - r) * ( Sum (v1 |-- I))) + ( Sum (r * (v2 |-- I)))) by RLVECT_3: 2

      .= (((1 - r) * ( Sum (v1 |-- I))) + (r * ( Sum (v2 |-- I)))) by RLVECT_3: 2

      .= (((1 - r) * v1) + (r * ( Sum (v2 |-- I)))) by A1, Def7

      .= rv12 by A2, Def7;

      ( sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)))) = (( sum ((1 - r) * (v1 |-- I))) + ( sum (r * (v2 |-- I)))) by Th34

      .= (((1 - r) * ( sum (v1 |-- I))) + ( sum (r * (v2 |-- I)))) by Th35

      .= (((1 - r) * ( sum (v1 |-- I))) + (r * ( sum (v2 |-- I)))) by Th35

      .= (((1 - r) * 1) + (r * ( sum (v2 |-- I)))) by A1, Def7

      .= (((1 - r) * 1) + (r * 1)) by A2, Def7

      .= 1;

      hence thesis by A3, A4, A5, Def7;

    end;

    theorem :: RLAFFIN1:71

    

     Th71: x in ( conv I) implies (x |-- I) is convex & 0 <= ((x |-- I) . v) & ((x |-- I) . v) <= 1

    proof

      assume

       A1: x in ( conv I);

      then

      reconsider I1 = I as non empty Subset of V;

      ( conv I1) = { ( Sum L) where L be Convex_Combination of I1 : L in ( ConvexComb V) } by CONVEX3: 5;

      then

      consider L be Convex_Combination of I1 such that

       A2: ( Sum L) = x and L in ( ConvexComb V) by A1;

      ( conv I) c= ( Affin I) & ( sum L) = 1 by Th62, Th65;

      then L = (x |-- I) by A1, A2, Def7;

      hence thesis by Th62, Th63;

    end;

    theorem :: RLAFFIN1:72

    

     Th72: x in ( conv I) implies (((x |-- I) . y) = 1 iff x = y & x in I)

    proof

      assume

       A1: x in ( conv I);

      then

      reconsider v = x as Element of V;

      hereby

        assume

         A2: ((x |-- I) . y) = 1;

        (x |-- I) is convex by A1, Th71;

        then

         A3: ( Carrier (x |-- I)) = {y} by A2, Th64;

        y in {y} by TARSKI:def 1;

        then

        reconsider v = y as Element of V by A3;

        ( conv I) c= ( Affin I) by Th65;

        

        hence

         A4: x = ( Sum (x |-- I)) by A1, Def7

        .= (((x |-- I) . v) * v) by A3, RLVECT_2: 35

        .= y by A2, RLVECT_1:def 8;

        ( Carrier (x |-- I)) c= I & v in ( Carrier (x |-- I)) by A2, RLVECT_2:def 6;

        hence x in I by A4;

      end;

      assume that

       A5: x = y and

       A6: x in I;

      consider L be Linear_Combination of {v} such that

       A7: (L . v) = jj by RLVECT_4: 37;

      ( Carrier L) c= {v} by RLVECT_2:def 6;

      then

       A8: ( sum L) = 1 by A7, Th32;

      

       A9: I c= ( Affin I) by Lm7;

       {v} c= I by A6, ZFMISC_1: 31;

      then

       A10: L is Linear_Combination of I by RLVECT_2: 21;

      ( Sum L) = (1 * v) by A7, RLVECT_2: 32

      .= v by RLVECT_1:def 8;

      hence thesis by A5, A6, A7, A8, A9, A10, Def7;

    end;

    theorem :: RLAFFIN1:73

    

     Th73: for I st x in ( Affin I) & for v st v in I holds 0 <= ((x |-- I) . v) holds x in ( conv I)

    proof

      let I such that

       A1: x in ( Affin I) and

       A2: for v st v in I holds 0 <= ((x |-- I) . v);

      set xI = (x |-- I);

      

       A3: ( Sum xI) = x by A1, Def7;

      reconsider I1 = I as non empty Subset of V by A1;

      

       A4: for v holds 0 <= (xI . v)

      proof

        let v;

        

         A5: v in ( Carrier xI) or not v in ( Carrier xI);

        ( Carrier xI) c= I by RLVECT_2:def 6;

        hence thesis by A2, A5;

      end;

      ( sum xI) = 1 by A1, Def7;

      then

       A6: xI is convex by A4, Th62;

      then ( conv I1) = { ( Sum L) where L be Convex_Combination of I1 : L in ( ConvexComb V) } & xI in ( ConvexComb V) by CONVEX3: 5, CONVEX3:def 1;

      hence thesis by A3, A6;

    end;

    theorem :: RLAFFIN1:74

    x in I implies (( conv I) \ {x}) is convex

    proof

      assume

       A1: x in I;

      then

      reconsider X = x as Element of V;

      

       A2: ( conv I) c= ( Affin I) by Th65;

      now

        let v1, v2, r;

        set rv12 = ((r * v1) + ((1 - r) * v2));

        assume that

         A3: 0 < r and

         A4: r < 1;

        assume that

         A5: v1 in (( conv I) \ {x}) and

         A6: v2 in (( conv I) \ {x});

        

         A7: (1 - r) > (1 - 1) by A4, XREAL_1: 10;

        

         A8: v2 in ( conv I) by A6, ZFMISC_1: 56;

        then

         A9: ((v2 |-- I) . X) <= 1 by Th71;

        

         A10: v1 in ( conv I) by A5, ZFMISC_1: 56;

        then

         A11: ((v1 |-- I) . X) <= 1 by Th71;

        

         A12: (rv12 |-- I) = (((1 - r) * (v2 |-- I)) + (r * (v1 |-- I))) by A2, A10, A8, Th70;

         A13:

        now

          let w;

          assume w in I;

          

           A14: ((rv12 |-- I) . w) = ((((1 - r) * (v2 |-- I)) . w) + ((r * (v1 |-- I)) . w)) by A12, RLVECT_2:def 10

          .= (((1 - r) * ((v2 |-- I) . w)) + ((r * (v1 |-- I)) . w)) by RLVECT_2:def 11

          .= (((1 - r) * ((v2 |-- I) . w)) + (r * ((v1 |-- I) . w))) by RLVECT_2:def 11;

          ((v2 |-- I) . w) >= 0 & ((v1 |-- I) . w) >= 0 by A10, A8, Th71;

          hence 0 <= ((rv12 |-- I) . w) by A3, A7, A14;

        end;

        rv12 in ( Affin I) by A2, A10, A8, RUSUB_4:def 4;

        then

         A15: rv12 in ( conv I) by A13, Th73;

        v1 <> x by A5, ZFMISC_1: 56;

        then ((v1 |-- I) . X) <> 1 by A10, Th72;

        then ((v1 |-- I) . X) < 1 by A11, XXREAL_0: 1;

        then

         A16: (r * ((v1 |-- I) . X)) < (r * 1) by A3, XREAL_1: 68;

        v2 <> x by A6, ZFMISC_1: 56;

        then ((v2 |-- I) . X) <> 1 by A8, Th72;

        then ((v2 |-- I) . X) < 1 by A9, XXREAL_0: 1;

        then ((1 - r) * ((v2 |-- I) . X)) < ((1 - r) * 1) by A7, XREAL_1: 68;

        then

         A17: (((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X))) < (((1 - r) * 1) + (r * 1)) by A16, XREAL_1: 8;

        ((rv12 |-- I) . X) = ((((1 - r) * (v2 |-- I)) . X) + ((r * (v1 |-- I)) . X)) by A12, RLVECT_2:def 10

        .= (((1 - r) * ((v2 |-- I) . X)) + ((r * (v1 |-- I)) . X)) by RLVECT_2:def 11

        .= (((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X))) by RLVECT_2:def 11;

        then rv12 <> X by A1, A15, A17, Th72;

        hence rv12 in (( conv I) \ {x}) by A15, ZFMISC_1: 56;

      end;

      hence thesis;

    end;

    theorem :: RLAFFIN1:75

    

     Th75: for B st x in ( Affin I) & for y st y in B holds ((x |-- I) . y) = 0 holds x in ( Affin (I \ B)) & (x |-- I) = (x |-- (I \ B))

    proof

      let B such that

       A1: x in ( Affin I) and

       A2: for y st y in B holds ((x |-- I) . y) = 0 ;

      

       A3: ( Affin I) = { ( Sum L) where L be Linear_Combination of I : ( sum L) = 1 } by Th59;

      

       A4: (I \ B) is affinely-independent by Th43, XBOOLE_1: 36;

      consider L be Linear_Combination of I such that

       A5: x = ( Sum L) & ( sum L) = 1 by A1, A3;

      

       A6: (x |-- I) = L by A1, A5, Def7;

      ( Carrier L) c= (I \ B)

      proof

        

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

        let y be object such that

         A8: y in ( Carrier L);

        assume not y in (I \ B);

        then y in B by A7, A8, XBOOLE_0:def 5;

        then (L . y) = 0 by A2, A6;

        hence thesis by A8, RLVECT_2: 19;

      end;

      then

       A9: L is Linear_Combination of (I \ B) by RLVECT_2:def 6;

      then x in { ( Sum K) where K be Linear_Combination of (I \ B) : ( sum K) = 1 } by A5;

      then x in ( Affin (I \ B)) by Th59;

      hence thesis by A4, A5, A6, A9, Def7;

    end;

    theorem :: RLAFFIN1:76

    for B st x in ( conv I) & for y st y in B holds ((x |-- I) . y) = 0 holds x in ( conv (I \ B))

    proof

      let B such that

       A1: x in ( conv I) and

       A2: for y st y in B holds ((x |-- I) . y) = 0 ;

      set IB = (I \ B);

      

       A3: ( conv I) c= ( Affin I) by Th65;

      then (x |-- I) = (x |-- IB) by A1, A2, Th75;

      then

       A4: for v st v in IB holds 0 <= ((x |-- IB) . v) by A1, Th71;

      

       A5: IB is affinely-independent by Th43, XBOOLE_1: 36;

      x in ( Affin IB) by A1, A2, A3, Th75;

      hence thesis by A4, A5, Th73;

    end;

    theorem :: RLAFFIN1:77

    

     Th77: B c= I & x in ( Affin B) implies (x |-- B) = (x |-- I)

    proof

      assume that

       A1: B c= I and

       A2: x in ( Affin B);

      B is affinely-independent by A1, Th43;

      then

       A3: ( Sum (x |-- B)) = x & ( sum (x |-- B)) = 1 by A2, Def7;

      ( Affin B) c= ( Affin I) & (x |-- B) is Linear_Combination of I by A1, Th52, RLVECT_2: 21;

      hence thesis by A2, A3, Def7;

    end;

    theorem :: RLAFFIN1:78

    

     Th78: v1 in ( Affin A) & v2 in ( Affin A) & (r + s) = 1 implies ((r * v1) + (s * v2)) in ( Affin A)

    proof

      

       A1: ( Affin A) = { ( Sum L) where L be Linear_Combination of A : ( sum L) = 1 } by Th59;

      assume v1 in ( Affin A);

      then

      consider L1 be Linear_Combination of A such that

       A2: v1 = ( Sum L1) and

       A3: ( sum L1) = 1 by A1;

      assume v2 in ( Affin A);

      then

      consider L2 be Linear_Combination of A such that

       A4: v2 = ( Sum L2) and

       A5: ( sum L2) = 1 by A1;

      

       A6: ( Sum ((r * L1) + (s * L2))) = (( Sum (r * L1)) + ( Sum (s * L2))) by RLVECT_3: 1

      .= ((r * ( Sum L1)) + ( Sum (s * L2))) by RLVECT_3: 2

      .= ((r * v1) + (s * v2)) by A2, A4, RLVECT_3: 2;

      (r * L1) is Linear_Combination of A & (s * L2) is Linear_Combination of A by RLVECT_2: 44;

      then

       A7: ((r * L1) + (s * L2)) is Linear_Combination of A by RLVECT_2: 38;

      assume

       A8: (r + s) = 1;

      ( sum ((r * L1) + (s * L2))) = (( sum (r * L1)) + ( sum (s * L2))) by Th34

      .= ((r * ( sum L1)) + ( sum (s * L2))) by Th35

      .= ((r * 1) + (s * 1)) by A3, A5, Th35

      .= 1 by A8;

      hence thesis by A1, A7, A6;

    end;

    theorem :: RLAFFIN1:79

    

     Th79: for A,B be finite Subset of V st A is affinely-independent & ( Affin A) c= ( Affin B) holds ( card A) <= ( card B)

    proof

      let A,B be finite Subset of V such that

       A1: A is affinely-independent and

       A2: ( Affin A) c= ( Affin B);

      per cases ;

        suppose A is empty;

        hence thesis;

      end;

        suppose A is non empty;

        then

        consider p be object such that

         A3: p in A;

        reconsider p as Element of V by A3;

        

         A4: A c= ( Affin A) by Lm7;

        then

         A5: p in ( Affin A) by A3;

        set LA = ( Lin (( - p) + A));

        

         A6: ( card A) = ( card (( - p) + A)) by Th7;

        ( {} V) c= B;

        then

        consider Ib be affinely-independent Subset of V such that ( {} V) c= Ib and

         A7: Ib c= B and

         A8: ( Affin Ib) = ( Affin B) by Th60;

        Ib is non empty by A2, A3, A8;

        then

        consider q be object such that

         A9: q in Ib;

        reconsider q as Element of V by A9;

        set LI = ( Lin (( - q) + Ib));

        

         A10: ( card Ib) = ( card (( - q) + Ib)) by Th7;

        (( - q) + Ib) c= the carrier of LI

        proof

          let x be object;

          assume x in (( - q) + Ib);

          then x in LI by RLVECT_3: 15;

          hence thesis;

        end;

        then

        reconsider qI = (( - q) + Ib) as finite Subset of LI by A7, A10;

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

        then

         A11: ( 0. V) in qI by A9;

        

        then

         A12: ( Lin (( - q) + Ib)) = ( Lin (((( - q) + Ib) \ {( 0. V)}) \/ {( 0. V)})) by ZFMISC_1: 116

        .= ( Lin ((( - q) + Ib) \ {( 0. V)})) by Lm9

        .= ( Lin (qI \ {( 0. V)})) by RLVECT_5: 20;

        

         A13: ((( - q) + Ib) \ {( 0. V)}) is linearly-independent by A9, Th41;

        then (qI \ {( 0. V)}) is linearly-independent by RLVECT_5: 15;

        then (qI \ {( 0. V)}) is Basis of LI by A12, RLVECT_3:def 3;

        then

        reconsider LI as finite-dimensional Subspace of V by RLVECT_5:def 1;

        

         A14: Ib c= ( Affin Ib) by Lm7;

        then

         A15: ( Affin Ib) = (q + ( Up LI)) by A9, Th57;

        

         A16: ( Affin A) = (p + ( Up LA)) by A3, A4, Th57;

        (( - p) + A) c= the carrier of LI

        proof

          let x be object;

          

           A17: (2 + ( - 1)) = 1;

          ((2 * q) + (( - 1) * p)) = (((1 + 1) * q) + (( - 1) * p))

          .= (((1 * q) + (1 * q)) + (( - 1) * p)) by RLVECT_1:def 6

          .= (((1 * q) + (1 * q)) + ( - p)) by RLVECT_1: 16

          .= (((1 * q) + q) + ( - p)) by RLVECT_1:def 8

          .= ((q + q) + ( - p)) by RLVECT_1:def 8

          .= ((q + q) - p) by RLVECT_1:def 11

          .= ((q - p) + q) by RLVECT_1: 28;

          then (q + ( Up LI)) = (q + LI) & ((q - p) + q) in (q + ( Up LI)) by A2, A8, A5, A9, A14, A15, A17, Th78, RUSUB_4: 30;

          then

           A18: (q - p) in LI by RLSUB_1: 61;

          assume x in (( - p) + A);

          then

           A19: x in LA by RLVECT_3: 15;

          then x in V by RLSUB_1: 9;

          then

          reconsider w = x as Element of V;

          w in ( Up LA) by A19;

          then (p + w) in ( Affin A) by A16;

          then (p + w) in (q + ( Up LI)) by A2, A8, A15;

          then

          consider u be Element of V such that

           A20: (p + w) = (q + u) and

           A21: u in ( Up LI);

          

           A22: w = ((q + u) - p) by A20, RLVECT_4: 1

          .= (q + (u - p)) by RLVECT_1: 28

          .= (u - (p - q)) by RLVECT_1: 29

          .= (u + ( - (p - q))) by RLVECT_1:def 11

          .= (u + (q + ( - p))) by RLVECT_1: 33

          .= (u + (q - p)) by RLVECT_1:def 11;

          u in LI by A21;

          then w in LI by A18, A22, RLSUB_1: 20;

          hence thesis;

        end;

        then

        reconsider LA as Subspace of LI by RLVECT_5: 19;

        (( - p) + A) c= the carrier of LA

        proof

          let x be object;

          assume x in (( - p) + A);

          then x in LA by RLVECT_3: 15;

          hence thesis;

        end;

        then

        reconsider pA = (( - p) + A) as finite Subset of LA by A6;

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

        then

         A23: ( 0. V) in pA by A3;

        then

         A24: {( 0. V)} c= pA by ZFMISC_1: 31;

        

         A25: ((( - p) + A) \ {( 0. V)}) is linearly-independent by A1, A3, Th41;

        

         A26: ( card {( 0. V)}) = 1 by CARD_1: 30;

        

         A27: {( 0. V)} c= qI by A11, ZFMISC_1: 31;

        

         A28: ( dim LI) = ( card (qI \ {( 0. V)})) by A13, A12, RLVECT_5: 15, RLVECT_5: 29

        .= (( card qI) - 1) by A27, A26, CARD_2: 44;

        ( Lin (( - p) + A)) = ( Lin (((( - p) + A) \ {( 0. V)}) \/ {( 0. V)})) by A23, ZFMISC_1: 116

        .= ( Lin ((( - p) + A) \ {( 0. V)})) by Lm9

        .= ( Lin (pA \ {( 0. V)})) by RLVECT_5: 20;

        

        then ( dim LA) = ( card (pA \ {( 0. V)})) by A25, RLVECT_5: 15, RLVECT_5: 29

        .= (( card A) - 1) by A6, A26, A24, CARD_2: 44;

        then (( card A) - 1) <= (( card qI) - 1) by A28, RLVECT_5: 28;

        then

         A29: ( card A) <= ( card qI) by XREAL_1: 9;

        ( card qI) <= ( card B) by A7, A10, NAT_1: 43;

        hence thesis by A29, XXREAL_0: 2;

      end;

    end;

    theorem :: RLAFFIN1:80

    for A,B be finite Subset of V st A is affinely-independent & ( Affin A) c= ( Affin B) & ( card A) = ( card B) holds B is affinely-independent

    proof

      let A,B be finite Subset of V such that

       A1: A is affinely-independent & ( Affin A) c= ( Affin B) & ( card A) = ( card B);

      ( {} V) c= B;

      then

      consider Ib be affinely-independent Subset of V such that ( {} V) c= Ib and

       A2: Ib c= B and

       A3: ( Affin Ib) = ( Affin B) by Th60;

      reconsider IB = Ib as finite Subset of V by A2;

      

       A4: ( card IB) <= ( card B) by A3, Th79;

      ( card B) <= ( card IB) by A1, A3, Th79;

      hence thesis by A2, A4, CARD_2: 102, XXREAL_0: 1;

    end;

    theorem :: RLAFFIN1:81

    (L1 . v) <> (L2 . v) implies ((((r * L1) + ((1 - r) * L2)) . v) = s iff r = (((L2 . v) - s) / ((L2 . v) - (L1 . v))))

    proof

      set u1 = (L1 . v), u2 = (L2 . v);

      

       A1: (((r * L1) + ((1 - r) * L2)) . v) = (((r * L1) . v) + (((1 - r) * L2) . v)) by RLVECT_2:def 10

      .= ((r * u1) + (((1 - r) * L2) . v)) by RLVECT_2:def 11

      .= ((r * u1) + ((( - r) + 1) * u2)) by RLVECT_2:def 11

      .= ((r * (u1 - u2)) + u2);

      assume

       A2: u1 <> u2;

      then

       A3: (u1 - u2) <> 0 ;

      

       A4: (u2 - u1) <> 0 by A2;

      hereby

        assume (((r * L1) + ((1 - r) * L2)) . v) = s;

        then (r * (u2 - u1)) = ((u2 - s) * 1) by A1;

        then (r / 1) = ((u2 - s) / (u2 - u1)) by A4, XCMPLX_1: 94;

        hence r = ((u2 - s) / (u2 - u1));

      end;

      assume r = ((u2 - s) / (u2 - u1));

      

      hence (((r * L1) + ((1 - r) * L2)) . v) = ((((u2 - s) / ( - (u1 - u2))) * (u1 - u2)) + u2) by A1

      .= (((( - (u2 - s)) / (u1 - u2)) * (u1 - u2)) + u2) by XCMPLX_1: 192

      .= (( - (u2 - s)) + u2) by A3, XCMPLX_1: 87

      .= s;

    end;

    theorem :: RLAFFIN1:82

    (A \/ {v}) is affinely-independent iff A is affinely-independent & (v in A or not v in ( Affin A))

    proof

      set Av = (A \/ {v});

      v in {v} by TARSKI:def 1;

      then

       A1: v in Av by XBOOLE_0:def 3;

      

       A2: A c= Av by XBOOLE_1: 7;

      hereby

        assume

         A3: Av is affinely-independent;

        hence A is affinely-independent by Th43, XBOOLE_1: 7;

        v in ( Affin A) implies v in A

        proof

          assume v in ( Affin A);

          then {v} c= ( Affin A) by ZFMISC_1: 31;

          then ( Affin Av) = ( Affin A) by Th69;

          hence thesis by A2, A1, A3, Th58;

        end;

        hence v in A or not v in ( Affin A);

      end;

      assume that

       A4: A is affinely-independent and

       A5: v in A or not v in ( Affin A);

      per cases by A5;

        suppose v in A;

        hence thesis by A4, ZFMISC_1: 40;

      end;

        suppose

         A6: not v in ( Affin A) & not v in A;

        consider I be affinely-independent Subset of V such that

         A7: A c= I and

         A8: I c= Av and

         A9: ( Affin I) = ( Affin Av) by A2, A4, Th60;

        assume

         A10: not Av is affinely-independent;

         not v in I

        proof

          assume v in I;

          then {v} c= I by ZFMISC_1: 31;

          hence contradiction by A7, A10, Th43, XBOOLE_1: 8;

        end;

        then

         A11: I c= (Av \ {v}) by A8, ZFMISC_1: 34;

        

         A12: Av c= ( Affin Av) by Lm7;

        (Av \ {v}) = A by A6, ZFMISC_1: 117;

        then I = A by A7, A11;

        hence contradiction by A1, A6, A9, A12;

      end;

    end;

    theorem :: RLAFFIN1:83

     not w in ( Affin A) & v1 in A & v2 in A & r <> 1 & ((r * w) + ((1 - r) * v1)) = ((s * w) + ((1 - s) * v2)) implies r = s & v1 = v2

    proof

      assume that

       A1: ( not w in ( Affin A)) & v1 in A & v2 in A and

       A2: r <> 1 and

       A3: ((r * w) + ((1 - r) * v1)) = ((s * w) + ((1 - s) * v2));

      (r * w) = ((r * w) + ( 0. V))

      .= ((r * w) + (((1 - r) * v1) - ((1 - r) * v1))) by RLVECT_1: 15

      .= (((s * w) + ((1 - s) * v2)) - ((1 - r) * v1)) by A3, RLVECT_1: 28

      .= ((((1 - s) * v2) - ((1 - r) * v1)) + (s * w)) by RLVECT_1: 28;

      then ((r * w) - (s * w)) = (((1 - s) * v2) - ((1 - r) * v1)) by RLVECT_4: 1;

      then

       A4: ((r - s) * w) = (((1 - s) * v2) - ((1 - r) * v1)) by RLVECT_1: 35;

      

       A5: A c= ( Affin A) by Lm7;

      per cases ;

        suppose r <> s;

        then

         A6: (r - s) <> 0 ;

        

         A7: ((1 / (r - s)) * (1 - s)) = (((r - s) - (r - 1)) / (r - s)) by XCMPLX_1: 99

        .= (((r - s) / (r - s)) - ((r - 1) / (r - s))) by XCMPLX_1: 120

        .= (1 - ((r - 1) / (r - s))) by A6, XCMPLX_1: 60;

        

         A8: ( - ((1 / (r - s)) * (1 - r))) = ( - ((1 - r) / (r - s))) by XCMPLX_1: 99

        .= (( - (1 - r)) / (r - s)) by XCMPLX_1: 187;

        1 = ((r - s) * (1 / (r - s))) by A6, XCMPLX_1: 106;

        

        then w = (((1 / (r - s)) * (r - s)) * w) by RLVECT_1:def 8

        .= ((1 / (r - s)) * ((r - s) * w)) by RLVECT_1:def 7

        .= (((1 / (r - s)) * ((1 - s) * v2)) - ((1 / (r - s)) * ((1 - r) * v1))) by A4, RLVECT_1: 34

        .= ((((1 / (r - s)) * (1 - s)) * v2) - ((1 / (r - s)) * ((1 - r) * v1))) by RLVECT_1:def 7

        .= ((((1 / (r - s)) * (1 - s)) * v2) - (((1 / (r - s)) * (1 - r)) * v1)) by RLVECT_1:def 7

        .= ((((1 / (r - s)) * (1 - s)) * v2) + ( - (((1 / (r - s)) * (1 - r)) * v1))) by RLVECT_1:def 11

        .= (((1 - ((r - 1) / (r - s))) * v2) + (((r - 1) / (r - s)) * v1)) by A7, A8, RLVECT_4: 3;

        hence thesis by A1, A5, RUSUB_4:def 4;

      end;

        suppose

         A9: r = s;

        

         A10: (1 - r) <> 0 by A2;

        ((1 - r) * v1) = ((1 - r) * v2) by A3, A9, RLVECT_1: 8;

        hence thesis by A9, A10, RLVECT_1: 36;

      end;

    end;

    theorem :: RLAFFIN1:84

    v in I & w in ( Affin I) & p in ( Affin (I \ {v})) & w = ((r * v) + ((1 - r) * p)) implies r = ((w |-- I) . v)

    proof

      assume that

       A1: v in I and w in ( Affin I) and

       A2: p in ( Affin (I \ {v})) and

       A3: w = ((r * v) + ((1 - r) * p));

      

       A4: I c= ( conv I) by CONVEX1: 41;

      ( Carrier (p |-- (I \ {v}))) c= (I \ {v}) by RLVECT_2:def 6;

      then not v in ( Carrier (p |-- (I \ {v}))) by ZFMISC_1: 56;

      then

       A5: ((p |-- (I \ {v})) . v) = 0 ;

      (I \ {v}) c= I by XBOOLE_1: 36;

      then ( Affin (I \ {v})) c= ( Affin I) & I c= ( Affin I) by Lm7, Th52;

      

      hence ((w |-- I) . v) = ((((1 - r) * (p |-- I)) + (r * (v |-- I))) . v) by A1, A2, A3, Th70

      .= ((((1 - r) * (p |-- I)) . v) + ((r * (v |-- I)) . v)) by RLVECT_2:def 10

      .= ((((1 - r) * (p |-- I)) . v) + (r * ((v |-- I) . v))) by RLVECT_2:def 11

      .= (((1 - r) * ((p |-- I) . v)) + (r * ((v |-- I) . v))) by RLVECT_2:def 11

      .= (((1 - r) * ((p |-- I) . v)) + (r * 1)) by A1, A4, Th72

      .= (((1 - r) * ((p |-- (I \ {v})) . v)) + (r * 1)) by A2, Th77, XBOOLE_1: 36

      .= r by A5;

    end;