:: MIDSP_2 semantic presentation

begin


definition
let G be non empty addLoopStr ;
let x be Element of G;
func Double x ->  Element of G equals :: MIDSP_2:def 1
x + x;
coherence
 x + x is Element of G ;
end;

:: deftheorem  defines Double MIDSP_2:def_1_:_
 for G being non empty addLoopStr
for x being Element of G holds Double x = x + x;

definition
let M be non empty MidStr ;
let G be non empty addLoopStr ;
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G;
attrw is associating  means :Def2: :: MIDSP_2:def 2
 for p, q, r being Point of M holds
( p @ q = r iff w . (p,r) = w . (r,q) );
end;

:: deftheorem Def2 defines associating MIDSP_2:def_2_:_
 for M being non empty MidStr
for G being non empty addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G holds
( w is associating iff for p, q, r being Point of M holds
( p @ q = r iff w . (p,r) = w . (r,q) ) );

theorem Th1: :: MIDSP_2:1
for G being non empty addLoopStr
for M being non empty MidStr
for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
proof
let G be non empty addLoopStr ; ::_thesis: for M being non empty MidStr
for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let M be non empty MidStr ; ::_thesis: for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let p be Point of M; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is associating implies p @ p = p )
A1: w . (p,p) = w . (p,p) ;
assume  w is associating ; ::_thesis: p @ p = p
hence  p @ p = p by A1, Def2; ::_thesis: verum
end;


definition
let S be non empty set ;
let G be non empty addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
predw is_atlas_of S,G means :Def3: :: MIDSP_2:def 3
( ( for a being Element of S
for x being Element of G ex b being Element of S st w . (a,b) = x ) & ( for a, b, c being Element of S st w . (a,b) = w . (a,c) holds
b = c ) & ( for a, b, c being Element of S holds (w . (a,b)) + (w . (b,c)) = w . (a,c) ) );
end;

:: deftheorem Def3 defines is_atlas_of MIDSP_2:def_3_:_
 for S being non empty set
for G being non empty addLoopStr
for w being Function of [:S,S:], the carrier of G holds
( w is_atlas_of S,G iff ( ( for a being Element of S
for x being Element of G ex b being Element of S st w . (a,b) = x ) & ( for a, b, c being Element of S st w . (a,b) = w . (a,c) holds
b = c ) & ( for a, b, c being Element of S holds (w . (a,b)) + (w . (b,c)) = w . (a,c) ) ) );

definition
let S be non empty set ;
let G be non empty addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
let a be Element of S;
let x be Element of G;
assume A1: w is_atlas_of S,G ;
func(a,x) . w ->  Element of S means :Def4: :: MIDSP_2:def 4
w . (a,it) = x;
existence
 ex b1 being Element of S st w . (a,b1) = x by A1, Def3;
uniqueness
 for b1, b2 being Element of S st w . (a,b1) = x & w . (a,b2) = x holds
b1 = b2 by A1, Def3;
end;

:: deftheorem Def4 defines . MIDSP_2:def_4_:_
 for S being non empty set
for G being non empty addLoopStr
for w being Function of [:S,S:], the carrier of G
for a being Element of S
for x being Element of G st w is_atlas_of S,G holds
for b6 being Element of S holds
( b6 = (a,x) . w iff w . (a,b6) = x );


theorem Th2: :: MIDSP_2:2
for S being non empty set
for a being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,a) = 0. G
proof
let S be non empty set ; ::_thesis: for a being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,a) = 0. G
let a be Element of S; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,a) = 0. G
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,a) = 0. G
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies w . (a,a) = 0. G )
assume  w is_atlas_of S,G ; ::_thesis: w . (a,a) = 0. G
then  (w . (a,a)) + (w . (a,a)) = w . (a,a) by Def3;
hence  w . (a,a) = 0. G by RLVECT_1:9; ::_thesis: verum
end;

theorem Th3: :: MIDSP_2:3
for S being non empty set
for a, b being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = 0. G holds
a = b
proof
let S be non empty set ; ::_thesis: for a, b being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = 0. G holds
a = b
let a, b be Element of S; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = 0. G holds
a = b
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = 0. G holds
a = b
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G & w . (a,b) = 0. G implies a = b )
assume that
A1: w is_atlas_of S,G and
A2: w . (a,b) = 0. G ; ::_thesis: a = b
 w . (a,b) = w . (a,a) by A1, A2, Th2;
hence  a = b by A1, Def3; ::_thesis: verum
end;

theorem Th4: :: MIDSP_2:4
for S being non empty set
for a, b being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
proof
let S be non empty set ; ::_thesis: for a, b being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let a, b be Element of S; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies w . (a,b) = - (w . (b,a)) )
assume A1: w is_atlas_of S,G ; ::_thesis: w . (a,b) = - (w . (b,a))
then (w . (b,a)) + (w . (a,b)) = w . (b,b) by Def3
.= 0. G by A1, Th2 ;
then  - (w . (b,a)) = - (- (w . (a,b))) by RLVECT_1:6;
hence  w . (a,b) = - (w . (b,a)) by RLVECT_1:17; ::_thesis: verum
end;

theorem Th5: :: MIDSP_2:5
for S being non empty set
for a, b, c, d being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = w . (c,d) holds
w . (b,a) = w . (d,c)
proof
let S be non empty set ; ::_thesis: for a, b, c, d being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = w . (c,d) holds
w . (b,a) = w . (d,c)
let a, b, c, d be Element of S; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = w . (c,d) holds
w . (b,a) = w . (d,c)
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (a,b) = w . (c,d) holds
w . (b,a) = w . (d,c)
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G & w . (a,b) = w . (c,d) implies w . (b,a) = w . (d,c) )
assume that
A1: w is_atlas_of S,G and
A2: w . (a,b) = w . (c,d) ; ::_thesis: w . (b,a) = w . (d,c)
thus w . (b,a) = - (w . (c,d)) by A1, A2, Th4
.= w . (d,c) by A1, Th4 ; ::_thesis: verum
end;

theorem Th6: :: MIDSP_2:6
for S being non empty set
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x
proof
let S be non empty set ; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x )
assume A1: w is_atlas_of S,G ; ::_thesis: for b being Element of S
for x being Element of G ex a being Element of S st w . (a,b) = x
let b be Element of S; ::_thesis: for x being Element of G ex a being Element of S st w . (a,b) = x
let x be Element of G; ::_thesis: ex a being Element of S st w . (a,b) = x
consider a being Element of S such that
A2: w . (b,a) = - x by A1, Def3;
take  a ; ::_thesis: w . (a,b) = x
w . (a,b) = - (- x) by A1, A2, Th4
.= x by RLVECT_1:17 ;
hence  w . (a,b) = x ; ::_thesis: verum
end;

theorem Th7: :: MIDSP_2:7
for S being non empty set
for b, a, c being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (b,a) = w . (c,a) holds
b = c
proof
let S be non empty set ; ::_thesis: for b, a, c being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (b,a) = w . (c,a) holds
b = c
let b, a, c be Element of S; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (b,a) = w . (c,a) holds
b = c
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G & w . (b,a) = w . (c,a) holds
b = c
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G & w . (b,a) = w . (c,a) implies b = c )
assume that
A1: w is_atlas_of S,G and
A2: w . (b,a) = w . (c,a) ; ::_thesis: b = c
 w . (a,b) = w . (a,c) by A1, A2, Th5;
hence  b = c by A1, Def3; ::_thesis: verum
end;

theorem Th8: :: MIDSP_2:8
for M being non empty MidStr
for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
p @ q = q @ p
proof
let M be non empty MidStr ; ::_thesis: for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
p @ q = q @ p
let p, q be Point of M; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
p @ q = q @ p
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
p @ q = q @ p
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies p @ q = q @ p )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; ::_thesis: p @ q = q @ p
set r = p @ q;
 w . (p,(p @ q)) = w . ((p @ q),q) by A2, Def2;
then  w . ((p @ q),p) = w . (q,(p @ q)) by A1, Th5;
hence  p @ q = q @ p by A2, Def2; ::_thesis: verum
end;

theorem Th9: :: MIDSP_2:9
for M being non empty MidStr
for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
ex r being Point of M st r @ p = q
proof
let M be non empty MidStr ; ::_thesis: for p, q being Point of M
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
ex r being Point of M st r @ p = q
let p, q be Point of M; ::_thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
ex r being Point of M st r @ p = q
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
ex r being Point of M st r @ p = q
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ex r being Point of M st r @ p = q )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; ::_thesis: ex r being Point of M st r @ p = q
consider r being Point of M such that
A3: w . (r,q) = w . (q,p) by A1, Th6;
take  r ; ::_thesis: r @ p = q
thus  r @ p = q by A2, A3, Def2; ::_thesis: verum
end;


theorem Th10: :: MIDSP_2:10
for G being non empty Abelian add-associative addLoopStr
for x, y, z, t being Element of G holds (x + y) + (z + t) = (x + z) + (y + t)
proof
let G be non empty Abelian add-associative addLoopStr ; ::_thesis: for x, y, z, t being Element of G holds (x + y) + (z + t) = (x + z) + (y + t)
let x, y, z, t be Element of G; ::_thesis: (x + y) + (z + t) = (x + z) + (y + t)
thus (x + y) + (z + t) = x + (y + (z + t)) by RLVECT_1:def_3
.= x + (z + (y + t)) by RLVECT_1:def_3
.= (x + z) + (y + t) by RLVECT_1:def_3 ; ::_thesis: verum
end;

theorem :: MIDSP_2:11
for G being non empty Abelian add-associative addLoopStr
for x, y being Element of G holds Double (x + y) = (Double x) + (Double y) by Th10;

theorem Th12: :: MIDSP_2:12
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x being Element of G holds Double (- x) = - (Double x)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for x being Element of G holds Double (- x) = - (Double x)
let x be Element of G; ::_thesis: Double (- x) = - (Double x)
0. G = Double (0. G) by RLVECT_1:def_4
.= Double (x + (- x)) by RLVECT_1:def_10
.= (Double x) + (Double (- x)) by Th10 ;
hence  Double (- x) = - (Double x) by RLVECT_1:6; ::_thesis: verum
end;

theorem Th13: :: MIDSP_2:13
for M being non empty MidStr
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
proof
let M be non empty MidStr ; ::_thesis: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) ) )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; ::_thesis: for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
let a, b, c, d be Point of M; ::_thesis: ( a @ b = c @ d iff w . (a,d) = w . (c,b) )
thus  ( a @ b = c @ d implies w . (a,d) = w . (c,b) ) ::_thesis: ( w . (a,d) = w . (c,b) implies a @ b = c @ d )
proof
set p = a @ b;
assume  a @ b = c @ d ; ::_thesis: w . (a,d) = w . (c,b)
then A3: w . (c,(a @ b)) = w . ((a @ b),d) by A2, Def2;
 w . (a,(a @ b)) = w . ((a @ b),b) by A2, Def2;
hence w . (a,d) = (w . (c,(a @ b))) + (w . ((a @ b),b)) by A1, A3, Def3
.= w . (c,b) by A1, Def3 ;
::_thesis: verum
end;
thus  ( w . (a,d) = w . (c,b) implies a @ b = c @ d ) ::_thesis: verum
proof
set p = a @ b;
assume A4: w . (a,d) = w . (c,b) ; ::_thesis: a @ b = c @ d
(w . ((a @ b),b)) + (w . ((a @ b),d)) = (w . (a,(a @ b))) + (w . ((a @ b),d)) by A2, Def2
.= w . (a,d) by A1, Def3
.= (w . ((a @ b),b)) + (w . (c,(a @ b))) by A1, A4, Def3 ;
then  w . ((a @ b),d) = w . (c,(a @ b)) by RLVECT_1:8;
hence  a @ b = c @ d by A2, Def2; ::_thesis: verum
end;
end;

theorem Th14: :: MIDSP_2:14
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9))
proof
let S be non empty set ; ::_thesis: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9))
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9))
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9)) )
assume A1: w is_atlas_of S,G ; ::_thesis: for a, b, b9, c, c9 being Element of S st w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) holds
w . (c,c9) = Double (w . (b,b9))
let a, b, b9, c, c9 be Element of S; ::_thesis: ( w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) implies w . (c,c9) = Double (w . (b,b9)) )
assume A2: ( w . (a,b) = w . (b,c) & w . (a,b9) = w . (b9,c9) ) ; ::_thesis: w . (c,c9) = Double (w . (b,b9))
thus w . (c,c9) = (w . (c,b9)) + (w . (b9,c9)) by A1, Def3
.= ((w . (c,a)) + (w . (a,b9))) + (w . (b9,c9)) by A1, Def3
.= (((w . (c,b)) + (w . (b,a))) + (w . (a,b9))) + (w . (b9,c9)) by A1, Def3
.= ((Double (w . (b,a))) + (w . (a,b9))) + (w . (a,b9)) by A1, A2, Th5
.= (Double (w . (b,a))) + (Double (w . (a,b9))) by RLVECT_1:def_3
.= Double ((w . (b,a)) + (w . (a,b9))) by Th10
.= Double (w . (b,b9)) by A1, Def3 ; ::_thesis: verum
end;


registration
let M be MidSp;
cluster vectgroup M ->  right_complementable Abelian add-associative right_zeroed ;
coherence
 ( vectgroup M is Abelian & vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable ) by MIDSP_1:56;
