midsp_3.miz



    begin

    reserve n,i,j,k,l for Nat;

    reserve D for non empty set;

    reserve c,d for Element of D;

    reserve p,q,q9,r for FinSequence of D;

    theorem :: MIDSP_3:1

    ( len p) = ((j + 1) + k) implies ex q, r, c st ( len q) = j & ( len r) = k & p = ((q ^ <*c*>) ^ r)

    proof

      assume ( len p) = ((j + 1) + k);

      then

      consider q9, r such that

       A1: ( len q9) = (j + 1) and

       A2: ( len r) = k & p = (q9 ^ r) by FINSEQ_2: 23;

      consider q, c such that

       A3: q9 = (q ^ <*c*>) by A1, FINSEQ_2: 19;

      take q, r, c;

      ( len q9) = (( len q) + 1) by A3, FINSEQ_2: 16;

      hence thesis by A1, A2, A3;

    end;

    theorem :: MIDSP_3:2

    i in ( Seg n) implies ex j, k st n = ((j + 1) + k) & i = (j + 1)

    proof

      assume

       A1: i in ( Seg n);

      then 1 <= i by FINSEQ_1: 1;

      then

      consider j be Nat such that

       A2: i = (1 + j) by NAT_1: 10;

      reconsider j as Element of NAT by ORDINAL1:def 12;

      i <= n by A1, FINSEQ_1: 1;

      then

      consider k be Nat such that

       A3: n = ((j + 1) + k) by A2, NAT_1: 10;

      reconsider k as Element of NAT by ORDINAL1:def 12;

      take j, k;

      thus thesis by A2, A3;

    end;

    theorem :: MIDSP_3:3

    p = ((q ^ <*c*>) ^ r) & i = (( len q) + 1) implies (for l st 1 <= l & l <= ( len q) holds (p . l) = (q . l)) & (p . i) = c & for l st (i + 1) <= l & l <= ( len p) holds (p . l) = (r . (l - i))

    proof

      set q9 = (q ^ <*c*>);

      assume that

       A1: p = (q9 ^ r) and

       A2: i = (( len q) + 1);

      

       A3: p = (q ^ ( <*c*> ^ r)) by A1, FINSEQ_1: 32;

      thus for l st 1 <= l & l <= ( len q) holds (p . l) = (q . l)

      proof

        let l;

        assume 1 <= l & l <= ( len q);

        then l in ( dom q) by FINSEQ_3: 25;

        hence thesis by A3, FINSEQ_1:def 7;

      end;

      

       A4: ( len q9) = i by A2, FINSEQ_2: 16;

      i in ( Seg i) by A2, FINSEQ_1: 3;

      then i in ( dom q9) by A4, FINSEQ_1:def 3;

      

      hence (p . i) = (q9 . i) by A1, FINSEQ_1:def 7

      .= c by A2, FINSEQ_1: 42;

      ( len p) = (( len q9) + ( len r)) by A1, FINSEQ_1: 22;

      hence thesis by A1, A4, FINSEQ_1: 23;

    end;

    theorem :: MIDSP_3:4

    

     Th4: l <= j or l = (j + 1) or (j + 2) <= l

    proof

      

       A1: ((j + 1) + 1) = (j + 2);

      l < (j + 1) or l = (j + 1) or (j + 1) < l by XXREAL_0: 1;

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: MIDSP_3:5

    l in (( Seg n) \ {i}) & i = (j + 1) implies 1 <= l & l <= j or (i + 1) <= l & l <= n

    proof

      assume that

       A1: l in (( Seg n) \ {i}) and

       A2: i = (j + 1);

      

       A3: (i + 1) = (j + 2) by A2;

      l in ( Seg n) & l <> i by A1, ZFMISC_1: 56;

      hence thesis by A2, A3, Th4, FINSEQ_1: 1;

    end;

    definition

      let D, n;

      let p be Element of (n -tuples_on D);

      let i, d;

      :: original: +*

      redefine

      func p +* (i,d) -> Element of (n -tuples_on D) ;

      coherence

      proof

        ( dom (p +* (i,d))) = ( dom p) by FUNCT_7: 30;

        

        then ( len (p +* (i,d))) = ( len p) by FINSEQ_3: 29

        .= n by CARD_1:def 7;

        hence (p +* (i,d)) is Element of (n -tuples_on D) by FINSEQ_2: 92;

      end;

    end

    

     Lm1: for p be Element of (n -tuples_on D) st i in ( Seg n) holds ((p +* (i,d)) . i) = d

    proof

      let p be Element of (n -tuples_on D);

      ( Seg n) = ( dom p) by FINSEQ_2: 124;

      hence thesis by FUNCT_7: 31;

    end;

    

     Lm2: for p be Element of (n -tuples_on D) holds for l st l in (( dom p) \ {i}) holds ((p +* (i,d)) . l) = (p . l)

    proof

      let p be Element of (n -tuples_on D);

      let l;

      assume l in (( dom p) \ {i});

      then not l in {i} by XBOOLE_0:def 5;

      then l <> i by TARSKI:def 1;

      hence thesis by FUNCT_7: 32;

    end;

    begin

    definition

      let n;

      struct ( MidStr) ReperAlgebraStr over n (# the carrier -> set,

the MIDPOINT -> BinOp of the carrier,

the reper -> Function of (n -tuples_on the carrier), the carrier #)

       attr strict strict;

    end

    registration

      let n;

      let A be non empty set, m be BinOp of A, r be Function of (n -tuples_on A), A;

      cluster ReperAlgebraStr (# A, m, r #) -> non empty;

      coherence ;

    end

     Lm3:

    now

      let n;

      let M be MidSp;

      let R be Function of ((n + 2) -tuples_on the carrier of M), the carrier of M;

      set RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);

      thus RA is MidSp-like

      proof

        let a,b,c,d be Element of RA;

        reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of M;

        

        thus (a @ a) = (a9 @ a9)

        .= a by MIDSP_1:def 3;

        consider x9 be Element of M such that

         A1: (x9 @ a9) = b9 by MIDSP_1:def 3;

        for a,b be Element of RA, a9,b9 be Element of M st a = a9 & b = b9 holds (a @ b) = (a9 @ b9);

        

        hence (a @ b) = (b9 @ a9)

        .= (b @ a);

        reconsider x = x9 as Element of RA;

        

        thus ((a @ b) @ (c @ d)) = ((a9 @ b9) @ (c9 @ d9))

        .= ((a9 @ c9) @ (b9 @ d9)) by MIDSP_1:def 3

        .= ((a @ c) @ (b @ d));

        take x;

        thus thesis by A1;

      end;

    end;

    registration

      let n;

      cluster non empty for ReperAlgebraStr over n;

      existence

      proof

        set A = the non empty set, m = the BinOp of A, r = the Function of (n -tuples_on A), A;

        take ReperAlgebraStr (# A, m, r #);

        thus thesis;

      end;

    end

    registration

      let n;

      cluster MidSp-like for non empty ReperAlgebraStr over (n + 2);

      existence

      proof

        set M = the MidSp;

        set R = the Function of ((n + 2) -tuples_on the carrier of M), the carrier of M;

        take ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);

        thus thesis by Lm3;

      end;

    end

    reserve RAS for MidSp-like non empty ReperAlgebraStr over (n + 2);

    reserve a,b,d,pii,p9i for Point of RAS;

    definition

      let n, RAS, i;

      mode Tuple of i,RAS is Element of (i -tuples_on the carrier of RAS);

    end

    reserve p,q for Tuple of (n + 1), RAS;

    definition

      let n, RAS, a;

      :: original: <*

      redefine

      func <*a*> -> Tuple of 1, RAS ;

      coherence by FINSEQ_2: 98;

    end

    definition

      let n, RAS, i, j;

      let p be Tuple of i, RAS, q be Tuple of j, RAS;

      :: original: ^

      redefine

      func p ^ q -> Tuple of (i + j), RAS ;

      coherence

      proof

        reconsider p as Tuple of i, the carrier of RAS;

        reconsider q as Tuple of j, the carrier of RAS;

        (p ^ q) is Tuple of (i + j), the carrier of RAS by FINSEQ_2: 107;

        hence thesis by FINSEQ_2: 131;

      end;

    end

    definition

      let n, RAS, a, p;

      :: MIDSP_3:def1

      func *' (a,p) -> Point of RAS equals (the reper of RAS . ( <*a*> ^ p));

      coherence

      proof

        reconsider p9 = ( <*a*> ^ p) as Tuple of (n + 2), RAS;

        (the reper of RAS . p9) is Point of RAS;

        hence thesis;

      end;

    end

    theorem :: MIDSP_3:6

    i in ( Seg (n + 1)) implies ((p +* (i,d)) . i) = d & for l st l in (( dom p) \ {i}) holds ((p +* (i,d)) . l) = (p . l) by Lm1, Lm2;

    definition

      let n;

      :: MIDSP_3:def2

      mode Nat of n -> Nat means

      : Def2: 1 <= it & it <= (n + 1);

      existence

      proof

        take 1;

         0 <= n by NAT_1: 2;

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

        hence thesis;

      end;

    end

    reserve m for Nat of n;

    theorem :: MIDSP_3:7

    

     Th7: i is Nat of n iff i in ( Seg (n + 1))

    proof

      i is Nat of n iff 1 <= i & i <= (n + 1) by Def2;

      hence thesis by FINSEQ_1: 1;

    end;

    theorem :: MIDSP_3:8

    

     Th8: i <= n implies (i + 1) is Nat of n

    proof

      assume i <= n;

      then

       A1: (i + 1) <= (n + 1) by XREAL_1: 7;

      1 <= (i + 1) by NAT_1: 11;

      hence thesis by A1, Def2;

    end;

    theorem :: MIDSP_3:9

    

     Th9: (for m holds (p . m) = (q . m)) implies p = q

    proof

      assume

       A1: for m holds (p . m) = (q . m);

      for j be Nat st j in ( Seg (n + 1)) holds (p . j) = (q . j)

      proof

        let j be Nat;

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

        then

        reconsider j as Nat of n by Th7;

        (p . j) = (q . j) by A1;

        hence thesis;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: MIDSP_3:10

    

     Th10: for l be Nat of n st l = i holds ((p +* (i,d)) . l) = d

    proof

      let l be Nat of n such that

       A1: l = i;

      l in ( Seg (n + 1)) by Th7;

      hence thesis by A1, Lm1;

    end;

    definition

      let n, D;

      let p be Element of ((n + 1) -tuples_on D);

      let m;

      :: original: .

      redefine

      func p . m -> Element of D ;

      coherence

      proof

        reconsider S = ( Seg (n + 1)) as non empty set by FINSEQ_1: 4;

        m in S & ( len p) = (n + 1) by Th7, CARD_1:def 7;

        then m in ( dom p) by FINSEQ_1:def 3;

        then ( rng p) c= D & (p . m) in ( rng p) by FINSEQ_1:def 4, FUNCT_1:def 3;

        hence thesis;

      end;

    end

    definition

      let n, RAS;

      :: MIDSP_3:def3

      attr RAS is being_invariance means for a, b, p, q st (for m holds (a @ (q . m)) = (b @ (p . m))) holds (a @ ( *' (b,q))) = (b @ ( *' (a,p)));

    end

    definition

      let n, RAS, p, i, a;

      :: original: +*

      redefine

      func p +* (i,a) -> Tuple of (n + 1), RAS ;

      coherence

      proof

        thus (p +* (i,a)) is Tuple of (n + 1), RAS;

      end;

    end

    definition

      let n, i, RAS;

      :: MIDSP_3:def4

      pred RAS has_property_of_zero_in i means for a, p holds ( *' (a,(p +* (i,a)))) = a;

    end

    definition

      let n, i, RAS;

      :: MIDSP_3:def5

      pred RAS is_semi_additive_in i means for a, pii, p st (p . i) = pii holds ( *' (a,(p +* (i,(a @ pii))))) = (a @ ( *' (a,p)));

    end

    theorem :: MIDSP_3:11

    

     Th11: RAS is_semi_additive_in m implies for a, d, p, q st q = (p +* (m,d)) holds ( *' (a,(p +* (m,(a @ d))))) = (a @ ( *' (a,q)))

    proof

      assume

       A1: RAS is_semi_additive_in m;

      let a, d, p, q;

      set qq = (q +* (m,(a @ d)));

      assume

       A2: q = (p +* (m,d));

      

       A3: qq = (p +* (m,(a @ d)))

      proof

        set pp = (p +* (m,(a @ d)));

        for k be Nat of n holds (qq . k) = (pp . k)

        proof

          let k be Nat of n;

          now

            per cases ;

              suppose

               A4: k = m;

              (pp . m) = (a @ d) by Th10;

              hence thesis by A4, Th10;

            end;

              suppose

               A5: k <> m;

              

              hence (qq . k) = (q . k) by FUNCT_7: 32

              .= (p . k) by A2, A5, FUNCT_7: 32

              .= (pp . k) by A5, FUNCT_7: 32;

            end;

          end;

          hence thesis;

        end;

        hence thesis by Th9;

      end;

      (q . m) = d by A2, Th10;

      hence thesis by A1, A3;

    end;

    definition

      let n, i, RAS;

      :: MIDSP_3:def6

      pred RAS is_additive_in i means for a, pii, p9i, p st (p . i) = pii holds ( *' (a,(p +* (i,(pii @ p9i))))) = (( *' (a,p)) @ ( *' (a,(p +* (i,p9i)))));

    end

    definition

      let n, i, RAS;

      :: MIDSP_3:def7

      pred RAS is_alternative_in i means for a, p, pii st (p . i) = pii holds ( *' (a,(p +* ((i + 1),pii)))) = a;

    end

    reserve W for ATLAS of RAS;

    reserve v for Vector of W;

    definition

      let n, RAS, W, i;

      mode Tuple of i,W is Element of (i -tuples_on the carrier of the algebra of W);

    end

    reserve x,y for Tuple of (n + 1), W;

    theorem :: MIDSP_3:12

    i in ( Seg (n + 1)) implies ((x +* (i,v)) . i) = v & for l st l in (( dom x) \ {i}) holds ((x +* (i,v)) . l) = (x . l) by Lm1, Lm2;

    theorem :: MIDSP_3:13

    

     Th13: (for l be Nat of n st l = i holds ((x +* (i,v)) . l) = v) & for l,i be Nat of n st l <> i holds ((x +* (i,v)) . l) = (x . l)

    proof

      thus for l be Nat of n st l = i holds ((x +* (i,v)) . l) = v

      proof

        let l be Nat of n such that

         A1: l = i;

        l in ( Seg (n + 1)) by Th7;

        hence thesis by A1, Lm1;

      end;

      thus thesis by FUNCT_7: 32;

    end;

    theorem :: MIDSP_3:14

    

     Th14: (for m holds (x . m) = (y . m)) implies x = y

    proof

      assume

       A1: for m holds (x . m) = (y . m);

      for j be Nat st j in ( Seg (n + 1)) holds (x . j) = (y . j)

      proof

        let j be Nat;

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

        then

        reconsider j as Nat of n by Th7;

        (x . j) = (y . j) by A1;

        hence thesis;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    scheme :: MIDSP_3:sch1

    SeqLambdaD9 { n() -> Nat , D() -> non empty set , F( set) -> Element of D() } :

ex z be FinSequence of D() st ( len z) = (n() + 1) & for j be Nat of n() holds (z . j) = F(j);

      reconsider S = ( Seg (n() + 1)) as non empty set by FINSEQ_1: 4;

      consider z be FinSequence of D() such that

       A1: ( len z) = (n() + 1) and

       A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

      take z;

      

       A3: ( dom z) = ( Seg (n() + 1)) by A1, FINSEQ_1:def 3;

      for j be Nat of n() holds (z . j) = F(j) by Th7, A2, A3;

      hence thesis by A1;

    end;

    definition

      let n, RAS, W, a, x;

      :: MIDSP_3:def8

      func (a,x) . W -> Tuple of (n + 1), RAS means

      : Def8: (it . m) = ((a,(x . m)) . W);

      existence

      proof

        deffunc F( Nat of n) = ((a,(x . $1)) . W);

        consider z be FinSequence of the carrier of RAS such that

         A1: ( len z) = (n + 1) and

         A2: (z . m) = F(m) from SeqLambdaD9;

        reconsider z as Tuple of (n + 1), RAS by A1, FINSEQ_2: 92;

        take z;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let p, q such that

         A3: for m holds (p . m) = ((a,(x . m)) . W) and

         A4: for m holds (q . m) = ((a,(x . m)) . W);

        for m holds (p . m) = (q . m)

        proof

          let m;

          (p . m) = ((a,(x . m)) . W) by A3;

          hence thesis by A4;

        end;

        hence thesis by Th9;

      end;

    end

    definition

      let n, RAS, W, a, p;

      :: MIDSP_3:def9

      func W . (a,p) -> Tuple of (n + 1), W means

      : Def9: (it . m) = (W . (a,(p . m)));

      existence

      proof

        deffunc F( Nat of n) = (W . (a,(p . $1)));

        consider z be FinSequence of the carrier of the algebra of W such that

         A1: ( len z) = (n + 1) and

         A2: (z . m) = F(m) from SeqLambdaD9;

        reconsider z as Tuple of (n + 1), W by A1, FINSEQ_2: 92;

        take z;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let x, y such that

         A3: for m holds (x . m) = (W . (a,(p . m))) and

         A4: for m holds (y . m) = (W . (a,(p . m)));

        for m holds (x . m) = (y . m)

        proof

          let m;

          (W . (a,(p . m))) = (x . m) by A3;

          hence thesis by A4;

        end;

        hence thesis by Th14;

      end;

    end

    theorem :: MIDSP_3:15

    

     Th15: (W . (a,p)) = x iff ((a,x) . W) = p

    proof

      thus (W . (a,p)) = x implies ((a,x) . W) = p

      proof

        assume

         A1: (W . (a,p)) = x;

        now

          let m;

          (W . (a,(p . m))) = (x . m) by A1, Def9;

          hence ((a,(x . m)) . W) = (p . m) by MIDSP_2: 33;

        end;

        hence thesis by Def8;

      end;

      thus ((a,x) . W) = p implies (W . (a,p)) = x

      proof

        assume

         A2: ((a,x) . W) = p;

        now

          let m;

          ((a,(x . m)) . W) = (p . m) by A2, Def8;

          hence (W . (a,(p . m))) = (x . m) by MIDSP_2: 33;

        end;

        hence thesis by Def9;

      end;

    end;

    theorem :: MIDSP_3:16

    (W . (a,((a,x) . W))) = x by Th15;

    theorem :: MIDSP_3:17

    ((a,(W . (a,p))) . W) = p by Th15;

    definition

      let n, RAS, W, a, x;

      :: MIDSP_3:def10

      func Phi (a,x) -> Vector of W equals (W . (a,( *' (a,((a,x) . W)))));

      coherence ;

    end

    theorem :: MIDSP_3:18

    

     Th18: (W . (a,p)) = x & (W . (a,b)) = v implies (( *' (a,p)) = b iff ( Phi (a,x)) = v)

    proof

      assume that

       A1: (W . (a,p)) = x and

       A2: (W . (a,b)) = v;

      ( Phi (a,x)) = (W . (a,( *' (a,p)))) by A1, Th15;

      hence thesis by A2, MIDSP_2: 32;

    end;

    theorem :: MIDSP_3:19

    

     Th19: RAS is being_invariance iff for a, b, x holds ( Phi (a,x)) = ( Phi (b,x))

    proof

      

       A1: (for a, b, x holds ( Phi (a,x)) = ( Phi (b,x))) implies RAS is being_invariance

      proof

        assume

         A2: for a, b, x holds ( Phi (a,x)) = ( Phi (b,x));

        let a, b, p, q;

        

         A3: (W . (a,( *' (a,((a,(W . (a,p))) . W))))) = ( Phi (a,(W . (a,p))))

        .= ( Phi (b,(W . (a,p)))) by A2

        .= (W . (b,( *' (b,((b,(W . (a,p))) . W)))));

        assume

         A4: for m holds (a @ (q . m)) = (b @ (p . m));

         A5:

        now

          let m;

          (a @ (q . m)) = (b @ (p . m)) by A4;

          then

           A6: (W . (a,(p . m))) = (W . (b,(q . m))) by MIDSP_2: 33;

          

          thus ((W . (a,p)) . m) = (W . (a,(p . m))) by Def9

          .= ((W . (b,q)) . m) by A6, Def9;

        end;

        (W . (a,( *' (a,p)))) = (W . (a,( *' (a,((a,(W . (a,p))) . W))))) by Th15

        .= (W . (b,( *' (b,((b,(W . (b,q))) . W))))) by A5, A3, Th14

        .= (W . (b,( *' (b,q)))) by Th15;

        hence thesis by MIDSP_2: 33;

      end;

      now

        assume

         A7: RAS is being_invariance;

        let a, b, x;

        set p = ((a,x) . W), q = ((b,x) . W);

        

         A8: (W . (a,p)) = x by Th15

        .= (W . (b,q)) by Th15;

        now

          let m;

          (W . (a,(p . m))) = ((W . (a,p)) . m) by Def9

          .= (W . (b,(q . m))) by A8, Def9;

          hence (a @ (q . m)) = (b @ (p . m)) by MIDSP_2: 33;

        end;

        then (a @ ( *' (b,q))) = (b @ ( *' (a,p))) by A7;

        hence ( Phi (a,x)) = ( Phi (b,x)) by MIDSP_2: 33;

      end;

      hence thesis by A1;

    end;

    theorem :: MIDSP_3:20

    

     Th20: 1 in ( Seg (n + 1))

    proof

       0 <= n by NAT_1: 2;

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

      hence thesis by FINSEQ_1: 1;

    end;

    theorem :: MIDSP_3:21

    

     Th21: 1 is Nat of n

    proof

      1 in ( Seg (n + 1)) by Th20;

      hence thesis by Th7;

    end;

    begin

    definition

      let n;

      :: MIDSP_3:def11

      mode ReperAlgebra of n -> MidSp-like non empty ReperAlgebraStr over (n + 2) means

      : Def11: it is being_invariance;

      existence

      proof

        reconsider one1 = 1 as Nat of (n + 1) by Th21;

        set M = the MidSp;

        set D = the carrier of M, k = ((n + 1) + 1);

        set C = (k -tuples_on D);

        deffunc F( Element of C) = ($1 . one1);

        consider R be Function of C, D such that

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

        reconsider R as Function of ((n + 2) -tuples_on D), D;

        reconsider RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #) as MidSp-like non empty ReperAlgebraStr over (n + 2) by Lm3;

        take RA;

        for a,b be Point of RA, p,q be Tuple of (n + 1), RA st for m holds (a @ (q . m)) = (b @ (p . m)) holds (a @ ( *' (b,q))) = (b @ ( *' (a,p)))

        proof

          let a,b be Point of RA, p,q be Tuple of (n + 1), RA such that for m holds (a @ (q . m)) = (b @ (p . m));

          

           A2: ( *' (a,p)) = (( <*a*> ^ p) . one1) by A1

          .= a by FINSEQ_1: 41;

          ( *' (b,q)) = (( <*b*> ^ q) . one1) by A1

          .= b by FINSEQ_1: 41;

          hence thesis by A2;

        end;

        hence thesis;

      end;

    end

    reserve RAS for ReperAlgebra of n;

    reserve a,b,pm,p9m,p99m for Point of RAS;

    reserve p for Tuple of (n + 1), RAS;

    reserve W for ATLAS of RAS;

    reserve v for Vector of W;

    reserve x for Tuple of (n + 1), W;

    theorem :: MIDSP_3:22

    

     Th22: ( Phi (a,x)) = ( Phi (b,x)) by Def11, Th19;

    definition

      let n, RAS, W, x;

      :: MIDSP_3:def12

      func Phi (x) -> Vector of W means

      : Def12: for a holds it = ( Phi (a,x));

      existence

      proof

        set a = the Point of RAS;

        take ( Phi (a,x));

        thus thesis by Th22;

      end;

      uniqueness

      proof

        set a = the Point of RAS;

        let y,z be Vector of W such that

         A1: for a holds y = ( Phi (a,x)) and

         A2: for a holds z = ( Phi (a,x));

        y = ( Phi (a,x)) by A1;

        hence thesis by A2;

      end;

    end

    

     Lm4: (W . (a,p)) = x implies ( Phi x) = (W . (a,( *' (a,p))))

    proof

      assume

       A1: (W . (a,p)) = x;

      

      thus ( Phi x) = ( Phi (a,x)) by Def12

      .= (W . (a,( *' (a,p)))) by A1, Th15;

    end;

    

     Lm5: ((a,x) . W) = p implies ( Phi x) = (W . (a,( *' (a,p))))

    proof

      assume ((a,x) . W) = p;

      then (W . (a,p)) = x by Th15;

      hence thesis by Lm4;

    end;

    theorem :: MIDSP_3:23

    

     Th23: (W . (a,p)) = x & (W . (a,b)) = v & ( Phi x) = v implies ( *' (a,p)) = b

    proof

      assume

       A1: (W . (a,p)) = x & (W . (a,b)) = v & ( Phi x) = v;

      ( Phi x) = ( Phi (a,x)) by Def12;

      hence thesis by A1, Th18;

    end;

    theorem :: MIDSP_3:24

    

     Th24: ((a,x) . W) = p & ((a,v) . W) = b & ( *' (a,p)) = b implies ( Phi x) = v

    proof

      assume ((a,x) . W) = p & ((a,v) . W) = b & ( *' (a,p)) = b;

      then ( Phi (a,x)) = v by MIDSP_2: 33;

      hence thesis by Def12;

    end;

    theorem :: MIDSP_3:25

    

     Th25: (W . (a,p)) = x & (W . (a,b)) = v implies (W . (a,(p +* (m,b)))) = (x +* (m,v))

    proof

      assume that

       A1: (W . (a,p)) = x and

       A2: (W . (a,b)) = v;

      set q = (p +* (m,b));

      set y = (W . (a,q)), z = (x +* (m,v));

      for k be Nat of n holds (y . k) = (z . k)

      proof

        let k be Nat of n;

        now

          per cases ;

            suppose

             A3: k = m;

            

            thus (y . k) = (W . (a,(q . k))) by Def9

            .= (W . (a,b)) by A3, Th10

            .= (z . k) by A2, A3, Th13;

          end;

            suppose

             A4: k <> m;

            

            thus (y . k) = (W . (a,(q . k))) by Def9

            .= (W . (a,(p . k))) by A4, FUNCT_7: 32

            .= (x . k) by A1, Def9

            .= (z . k) by A4, FUNCT_7: 32;

          end;

        end;

        hence thesis;

      end;

      hence thesis by Th14;

    end;

    theorem :: MIDSP_3:26

    

     Th26: ((a,x) . W) = p & ((a,v) . W) = b implies ((a,(x +* (m,v))) . W) = (p +* (m,b))

    proof

      assume ((a,x) . W) = p & ((a,v) . W) = b;

      then (W . (a,p)) = x & (W . (a,b)) = v by Th15, MIDSP_2: 33;

      then (W . (a,(p +* (m,b)))) = (x +* (m,v)) by Th25;

      hence thesis by Th15;

    end;

    theorem :: MIDSP_3:27

    RAS has_property_of_zero_in m iff for x holds ( Phi (x +* (m,( 0. W)))) = ( 0. W)

    proof

      thus RAS has_property_of_zero_in m implies for x holds ( Phi (x +* (m,( 0. W)))) = ( 0. W)

      proof

        set a = the Point of RAS;

        assume

         A1: RAS has_property_of_zero_in m;

        set b = ((a,( 0. W)) . W);

        let x;

        set p9 = (((a,x) . W) +* (m,a));

        

         A2: b = a by MIDSP_2: 34;

        then

         A3: ((a,(x +* (m,( 0. W)))) . W) = p9 by Th26;

        ( *' (a,p9)) = b by A1, A2;

        hence thesis by A3, Th24;

      end;

      thus (for x holds ( Phi (x +* (m,( 0. W)))) = ( 0. W)) implies RAS has_property_of_zero_in m

      proof

        assume

         A4: for x holds ( Phi (x +* (m,( 0. W)))) = ( 0. W);

        for a, p holds ( *' (a,(p +* (m,a)))) = a

        proof

          let a, p;

          set v = (W . (a,a));

          set x9 = ((W . (a,p)) +* (m,( 0. W)));

          v = ( 0. W) by MIDSP_2: 33;

          then (W . (a,(p +* (m,a)))) = x9 & ( Phi x9) = v by A4, Th25;

          hence thesis by Th23;

        end;

        hence thesis;

      end;

    end;

    theorem :: MIDSP_3:28

    

     Th28: RAS is_semi_additive_in m iff for x holds ( Phi (x +* (m,( Double (x . m))))) = ( Double ( Phi x))

    proof

      thus RAS is_semi_additive_in m implies for x holds ( Phi (x +* (m,( Double (x . m))))) = ( Double ( Phi x))

      proof

        set a = the Point of RAS;

        assume

         A1: RAS is_semi_additive_in m;

        let x;

        set x9 = (x +* (m,( Double (x . m))));

        set p = ((a,x) . W), p9 = ((a,x9) . W);

        set q = (p9 +* (m,(a @ (p9 . m))));

        for i be Nat of n holds (p . i) = (q . i)

        proof

          let i be Nat of n;

          now

            per cases ;

              suppose

               A2: i = m;

              (W . (a,p)) = x by Th15;

              then

               A3: (W . (a,(p . m))) = (x . m) by Def9;

              (W . (a,p9)) = x9 by Th15;

              then

               A4: (W . (a,(p9 . m))) = (x9 . m) by Def9;

              (x9 . m) = ( Double (x . m)) by Th13;

              

              then (p . m) = (a @ (p9 . m)) by A3, A4, MIDSP_2: 31

              .= (q . m) by Th10;

              hence thesis by A2;

            end;

              suppose

               A5: i <> m;

              

              thus (p . i) = ((a,(x . i)) . W) by Def8

              .= ((a,(x9 . i)) . W) by A5, FUNCT_7: 32

              .= (p9 . i) by Def8

              .= (q . i) by A5, FUNCT_7: 32;

            end;

          end;

          hence thesis;

        end;

        then p = q by Th9;

        then ( *' (a,p)) = (a @ ( *' (a,p9))) by A1;

        then

         A6: (W . (a,( *' (a,p9)))) = ( Double (W . (a,( *' (a,p))))) by MIDSP_2: 31;

        ( Phi x9) = (W . (a,( *' (a,p9)))) by Lm5;

        hence thesis by A6, Lm5;

      end;

      thus (for x holds ( Phi (x +* (m,( Double (x . m))))) = ( Double ( Phi x))) implies RAS is_semi_additive_in m

      proof

        assume

         A7: for x holds ( Phi (x +* (m,( Double (x . m))))) = ( Double ( Phi x));

        let a;

        let p9m be Point of RAS, p9 be Tuple of (n + 1), RAS such that

         A8: (p9 . m) = p9m;

        set p = (p9 +* (m,(a @ (p9 . m))));

        set x = (W . (a,p));

        set x9 = (x +* (m,( Double (x . m))));

        (W . (a,p9)) = x9

        proof

          set y = (W . (a,p9));

          for i be Nat of n holds (x9 . i) = (y . i)

          proof

            let i be Nat of n;

            now

              per cases ;

                suppose

                 A9: i = m;

                

                 A10: (W . (a,(p . m))) = (x . m) & (p . m) = (a @ (p9 . m)) by Def9, Th10;

                (x9 . m) = ( Double (x . m)) & (W . (a,(p9 . m))) = (y . m) by Def9, Th13;

                hence thesis by A9, A10, MIDSP_2: 31;

              end;

                suppose

                 A11: i <> m;

                

                hence (x9 . i) = (x . i) by FUNCT_7: 32

                .= (W . (a,(p . i))) by Def9

                .= (W . (a,(p9 . i))) by A11, FUNCT_7: 32

                .= (y . i) by Def9;

              end;

            end;

            hence thesis;

          end;

          hence thesis by Th14;

        end;

        then

         A12: ( Phi x9) = (W . (a,( *' (a,p9)))) by Lm4;

        ( Phi x) = (W . (a,( *' (a,p)))) by Lm4;

        then (W . (a,( *' (a,p9)))) = ( Double (W . (a,( *' (a,p))))) by A7, A12;

        hence thesis by A8, MIDSP_2: 31;

      end;

    end;

    theorem :: MIDSP_3:29

    

     Th29: RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS is_semi_additive_in m

    proof

      assume that

       A1: RAS has_property_of_zero_in m and

       A2: RAS is_additive_in m;

      let a, pm, p;

      assume (p . m) = pm;

      

      then ( *' (a,(p +* (m,(a @ pm))))) = (( *' (a,p)) @ ( *' (a,(p +* (m,a))))) by A2

      .= (a @ ( *' (a,p))) by A1;

      hence thesis;

    end;

    

     Lm6: RAS is_semi_additive_in m implies for a, p9m, p99m, p st (a @ p99m) = ((p . m) @ p9m) holds ( *' (a,(p +* (m,((p . m) @ p9m))))) = (( *' (a,p)) @ ( *' (a,(p +* (m,p9m))))) iff (W . (a,( *' (a,(p +* (m,p99m)))))) = ((W . (a,( *' (a,p)))) + (W . (a,( *' (a,(p +* (m,p9m)))))))

    proof

      assume

       A1: RAS is_semi_additive_in m;

      let a, p9m, p99m, p;

      assume (a @ p99m) = ((p . m) @ p9m);

      then ( *' (a,(p +* (m,((p . m) @ p9m))))) = (a @ ( *' (a,(p +* (m,p99m))))) by A1, Th11;

      hence thesis by MIDSP_2: 30;

    end;

    

     Lm7: (for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v))))) implies RAS is_semi_additive_in m

    proof

      assume

       A1: for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v))));

      for x holds ( Phi (x +* (m,( Double (x . m))))) = ( Double ( Phi x))

      proof

        let x;

        set v = (x . m);

        set y = (x +* (m,v));

        for k be Nat of n holds (y . k) = (x . k)

        proof

          let k be Nat of n;

          now

            per cases ;

              suppose k = m;

              hence thesis by Th13;

            end;

              suppose k <> m;

              hence thesis by FUNCT_7: 32;

            end;

          end;

          hence thesis;

        end;

        then

         A2: y = x by Th14;

        

        thus ( Phi (x +* (m,( Double v)))) = ( Phi (x +* (m,(v + v)))) by MIDSP_2:def 1

        .= (( Phi x) + ( Phi (x +* (m,v)))) by A1

        .= ( Double ( Phi x)) by A2, MIDSP_2:def 1;

      end;

      hence thesis by Th28;

    end;

    theorem :: MIDSP_3:30

    RAS has_property_of_zero_in m implies (RAS is_additive_in m iff for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v)))))

    proof

      assume

       A1: RAS has_property_of_zero_in m;

      thus RAS is_additive_in m implies for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v))))

      proof

        set a = the Point of RAS;

        assume

         A2: RAS is_additive_in m;

        let x, v;

        set p = ((a,x) . W), p9m = ((a,v) . W);

        consider p99m such that

         A3: (p99m @ a) = ((p . m) @ p9m) by MIDSP_1:def 3;

        

         A4: (W . (a,p)) = x & (W . (a,p9m)) = v by Th15, MIDSP_2: 33;

        

         A5: (W . (a,p99m)) = ((W . (a,(p . m))) + (W . (a,p9m))) by A3, MIDSP_2: 30

        .= ((x . m) + v) by A4, Def9;

        (p +* (m,p99m)) = ((a,(x +* (m,((x . m) + v)))) . W)

        proof

          set pp = (p +* (m,p99m)), xx = (x +* (m,((x . m) + v)));

          set qq = ((a,xx) . W);

          for i be Nat of n holds (pp . i) = (qq . i)

          proof

            let i be Nat of n;

            per cases ;

              suppose

               A6: i = m;

              

              hence (pp . i) = p99m by Th10

              .= ((a,((x . m) + v)) . W) by A5, MIDSP_2: 33

              .= ((a,(xx . m)) . W) by Th13

              .= (qq . i) by A6, Def8;

            end;

              suppose

               A7: i <> m;

              

              hence (pp . i) = (p . i) by FUNCT_7: 32

              .= ((a,(x . i)) . W) by Def8

              .= ((a,(xx . i)) . W) by A7, FUNCT_7: 32

              .= (qq . i) by Def8;

            end;

          end;

          hence thesis by Th9;

        end;

        then

         A8: ( Phi (x +* (m,((x . m) + v)))) = (W . (a,( *' (a,(p +* (m,p99m)))))) by Lm5;

        

         A9: (p +* (m,p9m)) = ((a,(x +* (m,v))) . W)

        proof

          set pp = (p +* (m,p9m)), qq = ((a,(x +* (m,v))) . W);

          for i be Nat of n holds (pp . i) = (qq . i)

          proof

            let i be Nat of n;

            per cases ;

              suppose

               A10: i = m;

              

              hence (pp . i) = p9m by Th10

              .= ((a,((x +* (m,v)) . m)) . W) by Th13

              .= (qq . i) by A10, Def8;

            end;

              suppose

               A11: i <> m;

              

              hence (pp . i) = (p . i) by FUNCT_7: 32

              .= ((a,(x . i)) . W) by Def8

              .= ((a,((x +* (m,v)) . i)) . W) by A11, FUNCT_7: 32

              .= (qq . i) by Def8;

            end;

          end;

          hence thesis by Th9;

        end;

        RAS is_semi_additive_in m & ( *' (a,(p +* (m,((p . m) @ p9m))))) = (( *' (a,p)) @ ( *' (a,(p +* (m,p9m))))) by A1, A2, Th29;

        then

         A12: (W . (a,( *' (a,(p +* (m,p99m)))))) = ((W . (a,( *' (a,p)))) + (W . (a,( *' (a,(p +* (m,p9m))))))) by A3, Lm6;

        ( Phi x) = (W . (a,( *' (a,p)))) by Lm5;

        hence thesis by A12, A8, A9, Lm5;

      end;

      thus (for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v))))) implies RAS is_additive_in m

      proof

        assume

         A13: for x, v holds ( Phi (x +* (m,((x . m) + v)))) = (( Phi x) + ( Phi (x +* (m,v))));

        then

         A14: RAS is_semi_additive_in m by Lm7;

        for a, pm, p9m, p st (p . m) = pm holds ( *' (a,(p +* (m,(pm @ p9m))))) = (( *' (a,p)) @ ( *' (a,(p +* (m,p9m)))))

        proof

          let a, pm, p9m, p such that

           A15: (p . m) = pm;

          set x = (W . (a,p)), v = (W . (a,p9m));

          consider p99m such that

           A16: (p99m @ a) = ((p . m) @ p9m) by MIDSP_1:def 3;

          

           A17: ((a,x) . W) = p by Th15;

          

           A18: (W . (a,p99m)) = ((W . (a,(p . m))) + (W . (a,p9m))) by A16, MIDSP_2: 30

          .= ((x . m) + v) by Def9;

          (p +* (m,p99m)) = ((a,(x +* (m,((x . m) + v)))) . W)

          proof

            set pp = (p +* (m,p99m)), xx = (x +* (m,((x . m) + v)));

            set qq = ((a,xx) . W);

            for i be Nat of n holds (pp . i) = (qq . i)

            proof

              let i be Nat of n;

              per cases ;

                suppose

                 A19: i = m;

                

                hence (pp . i) = p99m by Th10

                .= ((a,((x . m) + v)) . W) by A18, MIDSP_2: 33

                .= ((a,(xx . m)) . W) by Th13

                .= (qq . i) by A19, Def8;

              end;

                suppose

                 A20: i <> m;

                

                hence (pp . i) = (p . i) by FUNCT_7: 32

                .= ((a,(x . i)) . W) by A17, Def8

                .= ((a,(xx . i)) . W) by A20, FUNCT_7: 32

                .= (qq . i) by Def8;

              end;

            end;

            hence thesis by Th9;

          end;

          then

           A21: ( Phi (x +* (m,((x . m) + v)))) = (W . (a,( *' (a,(p +* (m,p99m)))))) by Lm5;

          

           A22: ((a,v) . W) = p9m by MIDSP_2: 33;

          (p +* (m,p9m)) = ((a,(x +* (m,v))) . W)

          proof

            set pp = (p +* (m,p9m)), qq = ((a,(x +* (m,v))) . W);

            for i be Nat of n holds (pp . i) = (qq . i)

            proof

              let i be Nat of n;

              per cases ;

                suppose

                 A23: i = m;

                

                hence (pp . i) = p9m by Th10

                .= ((a,((x +* (m,v)) . m)) . W) by A22, Th13

                .= (qq . i) by A23, Def8;

              end;

                suppose

                 A24: i <> m;

                

                hence (pp . i) = (p . i) by FUNCT_7: 32

                .= ((a,(x . i)) . W) by A17, Def8

                .= ((a,((x +* (m,v)) . i)) . W) by A24, FUNCT_7: 32

                .= (qq . i) by Def8;

              end;

            end;

            hence thesis by Th9;

          end;

          then

           A25: ( Phi (x +* (m,v))) = (W . (a,( *' (a,(p +* (m,p9m)))))) by Lm5;

          ( Phi x) = (W . (a,( *' (a,p)))) by Lm4;

          then (W . (a,( *' (a,(p +* (m,p99m)))))) = ((W . (a,( *' (a,p)))) + (W . (a,( *' (a,(p +* (m,p9m))))))) by A13, A21, A25;

          hence thesis by A14, A15, A16, Lm6;

        end;

        hence thesis;

      end;

    end;

    theorem :: MIDSP_3:31

    

     Th31: (W . (a,p)) = x & m <= n implies (W . (a,(p +* ((m + 1),(p . m))))) = (x +* ((m + 1),(x . m)))

    proof

      assume that

       A1: (W . (a,p)) = x and

       A2: m <= n;

      reconsider m9 = (m + 1) as Nat of n by A2, Th8;

      set y = (W . (a,(p +* (m9,(p . m))))), z = (x +* (m9,(x . m)));

      for k be Nat of n holds (y . k) = (z . k)

      proof

        let k be Nat of n;

        now

          per cases ;

            suppose

             A3: k = m9;

            

            thus (y . k) = (W . (a,((p +* (m9,(p . m))) . k))) by Def9

            .= (W . (a,(p . m))) by A3, Th10

            .= (x . m) by A1, Def9

            .= (z . k) by A3, Th13;

          end;

            suppose

             A4: k <> m9;

            

            thus (y . k) = (W . (a,((p +* (m9,(p . m))) . k))) by Def9

            .= (W . (a,(p . k))) by A4, FUNCT_7: 32

            .= (x . k) by A1, Def9

            .= (z . k) by A4, FUNCT_7: 32;

          end;

        end;

        hence thesis;

      end;

      hence thesis by Th14;

    end;

    theorem :: MIDSP_3:32

    

     Th32: ((a,x) . W) = p & m <= n implies ((a,(x +* ((m + 1),(x . m)))) . W) = (p +* ((m + 1),(p . m)))

    proof

      assume that

       A1: ((a,x) . W) = p and

       A2: m <= n;

      (W . (a,p)) = x by A1, Th15;

      then (W . (a,(p +* ((m + 1),(p . m))))) = (x +* ((m + 1),(x . m))) by A2, Th31;

      hence thesis by Th15;

    end;

    theorem :: MIDSP_3:33

    m <= n implies (RAS is_alternative_in m iff for x holds ( Phi (x +* ((m + 1),(x . m)))) = ( 0. W))

    proof

      assume

       A1: m <= n;

      thus RAS is_alternative_in m implies for x holds ( Phi (x +* ((m + 1),(x . m)))) = ( 0. W)

      proof

        set a = the Point of RAS;

        assume

         A2: RAS is_alternative_in m;

        let x;

        set p = ((a,x) . W), b = ((a,( 0. W)) . W);

        set p9 = (p +* ((m + 1),(p . m)));

        b = a by MIDSP_2: 34;

        then

         A3: ( *' (a,p9)) = b by A2;

        ((a,(x +* ((m + 1),(x . m)))) . W) = p9 by A1, Th32;

        hence thesis by A3, Th24;

      end;

      assume

       A4: for x holds ( Phi (x +* ((m + 1),(x . m)))) = ( 0. W);

      for a, p, pm st (p . m) = pm holds ( *' (a,(p +* ((m + 1),pm)))) = a

      proof

        let a, p, pm such that

         A5: (p . m) = pm;

        set x = (W . (a,p)), v = (W . (a,a));

        set x9 = (x +* ((m + 1),(x . m)));

        v = ( 0. W) by MIDSP_2: 33;

        then

         A6: ( Phi x9) = v by A4;

        (W . (a,(p +* ((m + 1),(p . m))))) = x9 by A1, Th31;

        hence thesis by A5, A6, Th23;

      end;

      hence thesis;

    end;