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

b = c :: thesis: for a, b, c being Point of M holds (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

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

thus
for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
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;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

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

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