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 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;
A2: ( M,the algebra of W are_associated_wrp the function of W & the function of W is_atlas_of the carrier of M,the algebra of W ) by Def12;
hence W . a,a = 0. W by A1, Th4; :: 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 A1, A2, Th5; :: 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 A1, A2, Th6; :: 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 A1, A2, Th7; :: 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 A1, A2, Th8;
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 A1, A2, Th9; :: 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 ) )
thus ( a @ b = c iff W . a,c = W . c,b ) by A2, 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 A1, A2, Th16; :: 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 A2, Def4; :: thesis: verum