midsp_1.miz



    begin

    definition

      struct ( 1-sorted) MidStr (# the carrier -> set,

the MIDPOINT -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for MidStr;

      existence

      proof

        set A = the non empty set, m = the BinOp of A;

        take MidStr (# A, m #);

        thus the carrier of MidStr (# A, m #) is non empty;

      end;

    end

    reserve MS for non empty MidStr;

    reserve a,b for Element of MS;

    definition

      let MS, a, b;

      :: MIDSP_1:def1

      func a @ b -> Element of MS equals (the MIDPOINT of MS . (a,b));

      coherence ;

    end

    definition

      :: MIDSP_1:def2

      func Example -> MidStr equals MidStr (# { 0 }, op2 #);

      correctness ;

    end

    registration

      cluster Example -> strict non empty;

      coherence ;

    end

    theorem :: MIDSP_1:1

    the carrier of Example = { {} };

    theorem :: MIDSP_1:2

    the MIDPOINT of Example = op2 ;

    theorem :: MIDSP_1:3

    for a,b be Element of Example holds (a @ b) = ( op2 . (a,b));

    theorem :: MIDSP_1:4

    

     Th4: for a,b,c,d be Element of Example holds (a @ a) = a & (a @ b) = (b @ a) & ((a @ b) @ (c @ d)) = ((a @ c) @ (b @ d)) & ex x be Element of Example st (x @ a) = b

    proof

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

      

      thus (a @ a) = {} by TARSKI:def 1

      .= a by TARSKI:def 1;

      

      thus (a @ b) = {} by TARSKI:def 1

      .= (b @ a) by TARSKI:def 1;

      

      thus ((a @ b) @ (c @ d)) = {} by TARSKI:def 1

      .= ((a @ c) @ (b @ d)) by TARSKI:def 1;

      take x = a;

      

      thus (x @ a) = {} by TARSKI:def 1

      .= b by TARSKI:def 1;

    end;

    definition

      let IT be non empty MidStr;

      :: MIDSP_1:def3

      attr IT is MidSp-like means

      : Def3: for a,b,c,d be Element of IT holds (a @ a) = a & (a @ b) = (b @ a) & ((a @ b) @ (c @ d)) = ((a @ c) @ (b @ d)) & ex x be Element of IT st (x @ a) = b;

    end

    registration

      cluster strict MidSp-like for non empty MidStr;

      existence by Def3, Th4;

    end

    definition

      mode MidSp is MidSp-like non empty MidStr;

    end

    definition

      let M be MidSp, a,b be Element of M;

      :: original: @

      redefine

      func a @ b;

      commutativity by Def3;

    end

    reserve M for MidSp;

    reserve a,b,c,d,a9,b9,c9,d9,x,y,x9 for Element of M;

    theorem :: MIDSP_1:5

    

     Th5: ((a @ b) @ c) = ((a @ c) @ (b @ c))

    proof

      ((a @ b) @ c) = ((a @ b) @ (c @ c)) by Def3

      .= ((a @ c) @ (b @ c)) by Def3;

      hence thesis;

    end;

    theorem :: MIDSP_1:6

    

     Th6: (a @ (b @ c)) = ((a @ b) @ (a @ c))

    proof

      (a @ (b @ c)) = ((a @ a) @ (b @ c)) by Def3

      .= ((a @ b) @ (a @ c)) by Def3;

      hence thesis;

    end;

    theorem :: MIDSP_1:7

    

     Th7: (a @ b) = a implies a = b

    proof

      assume

       A1: (a @ b) = a;

      consider x such that

       A2: (x @ a) = b by Def3;

      b = ((x @ a) @ b) by A2, Def3

      .= ((x @ b) @ a) by A1, Th5

      .= a by A1, A2, Th5;

      hence thesis;

    end;

    theorem :: MIDSP_1:8

    

     Th8: (x @ a) = (x9 @ a) implies x = x9

    proof

      assume

       A1: (x @ a) = (x9 @ a);

      consider y such that

       A2: (y @ a) = x by Def3;

      x = (x @ (y @ a)) by A2, Def3

      .= ((x @ y) @ (x9 @ a)) by A1, Th6

      .= (x @ (x @ x9)) by A2, Def3;

      then x = (x @ x9) by Th7;

      hence thesis by Th7;

    end;

    theorem :: MIDSP_1:9

    (a @ x) = (a @ x9) implies x = x9 by Th8;

    definition

      let M, a, b, c, d;

      :: MIDSP_1:def4

      pred a,b @@ c,d means (a @ d) = (b @ c);

    end

    theorem :: MIDSP_1:10

    (a,a) @@ (b,b);

    theorem :: MIDSP_1:11

    

     Th11: (a,b) @@ (c,d) implies (c,d) @@ (a,b);

    theorem :: MIDSP_1:12

    

     Th12: (a,a) @@ (b,c) implies b = c by Th8;

    theorem :: MIDSP_1:13

    

     Th13: (a,b) @@ (c,c) implies a = b by Th11, Th12;

    theorem :: MIDSP_1:14

    (a,b) @@ (a,b);

    theorem :: MIDSP_1:15

    

     Th15: ex d st (a,b) @@ (c,d)

    proof

      consider d such that

       A1: (d @ a) = (b @ c) by Def3;

      (a,b) @@ (c,d) by A1;

      hence thesis;

    end;

    theorem :: MIDSP_1:16

    

     Th16: (a,b) @@ (c,d) & (a,b) @@ (c,d9) implies d = d9 by Th8;

    theorem :: MIDSP_1:17

    

     Th17: (x,y) @@ (a,b) & (x,y) @@ (c,d) implies (a,b) @@ (c,d)

    proof

      assume

       A1: (x,y) @@ (a,b);

      assume

       A2: (x,y) @@ (c,d);

      ((y @ x) @ (a @ d)) = ((y @ a) @ (x @ d)) by Def3

      .= ((x @ b) @ (x @ d)) by A1

      .= ((x @ b) @ (y @ c)) by A2

      .= ((y @ x) @ (b @ c)) by Def3;

      hence (a @ d) = (b @ c) by Th8;

    end;

    theorem :: MIDSP_1:18

    

     Th18: (a,b) @@ (a9,b9) & (b,c) @@ (b9,c9) implies (a,c) @@ (a9,c9)

    proof

      assume

       A1: (a,b) @@ (a9,b9);

      assume

       A2: (b,c) @@ (b9,c9);

      ((b9 @ b) @ (a @ c9)) = ((a @ b9) @ (b @ c9)) by Def3

      .= ((b @ a9) @ (b @ c9)) by A1

      .= ((c @ b9) @ (b @ a9)) by A2

      .= ((b9 @ b) @ (c @ a9)) by Def3;

      hence (a @ c9) = (c @ a9) by Th8;

    end;

    reserve p,q,r,p9,q9 for Element of [:the carrier of M, the carrier of M:];

    definition

      let M, p, q;

      :: MIDSP_1:def5

      pred p ## q means ((p `1 ),(p `2 )) @@ ((q `1 ),(q `2 ));

      reflexivity ;

      symmetry ;

    end

    theorem :: MIDSP_1:19

    

     Th19: (a,b) @@ (c,d) implies [a, b] ## [c, d];

    theorem :: MIDSP_1:20

    

     Th20: [a, b] ## [c, d] implies (a,b) @@ (c,d);

    theorem :: MIDSP_1:21

    

     Th21: p ## q & p ## r implies q ## r by Th17;

    theorem :: MIDSP_1:22

    p ## r & q ## r implies p ## q by Th21;

    theorem :: MIDSP_1:23

    p ## q & q ## r implies p ## r by Th21;

    theorem :: MIDSP_1:24

    p ## q implies (r ## p iff r ## q) by Th21;

    theorem :: MIDSP_1:25

    

     Th25: for p holds { q : q ## p } is non empty Subset of [:the carrier of M, the carrier of M:]

    proof

      let p;

      set pp = { q : q ## p };

      

       A1: for x be object holds x in pp implies x in [:the carrier of M, the carrier of M:]

      proof

        let x be object;

        assume x in pp;

        then ex q st x = q & q ## p;

        hence thesis;

      end;

      p in pp;

      hence thesis by A1, TARSKI:def 3;

    end;

    definition

      let M, p;

      :: MIDSP_1:def6

      func p ~ -> Subset of [:the carrier of M, the carrier of M:] equals { q : q ## p };

      coherence by Th25;

    end

    registration

      let M, p;

      cluster (p ~ ) -> non empty;

      coherence by Th25;

    end

    theorem :: MIDSP_1:26

    

     Th26: for p holds r in (p ~ ) iff r ## p

    proof

      let p;

      thus r in (p ~ ) implies r ## p

      proof

        assume r in (p ~ );

        then ex q st r = q & q ## p;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: MIDSP_1:27

    

     Th27: p ## q implies (p ~ ) = (q ~ )

    proof

      assume

       A1: p ## q;

      for x be object holds x in (p ~ ) iff x in (q ~ )

      proof

        let x be object;

        thus x in (p ~ ) implies x in (q ~ )

        proof

          assume

           A2: x in (p ~ );

          then

          reconsider r = x as Element of [:the carrier of M, the carrier of M:];

          r ## p by A2, Th26;

          then r ## q by A1, Th21;

          hence thesis;

        end;

        thus x in (q ~ ) implies x in (p ~ )

        proof

          assume

           A3: x in (q ~ );

          then

          reconsider r = x as Element of [:the carrier of M, the carrier of M:];

          r ## q by A3, Th26;

          then r ## p by A1, Th21;

          hence thesis;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: MIDSP_1:28

    

     Th28: (p ~ ) = (q ~ ) implies p ## q

    proof

      p in (p ~ );

      hence thesis by Th26;

    end;

    theorem :: MIDSP_1:29

    

     Th29: ( [a, b] ~ ) = ( [c, d] ~ ) implies (a @ d) = (b @ c)

    proof

      assume ( [a, b] ~ ) = ( [c, d] ~ );

      then (a,b) @@ (c,d) by Th20, Th28;

      hence thesis;

    end;

    theorem :: MIDSP_1:30

    p in (p ~ );

    definition

      let M;

      :: MIDSP_1:def7

      mode Vector of M -> non empty Subset of [:the carrier of M, the carrier of M:] means

      : Def7: ex p st it = (p ~ );

      existence

      proof

        set p = the Element of [:the carrier of M, the carrier of M:];

        take (p ~ );

        thus thesis;

      end;

    end

    reserve u,v,w,u9,w9 for Vector of M;

    definition

      let M, p;

      :: original: ~

      redefine

      func p ~ -> Vector of M ;

      coherence by Def7;

    end

    theorem :: MIDSP_1:31

    

     Th31: ex u st for p holds p in u iff (p `1 ) = (p `2 )

    proof

      set a = the Element of M;

      take ( [a, a] ~ );

      let p;

      ((p `1 ),(p `2 )) @@ (a,a) iff p ## [a, a];

      hence thesis by Th13, Th26;

    end;

    definition

      let M;

      :: MIDSP_1:def8

      func ID (M) -> Vector of M equals { p : (p `1 ) = (p `2 ) };

      coherence

      proof

        consider u such that

         A1: for p holds p in u iff (p `1 ) = (p `2 ) by Th31;

        u = { p : (p `1 ) = (p `2 ) }

        proof

          for x be object holds x in u iff x in { p : (p `1 ) = (p `2 ) }

          proof

            let x be object;

            thus x in u implies x in { p : (p `1 ) = (p `2 ) }

            proof

              assume

               A2: x in u;

              then

              reconsider r = x as Element of [:the carrier of M, the carrier of M:];

              (r `1 ) = (r `2 ) by A1, A2;

              hence thesis;

            end;

            thus x in { p : (p `1 ) = (p `2 ) } implies x in u

            proof

              assume x in { p : (p `1 ) = (p `2 ) };

              then ex p st x = p & (p `1 ) = (p `2 );

              hence thesis by A1;

            end;

          end;

          hence thesis by TARSKI: 2;

        end;

        hence thesis;

      end;

    end

    theorem :: MIDSP_1:32

    

     Th32: ( ID M) = ( [b, b] ~ )

    proof

      p in ( ID M) iff p in ( [b, b] ~ )

      proof

        thus p in ( ID M) implies p in ( [b, b] ~ )

        proof

          assume p in ( ID M);

          then ex q st p = q & (q `1 ) = (q `2 );

          then

           A1: ((p `1 ),(p `2 )) @@ (b,b);

          p ## [b, b] by A1;

          hence thesis;

        end;

        thus p in ( [b, b] ~ ) implies p in ( ID M)

        proof

          assume p in ( [b, b] ~ );

          then

           A2: p ## [b, b] by Th26;

          ((p `1 ),(p `2 )) @@ (b,b) by A2;

          then (p `1 ) = (p `2 ) by Th11, Th12;

          hence thesis;

        end;

      end;

      then for p be object holds p in ( ID M) iff p in ( [b, b] ~ );

      hence thesis by TARSKI: 2;

    end;

    theorem :: MIDSP_1:33

    

     Th33: (ex p, q st u = (p ~ ) & v = (q ~ ) & (p `2 ) = (q `1 ) & w = ( [(p `1 ), (q `2 )] ~ )) & (ex p, q st u = (p ~ ) & v = (q ~ ) & (p `2 ) = (q `1 ) & w9 = ( [(p `1 ), (q `2 )] ~ )) implies w = w9

    proof

      given p, q such that

       A1: u = (p ~ ) and

       A2: v = (q ~ ) and

       A3: (p `2 ) = (q `1 ) and

       A4: w = ( [(p `1 ), (q `2 )] ~ );

      given p9, q9 such that

       A5: u = (p9 ~ ) and

       A6: v = (q9 ~ ) and

       A7: (p9 `2 ) = (q9 `1 ) and

       A8: w9 = ( [(p9 `1 ), (q9 `2 )] ~ );

      q ## q9 by A2, A6, Th28;

      then

       A9: ((q `1 ),(q `2 )) @@ ((q9 `1 ),(q9 `2 ));

      p ## p9 by A1, A5, Th28;

      then ((p `1 ),(p `2 )) @@ ((p9 `1 ),(p9 `2 ));

      then ((p `1 ),(q `2 )) @@ ((p9 `1 ),(q9 `2 )) by A3, A7, A9, Th18;

      hence thesis by A4, A8, Th19, Th27;

    end;

    definition

      let M, u, v;

      :: MIDSP_1:def9

      func u + v -> Vector of M means

      : Def9: ex p, q st u = (p ~ ) & v = (q ~ ) & (p `2 ) = (q `1 ) & it = ( [(p `1 ), (q `2 )] ~ );

      existence

      proof

        consider p such that

         A1: u = (p ~ ) by Def7;

        consider q such that

         A2: v = (q ~ ) by Def7;

        consider d such that

         A3: ((q `1 ),(q `2 )) @@ ((p `2 ),d) by Th15;

        take ( [(p `1 ), d] ~ ), p9 = p, q9 = [(p `2 ), d];

        thus u = (p9 ~ ) by A1;

        q ## q9 by A3;

        hence v = (q9 ~ ) by A2, Th27;

        thus (p9 `2 ) = (q9 `1 );

        thus thesis;

      end;

      uniqueness by Th33;

    end

    theorem :: MIDSP_1:34

    

     Th34: ex b st u = ( [a, b] ~ )

    proof

      consider p such that

       A1: u = (p ~ ) by Def7;

      consider b such that

       A2: ((p `1 ),(p `2 )) @@ (a,b) by Th15;

       [(p `1 ), (p `2 )] ## [a, b] by A2;

      then p ## [a, b];

      then (p ~ ) = ( [a, b] ~ ) by Th27;

      hence thesis by A1;

    end;

    definition

      let M, a, b;

      :: MIDSP_1:def10

      func vect (a,b) -> Vector of M equals ( [a, b] ~ );

      coherence ;

    end

    theorem :: MIDSP_1:35

    

     Th35: ex b st u = ( vect (a,b))

    proof

      consider b such that

       A1: u = ( [a, b] ~ ) by Th34;

      u = ( vect (a,b)) by A1;

      hence thesis;

    end;

    theorem :: MIDSP_1:36

     [a, b] ## [c, d] implies ( vect (a,b)) = ( vect (c,d)) by Th27;

    theorem :: MIDSP_1:37

    ( vect (a,b)) = ( vect (c,d)) implies (a @ d) = (b @ c) by Th29;

    theorem :: MIDSP_1:38

    ( ID M) = ( vect (b,b)) by Th32;

    theorem :: MIDSP_1:39

    ( vect (a,b)) = ( vect (a,c)) implies b = c

    proof

      assume ( vect (a,b)) = ( vect (a,c));

      then (a,b) @@ (a,b) & (a,b) @@ (a,c) by Th20, Th28;

      hence thesis by Th16;

    end;

    theorem :: MIDSP_1:40

    

     Th40: (( vect (a,b)) + ( vect (b,c))) = ( vect (a,c))

    proof

      set p = [a, b], q = [b, c];

      set u = (p ~ ), v = (q ~ );

      (p `2 ) = b

      .= (q `1 );

      then (q `2 ) = c & (u + v) = ( [(p `1 ), (q `2 )] ~ ) by Def9;

      hence thesis;

    end;

    theorem :: MIDSP_1:41

    

     Th41: [a, (a @ b)] ## [(a @ b), b]

    proof

      (a @ b) = ((a @ b) @ (a @ b)) by Def3;

      then (a,(a @ b)) @@ ((a @ b),b);

      hence thesis;

    end;

    theorem :: MIDSP_1:42

    (( vect (a,(a @ b))) + ( vect (a,(a @ b)))) = ( vect (a,b))

    proof

      (( vect (a,(a @ b))) + ( vect (a,(a @ b)))) = (( vect (a,(a @ b))) + ( vect ((a @ b),b))) by Th27, Th41

      .= ( vect (a,b)) by Th40;

      hence thesis;

    end;

    theorem :: MIDSP_1:43

    

     Th43: ((u + v) + w) = (u + (v + w))

    proof

      set a = the Element of M;

      consider b such that

       A1: u = ( vect (a,b)) by Th35;

      consider c such that

       A2: v = ( vect (b,c)) by Th35;

      consider d such that

       A3: w = ( vect (c,d)) by Th35;

      ((u + v) + w) = (( vect (a,c)) + w) by A1, A2, Th40

      .= ( vect (a,d)) by A3, Th40

      .= (( vect (a,b)) + ( vect (b,d))) by Th40

      .= (u + (v + w)) by A1, A2, A3, Th40;

      hence thesis;

    end;

    theorem :: MIDSP_1:44

    

     Th44: (u + ( ID M)) = u

    proof

      set a = the Element of M;

      consider b such that

       A1: u = ( vect (a,b)) by Th35;

      (u + ( ID M)) = (( vect (a,b)) + ( vect (b,b))) by A1, Th32

      .= u by A1, Th40;

      hence thesis;

    end;

    theorem :: MIDSP_1:45

    

     Th45: ex v st (u + v) = ( ID M)

    proof

      set a = the Element of M;

      consider b such that

       A1: u = ( vect (a,b)) by Th35;

      (u + ( vect (b,a))) = ( vect (a,a)) by A1, Th40

      .= ( ID M) by Th32;

      hence thesis;

    end;

    theorem :: MIDSP_1:46

    

     Th46: (u + v) = (v + u)

    proof

      set a = the Element of M;

      consider b such that

       A1: u = ( vect (a,b)) by Th35;

      consider c such that

       A2: v = ( vect (b,c)) by Th35;

      consider d such that

       A3: v = ( vect (a,d)) by Th35;

      consider c9 such that

       A4: u = ( vect (d,c9)) by Th35;

      

       A5: (a @ c9) = (b @ d) by A1, A4, Th29

      .= (a @ c) by A2, A3, Th29;

      (u + v) = ( vect (a,c)) by A1, A2, Th40

      .= ( vect (a,c9)) by A5, Th8

      .= (v + u) by A3, A4, Th40;

      hence thesis;

    end;

    theorem :: MIDSP_1:47

    

     Th47: (u + v) = (u + w) implies v = w

    proof

      assume

       A1: (u + v) = (u + w);

      consider u9 such that

       A2: (u + u9) = ( ID M) by Th45;

      v = (v + ( ID M)) by Th44

      .= ((u + u9) + v) by A2, Th46

      .= ((u9 + u) + v) by Th46

      .= (u9 + (u + w)) by A1, Th43

      .= ((u9 + u) + w) by Th43

      .= (( ID M) + w) by A2, Th46

      .= (w + ( ID M)) by Th46;

      hence thesis by Th44;

    end;

    definition

      let M, u;

      :: MIDSP_1:def11

      func - u -> Vector of M means (u + it ) = ( ID M);

      existence by Th45;

      uniqueness by Th47;

    end

    reserve X for Subset of [:the carrier of M, the carrier of M:];

    definition

      let M;

      :: MIDSP_1:def12

      func setvect (M) -> set equals { X : X is Vector of M };

      coherence ;

    end

    reserve x for set;

    theorem :: MIDSP_1:48

    

     Th48: x is Vector of M iff x in ( setvect M)

    proof

      thus x is Vector of M implies x in ( setvect M);

      thus x in ( setvect M) implies x is Vector of M

      proof

        assume x in ( setvect M);

        then ex X st x = X & X is Vector of M;

        hence thesis;

      end;

    end;

    registration

      let M;

      cluster ( setvect M) -> non empty;

      coherence

      proof

        ( ID M) in ( setvect M);

        hence thesis;

      end;

    end

    reserve u1,v1,w1,W,W1,W2,T for Element of ( setvect M);

    definition

      let M, u1, v1;

      :: MIDSP_1:def13

      func u1 + v1 -> Element of ( setvect M) means

      : Def13: for u, v holds u1 = u & v1 = v implies it = (u + v);

      existence

      proof

        reconsider u2 = u1, v2 = v1 as Vector of M by Th48;

        reconsider suma = (u2 + v2) as Element of ( setvect M) by Th48;

        take suma;

        thus thesis;

      end;

      uniqueness

      proof

        reconsider u = u1, v = v1 as Vector of M by Th48;

        let W1, W2 such that

         A1: for u, v holds u1 = u & v1 = v implies W1 = (u + v) and

         A2: for u, v holds u1 = u & v1 = v implies W2 = (u + v);

        W1 = (u + v) by A1;

        hence thesis by A2;

      end;

    end

    theorem :: MIDSP_1:49

    

     Th49: (u1 + v1) = (v1 + u1)

    proof

      reconsider u = u1, v = v1 as Vector of M by Th48;

      

      thus (u1 + v1) = (u + v) by Def13

      .= (v + u) by Th46

      .= (v1 + u1) by Def13;

    end;

    theorem :: MIDSP_1:50

    

     Th50: ((u1 + v1) + w1) = (u1 + (v1 + w1))

    proof

      reconsider u = u1, v = v1, w = w1 as Vector of M by Th48;

      

       A1: (v1 + w1) = (v + w) by Def13;

      (u1 + v1) = (u + v) by Def13;

      

      hence ((u1 + v1) + w1) = ((u + v) + w) by Def13

      .= (u + (v + w)) by Th43

      .= (u1 + (v1 + w1)) by A1, Def13;

    end;

    definition

      let M;

      :: MIDSP_1:def14

      func addvect (M) -> BinOp of ( setvect M) means

      : Def14: for u1, v1 holds (it . (u1,v1)) = (u1 + v1);

      existence

      proof

        defpred P[ Element of ( setvect M), Element of ( setvect M), Element of ( setvect M)] means $3 = ($1 + $2);

        

         A1: for u1, v1 holds ex W st P[u1, v1, W];

        consider o be BinOp of ( setvect M) such that

         A2: for u1, v1 holds P[u1, v1, (o . (u1,v1))] from BINOP_1:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be BinOp of ( setvect M) such that

         A3: for u1, v1 holds (f . (u1,v1)) = (u1 + v1) and

         A4: for u1, v1 holds (g . (u1,v1)) = (u1 + v1);

        for u1, v1 holds (f . (u1,v1)) = (g . (u1,v1))

        proof

          let u1, v1;

          (f . (u1,v1)) = (u1 + v1) by A3;

          hence thesis by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: MIDSP_1:51

    

     Th51: for W holds ex T st (W + T) = ( ID M)

    proof

      let W;

      reconsider x = W as Vector of M by Th48;

      consider y be Vector of M such that

       A1: (x + y) = ( ID M) by Th45;

      reconsider T = y as Element of ( setvect M) by Th48;

      (x + y) = (W + T) by Def13;

      hence thesis by A1;

    end;

    theorem :: MIDSP_1:52

    

     Th52: for W, W1, W2 st (W + W1) = ( ID M) & (W + W2) = ( ID M) holds W1 = W2

    proof

      let W, W1, W2 such that

       A1: (W + W1) = ( ID M) & (W + W2) = ( ID M);

      reconsider x = W, y1 = W1, y2 = W2 as Vector of M by Th48;

      (x + y1) = (W + W2) by A1, Def13

      .= (x + y2) by Def13;

      hence thesis by Th47;

    end;

    definition

      let M;

      :: MIDSP_1:def15

      func complvect (M) -> UnOp of ( setvect M) means

      : Def15: for W holds (W + (it . W)) = ( ID M);

      existence

      proof

        defpred Z[ Element of ( setvect M), Element of ( setvect M)] means ($1 + $2) = ( ID M);

        

         A1: for W holds ex T st Z[W, T] by Th51;

        consider o be UnOp of ( setvect M) such that

         A2: for W holds Z[W, (o . W)] from FUNCT_2:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be UnOp of ( setvect M) such that

         A3: (for W holds (W + (f . W)) = ( ID M)) & for W holds (W + (g . W)) = ( ID M);

        for W holds (f . W) = (g . W)

        proof

          let W;

          (W + (f . W)) = ( ID M) & (W + (g . W)) = ( ID M) by A3;

          hence thesis by Th52;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let M;

      :: MIDSP_1:def16

      func zerovect (M) -> Element of ( setvect M) equals ( ID M);

      coherence by Th48;

    end

    definition

      let M;

      :: MIDSP_1:def17

      func vectgroup (M) -> addLoopStr equals addLoopStr (# ( setvect M), ( addvect M), ( zerovect M) #);

      coherence ;

    end

    registration

      let M;

      cluster ( vectgroup M) -> strict non empty;

      coherence ;

    end

    theorem :: MIDSP_1:53

    the carrier of ( vectgroup M) = ( setvect M);

    theorem :: MIDSP_1:54

    the addF of ( vectgroup M) = ( addvect M);

    theorem :: MIDSP_1:55

    ( 0. ( vectgroup M)) = ( zerovect M);

    theorem :: MIDSP_1:56

    ( vectgroup M) is add-associative right_zeroed right_complementable Abelian

    proof

      set GS = ( vectgroup M);

      thus GS is add-associative

      proof

        let x,y,z be Element of GS;

        reconsider xx = x, yy = y, zz = z as Element of ( setvect M);

        

        thus ((x + y) + z) = (( addvect M) . ((xx + yy),zz)) by Def14

        .= ((xx + yy) + zz) by Def14

        .= (xx + (yy + zz)) by Th50

        .= (( addvect M) . (xx,(yy + zz))) by Def14

        .= (x + (y + z)) by Def14;

      end;

      thus GS is right_zeroed

      proof

        let x be Element of GS;

        reconsider xx = x as Element of ( setvect M);

        thus (x + ( 0. GS)) = x

        proof

          reconsider xxx = xx as Vector of M by Th48;

          (xx + ( zerovect M)) = (xxx + ( ID M)) by Def13

          .= x by Th44;

          hence thesis by Def14;

        end;

      end;

      thus GS is right_complementable

      proof

        let x be Element of GS;

        reconsider xx = x as Element of ( setvect M);

        reconsider w = (( complvect M) . xx) as Element of GS;

        take w;

        

        thus (x + w) = (xx + (( complvect M) . xx)) by Def14

        .= ( 0. GS) by Def15;

      end;

      thus GS is Abelian

      proof

        let x,y be Element of GS;

        reconsider xx = x, yy = y as Element of ( setvect M);

        

        thus (x + y) = (xx + yy) by Def14

        .= (yy + xx) by Th49

        .= (y + x) by Def14;

      end;

    end;