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 ) )

A4: the function of W is associating by Def12;

hence ( a @ b = c iff W . (a,c) = W . (c,b) ) ; :: 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

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

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 ) )
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;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

A4: the function of W is associating by Def12;

hence ( a @ b = c iff W . (a,c) = W . (c,b) ) ; :: 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