end;

theorem Th15: :: MIDSP_2:15
for M being MidSp holds
( ( for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
proof
let M be MidSp; ::_thesis: ( ( for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
set G = vectgroup M;
thus  for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) ::_thesis: ( 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
proof
let a be set ; ::_thesis: ( a is Element of (vectgroup M) iff a is Vector of M )
 ( a is Element of (vectgroup M) iff a is Element of setvect M ) by MIDSP_1:53;
hence  ( a is Element of (vectgroup M) iff a is Vector of M ) by MIDSP_1:48; ::_thesis: verum
end;
thus  0. (vectgroup M) = zerovect M by MIDSP_1:55
.= ID M by MIDSP_1:def_16 ; ::_thesis: for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y
thus  for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ::_thesis: verum
proof
let a, b be Element of (vectgroup M); ::_thesis: for x, y being Vector of M st a = x & b = y holds
a + b = x + y
let x, y be Vector of M; ::_thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; ::_thesis: a + b = x + y
reconsider xx = x, yy = y as Element of setvect M by MIDSP_1:48;
thus a + b = the addF of (vectgroup M) . (a,b) by RLVECT_1:2
.= (addvect M) . (xx,yy) by A1, MIDSP_1:54
.= xx + yy by MIDSP_1:def_14
.= x + y by MIDSP_1:def_13 ; ::_thesis: verum
end;
end;

Lm1:  for M being MidSp holds
( ( for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a ) & ( for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M) ) )
proof
let M be MidSp; ::_thesis: ( ( for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a ) & ( for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M) ) )
set G = vectgroup M;
set p = the Point of M;
thus  for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a ::_thesis: for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M)
proof
set p = the Point of M;
let a be Element of (vectgroup M); ::_thesis: ex x being Element of (vectgroup M) st Double x = a
reconsider aa = a as Vector of M by Th15;
consider q being Point of M such that
A1: aa = vect ( the Point of M,q) by MIDSP_1:35;
set xx = vect ( the Point of M,( the Point of M @ q));
reconsider x = vect ( the Point of M,( the Point of M @ q)) as Element of (vectgroup M) by Th15;
take  x ; ::_thesis: Double x = a
 (vect ( the Point of M,( the Point of M @ q))) + (vect ( the Point of M,( the Point of M @ q))) = aa by A1, MIDSP_1:42;
hence  Double x = a by Th15; ::_thesis: verum
end;
let a be Element of (vectgroup M); ::_thesis: ( Double a = 0. (vectgroup M) implies a = 0. (vectgroup M) )
reconsider aa = a as Vector of M by Th15;
consider q being Point of M such that
A2: aa = vect ( the Point of M,q) by MIDSP_1:35;
consider r being Point of M such that
A3: aa = vect (q,r) by MIDSP_1:35;
assume  Double a = 0. (vectgroup M) ; ::_thesis: a = 0. (vectgroup M)
then aa + aa = 0. (vectgroup M) by Th15
.= ID M by Th15 ;
then  (vect ( the Point of M,q)) + (vect (q,r)) = vect ( the Point of M, the Point of M) by A2, A3, MIDSP_1:38;
then  vect ( the Point of M,r) = vect ( the Point of M, the Point of M) by MIDSP_1:40;
then  vect ( the Point of M,q) = vect (q, the Point of M) by A2, A3, MIDSP_1:39;
then A4: the Point of M @ the Point of M = q @ q by MIDSP_1:37;
the Point of M = the Point of M @ the Point of M by MIDSP_1:def_3
.= q by A4, MIDSP_1:def_3 ;
hence a = ID M by A2, MIDSP_1:38
.= 0. (vectgroup M) by Th15 ;
::_thesis: verum
end;

definition
let IT be non empty addLoopStr ;
attrIT is midpoint_operator  means :Def5: :: MIDSP_2:def 5
( ( for a being Element of IT ex x being Element of IT st Double x = a ) & ( for a being Element of IT st Double a = 0. IT holds
a = 0. IT ) );
end;

:: deftheorem Def5 defines midpoint_operator MIDSP_2:def_5_:_
 for IT being non empty addLoopStr holds
( IT is midpoint_operator iff ( ( for a being Element of IT ex x being Element of IT st Double x = a ) & ( for a being Element of IT st Double a = 0. IT holds
a = 0. IT ) ) );

registration
cluster non empty midpoint_operator  ->  non empty Fanoian for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is midpoint_operator holds
b1 is Fanoian
proof
let L be non empty addLoopStr ; ::_thesis: ( L is midpoint_operator implies L is Fanoian )
assume A1: L is midpoint_operator ; ::_thesis: L is Fanoian
let a be Element of L; :: according to VECTSP_1:def_18 ::_thesis: ( not a + a = 0. L or a = 0. L )
assume  a + a = 0. L ; ::_thesis: a = 0. L
then  Double a = 0. L ;
hence  a = 0. L by A1, Def5; ::_thesis: verum
end;
end;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed midpoint_operator for addLoopStr ;
existence
 ex b1 being non empty addLoopStr st
( b1 is strict & b1 is midpoint_operator & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian )
proof
set M = the MidSp;
set G = vectgroup the MidSp;
 ( ( for a being Element of (vectgroup the MidSp) ex x being Element of (vectgroup the MidSp) st Double x = a ) & ( for a being Element of (vectgroup the MidSp) st Double a = 0. (vectgroup the MidSp) holds
a = 0. (vectgroup the MidSp) ) ) by Lm1;
then  vectgroup the MidSp is midpoint_operator by Def5;
hence  ex b1 being non empty addLoopStr st
( b1 is strict & b1 is midpoint_operator & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian ) ; ::_thesis: verum
end;
end;


theorem Th16: :: MIDSP_2:16
for G being non empty right_complementable Fanoian add-associative right_zeroed addLoopStr
for x being Element of G st x = - x holds
x = 0. G
proof
let G be non empty right_complementable Fanoian add-associative right_zeroed addLoopStr ; ::_thesis: for x being Element of G st x = - x holds
x = 0. G
let x be Element of G; ::_thesis: ( x = - x implies x = 0. G )
A1: (- x) + x = 0. G by RLVECT_1:5;
assume  x = - x ; ::_thesis: x = 0. G
hence  x = 0. G by A1, VECTSP_1:def_18; ::_thesis: verum
end;

theorem Th17: :: MIDSP_2:17
for G being non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr
for x, y being Element of G st Double x = Double y holds
x = y
proof
let G be non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for x, y being Element of G st Double x = Double y holds
x = y
let x, y be Element of G; ::_thesis: ( Double x = Double y implies x = y )
assume  Double x = Double y ; ::_thesis: x = y
then  0. G = (x + x) + (- (y + y)) by RLVECT_1:def_10
.= (x + x) + ((- y) + (- y)) by RLVECT_1:31
.= x + (x + ((- y) + (- y))) by RLVECT_1:def_3
.= x + ((x + (- y)) + (- y)) by RLVECT_1:def_3
.= (x + (- y)) + (x + (- y)) by RLVECT_1:def_3 ;
then  (- y) + x = 0. G by VECTSP_1:def_18;
hence x = - (- y) by RLVECT_1:6
.= y by RLVECT_1:17 ;
::_thesis: verum
end;

definition
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let x be Element of G;
func Half x ->  Element of G means :Def6: :: MIDSP_2:def 6
 Double it = x;
existence
 ex b1 being Element of G st Double b1 = x by Def5;
uniqueness
 for b1, b2 being Element of G st Double b1 = x & Double b2 = x holds
b1 = b2 by Th17;
end;

:: deftheorem Def6 defines Half MIDSP_2:def_6_:_
 for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for x, b3 being Element of G holds
( b3 = Half x iff Double b3 = x );

theorem :: MIDSP_2:18
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for x, y being Element of G holds
( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )
proof
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for x, y being Element of G holds
( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )
let x, y be Element of G; ::_thesis: ( Half (0. G) = 0. G & Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )
 Double (0. G) = 0. G by RLVECT_1:def_4;
hence  Half (0. G) = 0. G by Def6; ::_thesis: ( Half (x + y) = (Half x) + (Half y) & ( Half x = Half y implies x = y ) & Half (Double x) = x )
Double ((Half x) + (Half y)) = (Double (Half x)) + (Double (Half y)) by Th10
.= x + (Double (Half y)) by Def6
.= x + y by Def6 ;
hence  Half (x + y) = (Half x) + (Half y) by Def6; ::_thesis: ( ( Half x = Half y implies x = y ) & Half (Double x) = x )
thus  ( Half x = Half y implies x = y ) ::_thesis: Half (Double x) = x
proof
assume  Half x = Half y ; ::_thesis: x = y
hence x = Double (Half y) by Def6
.= y by Def6 ;
::_thesis: verum
end;
thus  Half (Double x) = x by Def6; ::_thesis: verum
end;

theorem Th19: :: MIDSP_2:19
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
let M be non empty MidStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d) )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; ::_thesis: for a, b, c, d being Point of M holds (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
let a, b, c, d be Point of M; ::_thesis: (a @ b) @ (c @ d) = (a @ c) @ (b @ d)
A3: w . (b,(a @ b)) = w . (b,(b @ a)) by A1, A2, Th8
.= w . ((b @ a),a) by A2, Def2
.= w . ((a @ b),a) by A1, A2, Th8 ;
set p = (a @ b) @ (c @ d);
A4: w . (c,(c @ d)) = w . ((c @ d),d) by A2, Def2;
A5: w . (b,(b @ d)) = w . ((b @ d),d) by A2, Def2;
w . (c,(a @ c)) = w . (c,(c @ a)) by A1, A2, Th8
.= w . ((c @ a),a) by A2, Def2
.= w . ((a @ c),a) by A1, A2, Th8 ;
then  Double (w . ((a @ c),(c @ d))) = w . (a,d) by A1, A4, Th14
.= - (w . (d,a)) by A1, Th4
.= - (Double (w . ((b @ d),(a @ b)))) by A1, A5, A3, Th14
.= Double (- (w . ((b @ d),(a @ b)))) by Th12
.= Double (w . ((a @ b),(b @ d))) by A1, Th4 ;
then  w . ((a @ c),(c @ d)) = w . ((a @ b),(b @ d)) by Th17;
then A6: (w . ((a @ c),((a @ b) @ (c @ d)))) + (w . (((a @ b) @ (c @ d)),(c @ d))) = w . ((a @ b),(b @ d)) by A1, Def3
.= (w . (((a @ b) @ (c @ d)),(b @ d))) + (w . ((a @ b),((a @ b) @ (c @ d)))) by A1, Def3 ;
 w . ((a @ b),((a @ b) @ (c @ d))) = w . (((a @ b) @ (c @ d)),(c @ d)) by A2, Def2;
then  w . ((a @ c),((a @ b) @ (c @ d))) = w . (((a @ b) @ (c @ d)),(b @ d)) by A6, RLVECT_1:8;
hence  (a @ b) @ (c @ d) = (a @ c) @ (b @ d) by A2, Def2; ::_thesis: verum
end;

theorem Th20: :: MIDSP_2:20
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
M is MidSp
proof
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
M is MidSp
let M be non empty MidStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of the carrier of M,G & w is associating holds
M is MidSp
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies M is MidSp )
assume  ( w is_atlas_of the carrier of M,G & w is associating ) ; ::_thesis: M is MidSp
then  for a, b, c, d being Point of M holds
( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Point of M st x @ a = b ) by Th1, Th8, Th9, Th19;
hence  M is MidSp by MIDSP_1:def_3; ::_thesis: verum
end;


registration
let M be MidSp;
cluster vectgroup M ->  midpoint_operator ;
coherence
 vectgroup M is midpoint_operator
proof
set G = vectgroup M;
 ( ( for x being Element of (vectgroup M) ex y being Element of (vectgroup M) st Double y = x ) & ( for x being Element of (vectgroup M) st Double x = 0. (vectgroup M) holds
x = 0. (vectgroup M) ) ) by Lm1;
hence  vectgroup M is midpoint_operator by Def5; ::_thesis: verum
end;
end;

definition
let M be MidSp;
let p, q be Point of M;
func vector (p,q) ->  Element of (vectgroup M) equals :: MIDSP_2:def 7
 vect (p,q);
coherence
 vect (p,q) is Element of (vectgroup M) by Th15;
end;

:: deftheorem  defines vector MIDSP_2:def_7_:_
 for M being MidSp
for p, q being Point of M holds vector (p,q) = vect (p,q);

definition
let M be MidSp;
func vect M ->  Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) means :Def8: :: MIDSP_2:def 8
 for p, q being Point of M holds it . (p,q) = vect (p,q);
existence
 ex b1 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
for p, q being Point of M holds b1 . (p,q) = vect (p,q)
proof
deffunc H1( Point of M, Point of M) ->  Element of (vectgroup M) = vector ($1,$2);
consider f being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) such that
A1: for p, q being Point of M holds f . (p,q) = H1(p,q) from BINOP_1:sch_4();
take  f ; ::_thesis: for p, q being Point of M holds f . (p,q) = vect (p,q)
 for p, q being Point of M holds f . (p,q) = vect (p,q)
proof
let p, q be Point of M; ::_thesis: f . (p,q) = vect (p,q)
thus f . (p,q) = vector (p,q) by A1
.= vect (p,q) ; ::_thesis: verum
end;
hence  for p, q being Point of M holds f . (p,q) = vect (p,q) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st ( for p, q being Point of M holds b1 . (p,q) = vect (p,q) ) & ( for p, q being Point of M holds b2 . (p,q) = vect (p,q) ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M); ::_thesis: ( ( for p, q being Point of M holds f . (p,q) = vect (p,q) ) & ( for p, q being Point of M holds g . (p,q) = vect (p,q) ) implies f = g )
assume that
A2: for p, q being Point of M holds f . (p,q) = vect (p,q) and
A3: for p, q being Point of M holds g . (p,q) = vect (p,q) ; ::_thesis: f = g
 for p, q being Point of M holds f . (p,q) = g . (p,q)
proof
let p, q be Point of M; ::_thesis: f . (p,q) = g . (p,q)
thus f . (p,q) = vect (p,q) by A2
.= g . (p,q) by A3 ; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines vect MIDSP_2:def_8_:_
 for M being MidSp
for b2 being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) holds
( b2 = vect M iff for p, q being Point of M holds b2 . (p,q) = vect (p,q) );

theorem Th21: :: MIDSP_2:21
for M being MidSp holds vect M is_atlas_of the carrier of M, vectgroup M
proof
let M be MidSp; ::_thesis: vect M is_atlas_of the carrier of M, vectgroup M
set w = vect M;
A1: for p being Point of M
for x being Element of (vectgroup M) ex q being Point of M st (vect M) . (p,q) = x
proof
let p be Point of M; ::_thesis: for x being Element of (vectgroup M) ex q being Point of M st (vect M) . (p,q) = x
let x be Element of (vectgroup M); ::_thesis: ex q being Point of M st (vect M) . (p,q) = x
reconsider xx = x as Vector of M by Th15;
consider q being Point of M such that
A2: xx = vect (p,q) by MIDSP_1:35;
take  q ; ::_thesis: (vect M) . (p,q) = x
thus  (vect M) . (p,q) = x by A2, Def8; ::_thesis: verum
end;
A3: for p, q, r being Point of M st (vect M) . (p,q) = (vect M) . (p,r) holds
q = r
proof
let p, q, r be Point of M; ::_thesis: ( (vect M) . (p,q) = (vect M) . (p,r) implies q = r )
assume  (vect M) . (p,q) = (vect M) . (p,r) ; ::_thesis: q = r
then  vect (p,q) = (vect M) . (p,r) by Def8
.= vect (p,r) by Def8 ;
hence  q = r by MIDSP_1:39; ::_thesis: verum
end;
 for p, q, r being Point of M holds ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect M) . (p,r)
proof
let p, q, r be Point of M; ::_thesis: ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect M) . (p,r)
 ( (vect M) . (p,q) = vect (p,q) & (vect M) . (q,r) = vect (q,r) ) by Def8;
hence ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect (p,q)) + (vect (q,r)) by Th15
.= vect (p,r) by MIDSP_1:40
.= (vect M) . (p,r) by Def8 ;
::_thesis: verum
end;
hence  vect M is_atlas_of the carrier of M, vectgroup M by A1, A3, Def3; ::_thesis: verum
end;

theorem Th22: :: MIDSP_2:22
for M being MidSp
for p, q, r, s being Point of M holds
( vect (p,q) = vect (r,s) iff p @ s = q @ r )
proof
let M be MidSp; ::_thesis: for p, q, r, s being Point of M holds
( vect (p,q) = vect (r,s) iff p @ s = q @ r )
let p, q, r, s be Point of M; ::_thesis: ( vect (p,q) = vect (r,s) iff p @ s = q @ r )
thus  ( vect (p,q) = vect (r,s) implies p @ s = q @ r ) by MIDSP_1:37; ::_thesis: ( p @ s = q @ r implies vect (p,q) = vect (r,s) )
thus  ( p @ s = q @ r implies vect (p,q) = vect (r,s) ) ::_thesis: verum
proof
assume  p @ s = q @ r ; ::_thesis: vect (p,q) = vect (r,s)
then  p,q @@ r,s by MIDSP_1:def_4;
then  [p,q] ## [r,s] by MIDSP_1:19;
hence  vect (p,q) = vect (r,s) by MIDSP_1:36; ::_thesis: verum
end;
end;

theorem Th23: :: MIDSP_2:23
for M being MidSp
for p, q, r being Point of M holds
( p @ q = r iff vect (p,r) = vect (r,q) )
proof
let M be MidSp; ::_thesis: for p, q, r being Point of M holds
( p @ q = r iff vect (p,r) = vect (r,q) )
let p, q, r be Point of M; ::_thesis: ( p @ q = r iff vect (p,r) = vect (r,q) )
 ( p @ q = r iff p @ q = r @ r ) by MIDSP_1:def_3;
hence  ( p @ q = r iff vect (p,r) = vect (r,q) ) by Th22; ::_thesis: verum
end;

theorem :: MIDSP_2:24
canceled;

Lm2:  for M being MidSp holds vect M is associating
proof
let M be MidSp; ::_thesis: vect M is associating
let p be Point of M; :: according to MIDSP_2:def_2 ::_thesis: for q, r being Point of M holds
( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) )
let q, r be Point of M; ::_thesis: ( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) )
set w = vect M;
 ( (vect M) . (p,r) = vect (p,r) & (vect M) . (r,q) = vect (r,q) ) by Def8;
hence  ( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) ) by Th23; ::_thesis: verum
end;

registration
let M be MidSp;
cluster vect M ->  associating ;
coherence
 vect M is associating by Lm2;
end;

definition
let S be non empty set ;
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
assume A1: w is_atlas_of S,G ;
func @ w ->  BinOp of S means :Def9: :: MIDSP_2:def 9
 for a, b being Element of S holds w . (a,(it . (a,b))) = w . ((it . (a,b)),b);
existence
 ex b1 being BinOp of S st
