let M be MidSp; :: thesis:
let W be ATLAS of M; :: thesis:
let a, b, c, d be Point of M; :: thesis:
let x be Vector of W; :: thesis:
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:
thus ( W . (a,b) = 0. W implies a = b ) by A2, A1, Th3; :: thesis:
thus W . (a,b) = - (W . (b,a)) by A2, A1, Th4; :: thesis:
thus ( W . (a,b) = W . (c,d) implies W . (b,a) = W . (d,c) ) by A2, A1, Th5; :: thesis:
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:

let b be Point of M; :: thesis:
let x be Vector of W; :: thesis:
consider a being Point of M such that
A3: the function of W . (a,b) = x by A2, A1, Th6;
take a ; :: thesis:
thus W . (a,b) = x by A3; :: thesis:

end;

thus ( W . (b,a) = W . (c,a) implies b = c ) by A2, A1, Th7; :: thesis:
A4: the function of W is associating by Def12;
hence ( a @ b = c iff W . (a,c) = W . (c,b) ) ; :: thesis:
thus ( a @ b = c @ d iff W . (a,d) = W . (c,b) ) by A2, A4, A1, Th13; :: thesis:
thus ( ( W . (a,b) = x implies (a,x) . W = b ) & ( (a,x) . W = b implies W . (a,b) = x ) ) by A1, Def4; :: thesis: