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 ;
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; :: 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) ; :: thesis: verum