for a, b being Element of S holds w . (a,(b1 . (a,b))) = w . ((b1 . (a,b)),b)
proof
defpred S1[ Element of S, Element of S, Element of S] means w . ($1,$3) = w . ($3,$2);
A2: for a, b being Element of S ex c being Element of S st S1[a,b,c]
proof
let a, b be Element of S; ::_thesis: ex c being Element of S st S1[a,b,c]
set x = Half (w . (a,b));
consider c being Element of S such that
A3: w . (a,c) = Half (w . (a,b)) by A1, Def3;
take  c ; ::_thesis: S1[a,b,c]
(Half (w . (a,b))) + (Half (w . (a,b))) = Double (Half (w . (a,b)))
.= w . (a,b) by Def6
.= (Half (w . (a,b))) + (w . (c,b)) by A1, A3, Def3 ;
hence  S1[a,b,c] by A3, RLVECT_1:8; ::_thesis: verum
end;
consider o being BinOp of S such that
A4: for a, b being Element of S holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A2);
take  o ; ::_thesis: for a, b being Element of S holds w . (a,(o . (a,b))) = w . ((o . (a,b)),b)
thus  for a, b being Element of S holds w . (a,(o . (a,b))) = w . ((o . (a,b)),b) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of S st ( for a, b being Element of S holds w . (a,(b1 . (a,b))) = w . ((b1 . (a,b)),b) ) & ( for a, b being Element of S holds w . (a,(b2 . (a,b))) = w . ((b2 . (a,b)),b) ) holds
b1 = b2
proof
defpred S1[ Element of S, Element of S, Element of S] means w . ($1,$3) = w . ($3,$2);
A5: for a, b, c, c9 being Element of S st S1[a,b,c] & S1[a,b,c9] holds
c = c9
proof
let a, b, c, c9 be Element of S; ::_thesis: ( S1[a,b,c] & S1[a,b,c9] implies c = c9 )
assume A6: ( S1[a,b,c] & S1[a,b,c9] ) ; ::_thesis: c = c9
w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1, Def3
.= (w . (c9,b)) + (w . (b,c)) by A1, A6, Th5
.= w . (c9,c) by A1, Def3
.= - (w . (c,c9)) by A1, Th4 ;
then  w . (c,c9) = 0. G by Th16;
hence  c = c9 by A1, Th3; ::_thesis: verum
end;
let f, g be BinOp of S; ::_thesis: ( ( for a, b being Element of S holds w . (a,(f . (a,b))) = w . ((f . (a,b)),b) ) & ( for a, b being Element of S holds w . (a,(g . (a,b))) = w . ((g . (a,b)),b) ) implies f = g )
assume A7: ( ( for a, b being Element of S holds w . (a,(f . (a,b))) = w . ((f . (a,b)),b) ) & ( for a, b being Element of S holds w . (a,(g . (a,b))) = w . ((g . (a,b)),b) ) ) ; ::_thesis: f = g
 for a, b being Element of S holds f . (a,b) = g . (a,b)
proof
let a, b be Element of S; ::_thesis: f . (a,b) = g . (a,b)
 ( w . (a,(f . (a,b))) = w . ((f . (a,b)),b) & w . (a,(g . (a,b))) = w . ((g . (a,b)),b) ) by A7;
hence  f . (a,b) = g . (a,b) by A5; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines @ MIDSP_2:def_9_:_
 for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for b4 being BinOp of S holds
( b4 = @ w iff for a, b being Element of S holds w . (a,(b4 . (a,b))) = w . ((b4 . (a,b)),b) );

theorem Th25: :: MIDSP_2:25
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, c being Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
proof
let S be non empty set ; ::_thesis: for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, c being Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
for a, b, c being Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies for a, b, c being Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) ) )
assume A1: w is_atlas_of S,G ; ::_thesis: for a, b, c being Element of S holds
( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
let a, b, c be Element of S; ::_thesis: ( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) )
thus  ( (@ w) . (a,b) = c implies w . (a,c) = w . (c,b) ) by A1, Def9; ::_thesis: ( w . (a,c) = w . (c,b) implies (@ w) . (a,b) = c )
thus  ( w . (a,c) = w . (c,b) implies (@ w) . (a,b) = c ) ::_thesis: verum
proof
defpred S1[ Element of S, Element of S, Element of S] means w . ($1,$3) = w . ($3,$2);
assume A2: w . (a,c) = w . (c,b) ; ::_thesis: (@ w) . (a,b) = c
A3: for a, b, c, c9 being Element of S st S1[a,b,c] & S1[a,b,c9] holds
c = c9
proof
let a, b, c, c9 be Element of S; ::_thesis: ( S1[a,b,c] & S1[a,b,c9] implies c = c9 )
assume A4: ( S1[a,b,c] & S1[a,b,c9] ) ; ::_thesis: c = c9
w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1, Def3
.= (w . (c9,b)) + (w . (b,c)) by A1, A4, Th5
.= w . (c9,c) by A1, Def3
.= - (w . (c,c9)) by A1, Th4 ;
then  w . (c,c9) = 0. G by Th16;
hence  c = c9 by A1, Th3; ::_thesis: verum
end;
set c9 = (@ w) . (a,b);
 S1[a,b,(@ w) . (a,b)] by A1, Def9;
