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

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
set w = the function of W;
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

let a, b, c be Point of M; :: thesis: ( W . a,b = W . a,c implies b = c )
assume A2: W . a,b = W . a,c ; :: thesis: b = c
set w = the function of W;
the function of W is_atlas_of the carrier of M,the algebra of W by Def12;
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
set w = the function of W;
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