hence  (@ w) . (a,b) = c by A2, A3; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let M be BinOp of D;
cluster MidStr(# D,M #) ->  non empty ;
coherence
 not MidStr(# D,M #) is empty ;
end;


definition
let S be non empty set ;
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
func Atlas w ->  Function of [: the carrier of MidStr(# S,(@ w) #), the carrier of MidStr(# S,(@ w) #):], the carrier of G equals :: MIDSP_2:def 10
w;
coherence
 w is Function of [: the carrier of MidStr(# S,(@ w) #), the carrier of MidStr(# S,(@ w) #):], the carrier of G ;
end;

:: deftheorem  defines Atlas MIDSP_2:def_10_:_
 for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G holds Atlas w = w;

theorem Th26: :: MIDSP_2:26
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
Atlas w is associating
proof
let S be non empty set ; ::_thesis: for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
Atlas w is associating
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
Atlas w is associating
let w be Function of [:S,S:], the carrier of G; ::_thesis: ( w is_atlas_of S,G implies Atlas w is associating )
assume A1: w is_atlas_of S,G ; ::_thesis: Atlas w is associating
 for a, b, c being Point of MidStr(# S,(@ w) #) holds
( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) )
proof
let a, b, c be Point of MidStr(# S,(@ w) #); ::_thesis: ( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) )
 ( (@ w) . (a,b) = c iff w . (a,c) = w . (c,b) ) by A1, Th25;
hence  ( a @ b = c iff (Atlas w) . (a,c) = (Atlas w) . (c,b) ) by MIDSP_1:def_1; ::_thesis: verum
end;
hence  Atlas w is associating by Def2; ::_thesis: verum
end;

definition
let S be non empty set ;
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ;
let w be Function of [:S,S:], the carrier of G;
assume A1: w is_atlas_of S,G ;
func MidSp. w ->  strict MidSp equals :: MIDSP_2:def 11
 MidStr(# S,(@ w) #);
coherence
 MidStr(# S,(@ w) #) is strict MidSp
proof
set M = MidStr(# S,(@ w) #);
set W = Atlas w;
 Atlas w is associating by A1, Th26;
hence  MidStr(# S,(@ w) #) is strict MidSp by A1, Th20; ::_thesis: verum
end;
end;

:: deftheorem  defines MidSp. MIDSP_2:def_11_:_
 for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
MidSp. w = MidStr(# S,(@ w) #);


theorem Th27: :: MIDSP_2:27
for M being non empty MidStr holds
( M is MidSp iff ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) )
proof
let M be non empty MidStr ; ::_thesis: ( M is MidSp iff ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) )
hereby  ::_thesis: ( ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) implies M is MidSp )
assume A1: M is MidSp ; ::_thesis: ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating )
thus  ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) ::_thesis: verum
proof
reconsider M = M as MidSp by A1;
set G = vectgroup M;
take  vectgroup M ; ::_thesis: ex w being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
( w is_atlas_of the carrier of M, vectgroup M & w is associating )
 ex w being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
( w is_atlas_of the carrier of M, vectgroup M & w is associating )
proof
take  vect M ; ::_thesis: ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating )
thus  ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating ) by Th21; ::_thesis: verum
end;
hence  ex w being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
( w is_atlas_of the carrier of M, vectgroup M & w is associating ) ; ::_thesis: verum
end;
end;
given G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr , w being Function of [: the carrier of M, the carrier of M:], the carrier of G such that A2: ( w is_atlas_of the carrier of M,G & w is associating ) ; ::_thesis: M is MidSp
thus  M is MidSp by A2, Th20; ::_thesis: verum
end;

definition
let M be non empty MidStr ;
attrc2 is strict ;
struct AtlasStr over M -> ;
aggrAtlasStr(# algebra, function #) ->  AtlasStr over M;
sel algebra c2 ->  non empty addLoopStr ;
sel function c2 ->  Function of [: the carrier of M, the carrier of M:], the carrier of the algebra of c2;
end;

definition
let M be non empty MidStr ;
let IT be AtlasStr over M;
attrIT is ATLAS-like  means :Def12: :: MIDSP_2:def 12
( the algebra of IT is midpoint_operator & the algebra of IT is add-associative & the algebra of IT is right_zeroed & the algebra of IT is right_complementable & the algebra of IT is Abelian & the function of IT is associating & the function of IT is_atlas_of the carrier of M, the algebra of IT );
end;

:: deftheorem Def12 defines ATLAS-like MIDSP_2:def_12_:_
 for M being non empty MidStr
for IT being AtlasStr over M holds
( IT is ATLAS-like iff ( the algebra of IT is midpoint_operator & the algebra of IT is add-associative & the algebra of IT is right_zeroed & the algebra of IT is right_complementable & the algebra of IT is Abelian & the function of IT is associating & the function of IT is_atlas_of the carrier of M, the algebra of IT ) );

registration
let M be MidSp;
cluster ATLAS-like for AtlasStr over M;
existence
 ex b1 being AtlasStr over M st b1 is ATLAS-like
proof
consider G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr , w being Function of [: the carrier of M, the carrier of M:], the carrier of G such that
A1: ( w is_atlas_of the carrier of M,G & w is associating ) by Th27;
take  AtlasStr(# G,w #) ; ::_thesis: AtlasStr(# G,w #) is ATLAS-like
thus  AtlasStr(# G,w #) is ATLAS-like by A1, Def12; ::_thesis: verum
end;
end;

definition
let M be MidSp;
mode ATLAS of M is ATLAS-like AtlasStr over M;
end;

definition
let M be non empty MidStr ;
let W be AtlasStr over M;
mode Vector of W is Element of the algebra of W;
end;

definition
let M be MidSp;
let W be AtlasStr over M;
let a, b be Point of M;
funcW . (a,b) ->  Element of the algebra of W equals :: MIDSP_2:def 13
 the function of W . (a,b);
coherence
 the function of W . (a,b) is Element of the algebra of W ;
end;

:: deftheorem  defines . MIDSP_2:def_13_:_
 for M being MidSp
for W being AtlasStr over M
for a, b being Point of M holds W . (a,b) = the function of W . (a,b);

definition
let M be MidSp;
let W be AtlasStr over M;
let a be Point of M;
let x be Vector of W;
func(a,x) . W ->  Point of M equals :: MIDSP_2:def 14
(a,x) . the function of W;
coherence
 (a,x) . the function of W is Point of M ;
end;

:: deftheorem  defines . MIDSP_2:def_14_:_
 for M being MidSp
for W being AtlasStr over M
for a being Point of M
for x being Vector of W holds (a,x) . W = (a,x) . the function of W;

definition
let M be MidSp;
let W be ATLAS of M;
func 0. W ->  Vector of W equals :: MIDSP_2:def 15
 0. the algebra of W;
coherence
 0. the algebra of W is Vector of W ;
end;

:: deftheorem  defines 0. MIDSP_2:def_15_:_
 for M being MidSp
for W being ATLAS of M holds 0. W = 0. the algebra of W;

theorem Th28: :: MIDSP_2:28
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
proof
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
let M be non empty MidStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: for a, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
let a, c, b1, b2 be Point of M; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; ::_thesis: ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )
A3: ( a @ c = b1 @ b2 iff w . (a,b2) = w . (b1,c) ) by A1, A2, Th13;
hence  ( a @ c = b1 @ b2 implies w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) by A1, Def3; ::_thesis: ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 )
 w . (a,c) = (w . (a,b1)) + (w . (b1,c)) by A1, Def3;
hence  ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 ) by A3, RLVECT_1:8; ::_thesis: verum
end;

theorem Th29: :: MIDSP_2:29
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
proof
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; ::_thesis: for M being non empty MidStr
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
let M be non empty MidStr ; ::_thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G
for a, c, b being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ::_thesis: for a, c, b being Point of M st w is_atlas_of the carrier of M,G & w is associating holds
( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
let a, c, b be Point of M; ::_thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ( a @ c = b iff w . (a,c) = Double (w . (a,b)) ) )
assume A1: ( w is_atlas_of the carrier of M,G & w is associating ) ; ::_thesis: ( a @ c = b iff w . (a,c) = Double (w . (a,b)) )
then reconsider MM = M as MidSp by Th20;
reconsider bb = b as Point of MM ;
 bb @ bb = bb by MIDSP_1:def_3;
hence  ( a @ c = b iff w . (a,c) = Double (w . (a,b)) ) by A1, Th28; ::_thesis: verum
end;


theorem :: MIDSP_2:30
for M being MidSp
for W being ATLAS of M
for a, c, b1, b2 being Point of M holds
( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )
proof
let M be MidSp; ::_thesis: for W being ATLAS of M
for a, c, b1, b2 being Point of M holds
( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )
let W be ATLAS of M; ::_thesis: for a, c, b1, b2 being Point of M holds
( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )
let a, c, b1, b2 be Point of M; ::_thesis: ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) )
set w = the function of W;
set G = the algebra of W;
A1: ( the algebra of W is midpoint_operator & the algebra of W is add-associative & the algebra of W is right_zeroed & the algebra of W is right_complementable & the algebra of W is Abelian ) by Def12;
 ( the function of W is_atlas_of the carrier of M, the algebra of W & the function of W is associating ) by Def12;
hence  ( a @ c = b1 @ b2 iff W . (a,c) = (W . (a,b1)) + (W . (a,b2)) ) by A1, Th28; ::_thesis: verum
end;

theorem :: MIDSP_2:31
for M being MidSp
for W being ATLAS of M
for a, c, b being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
proof
let M be MidSp; ::_thesis: for W being ATLAS of M
for a, c, b being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
let W be ATLAS of M; ::_thesis: for a, c, b being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
let a, c, b be Point of M; ::_thesis: ( a @ c = b iff W . (a,c) = Double (W . (a,b)) )
set w = the function of W;
set G = the algebra of W;
A1: ( the algebra of W is midpoint_operator & the algebra of W is add-associative & the algebra of W is right_zeroed & the algebra of W is right_complementable & the algebra of W is Abelian ) by Def12;
 ( the function of W is_atlas_of the carrier of M, the algebra of W & the function of W is associating ) by Def12;
hence  ( a @ c = b iff W . (a,c) = Double (W . (a,b)) ) by A1, Th29; ::_thesis: verum
end;

theorem :: MIDSP_2:32
for M being MidSp
for W being ATLAS of M holds
( ( for a being Point of M
for x being Vector of W ex b being Point of M st W . (a,b) = x ) & ( for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ) & ( for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c) ) )
proof
let M be MidSp; ::_thesis: for W being ATLAS of M holds
( ( for a being Point of M
for x being Vector of W ex b being Point of M st W . (a,b) = x ) & ( for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ) & ( for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c) ) )
let W be ATLAS of M; ::_thesis: ( ( for a being Point of M
for x being Vector of W ex b being Point of M st W . (a,b) = x ) & ( for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ) & ( for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c) ) )
set w = the function of W;
thus  for a being Point of M
for x being Vector of W ex b being Point of M st W . (a,b) = x ::_thesis: ( ( for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ) & ( for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c) ) )
proof
set w = the function of W;
let a be Point of M; ::_thesis: for x being Vector of W ex b being Point of M st W . (a,b) = x
let x be Vector of W; ::_thesis: ex b being Point of M st W . (a,b) = x
 the function of W is_atlas_of the carrier of M, the algebra of W by Def12;
then consider b being Point of M such that
A1: the function of W . (a,b) = x by Def3;
take  b ; ::_thesis: W . (a,b) = x
thus  W . (a,b) = x by A1; ::_thesis: verum
end;
thus  for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ::_thesis: for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c)
proof
set w = the function of W;
A2: the function of W is_atlas_of the carrier of M, the algebra of W by Def12;
let a, b, c be Point of M; ::_thesis: ( W . (a,b) = W . (a,c) implies b = c )
assume  W . (a,b) = W . (a,c) ; ::_thesis: b = c
hence  b = c by A2, Def3; ::_thesis: verum
end;
let a, b, c be Point of M; ::_thesis: (W . (a,b)) + (W . (b,c)) = W . (a,c)
 the function of W is_atlas_of the carrier of M, the algebra of W by Def12;
hence  (W . (a,b)) + (W . (b,c)) = W . (a,c) by Def3; ::_thesis: verum
end;

theorem Th33: :: MIDSP_2:33
for M being MidSp
for W being ATLAS of M
for a, b, c, d being Point of M
for x being Vector of W holds
( W . (a,a) = 0. W & ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
proof
let M be MidSp; ::_thesis: for W being ATLAS of M
for a, b, c, d being Point of M
for x being Vector of W holds
( W . (a,a) = 0. W & ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
let W be ATLAS of M; ::_thesis: for a, b, c, d being Point of M
for x being Vector of W holds
( W . (a,a) = 0. W & ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
let a, b, c, d be Point of M; ::_thesis: for x being Vector of W holds
( W . (a,a) = 0. W & ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
let x be Vector of W; ::_thesis: ( W . (a,a) = 0. W & ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
set w = the function of W;
set G = the algebra of W;
A1: the function of W is_atlas_of the carrier of M, the algebra of W by Def12;
A2: ( the algebra of W is midpoint_operator & the algebra of W is add-associative & the algebra of W is right_zeroed & the algebra of W is right_complementable & the algebra of W is Abelian ) by Def12;
hence  W . (a,a) = 0. W by A1, Th2; ::_thesis: ( ( W . (a,b) = 0. W implies a = b ) & W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  ( W . (a,b) = 0. W implies a = b ) by A2, A1, Th3; ::_thesis: ( W . (a,b) = - (W . (b,a)) & ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  W . (a,b) = - (W . (b,a)) by A2, A1, Th4; ::_thesis: ( ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) & ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) by A2, A1, Th5; ::_thesis: ( ( for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ) & ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  for b being Point of M
for x being Vector of W ex a being Point of M st W . (a,b) = x ::_thesis: ( ( W . (b,a) = W . (c,a) implies b = c ) & ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
proof
let b be Point of M; ::_thesis: for x being Vector of W ex a being Point of M st W . (a,b) = x
let x be Vector of W; ::_thesis: ex a being Point of M st W . (a,b) = x
consider a being Point of M such that
A3: the function of W . (a,b) = x by A2, A1, Th6;
take  a ; ::_thesis: W . (a,b) = x
thus  W . (a,b) = x by A3; ::_thesis: verum
end;
thus  ( W . (b,a) = W . (c,a) implies b = c ) by A2, A1, Th7; ::_thesis: ( ( a @ b = c implies W . (a,c) = W . (c,b) ) & ( W . (a,c) = W . (c,b) implies a @ b = c ) & ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
A4: the function of W is associating by Def12;
hence  ( a @ b = c iff W . (a,c) = W . (c,b) ) by Def2; ::_thesis: ( ( a @ b = c @ d implies W . (a,d) = W . (c,b) ) & ( W . (a,d) = W . (c,b) implies a @ b = c @ d ) & ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  ( a @ b = c @ d iff W . (a,d) = W . (c,b) ) by A2, A4, A1, Th13; ::_thesis: ( ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) )
thus  ( ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) ) by A1, Def4; ::_thesis: verum
end;

theorem :: MIDSP_2:34
for M being MidSp
for W being ATLAS of M
for a being Point of M holds (a,(0. W)) . W = a
proof
let M be MidSp; ::_thesis: for W being ATLAS of M
for a being Point of M holds (a,(0. W)) . W = a
let W be ATLAS of M; ::_thesis: for a being Point of M holds (a,(0. W)) . W = a
let a be Point of M; ::_thesis: (a,(0. W)) . W = a
 W . (a,a) = 0. W by Th33;
hence  (a,(0. W)) . W = a by Th33; ::_thesis: verum
end;