let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for M being non empty MidStr

for w being Function of [: the carrier of M, the carrier of M:], the carrier of G

for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let M be non empty MidStr ; :: thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G

for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let a, b1, b2, c be Point of M; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) )

assume that

A1: w is_atlas_of the carrier of M,G and

A2: w is associating ; :: thesis: ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

A3: ( a @ c = b1 @ b2 iff w . (a,b2) = w . (b1,c) ) by A1, A2, Th13;

hence ( a @ c = b1 @ b2 implies w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) by A1; :: thesis: ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 )

w . (a,c) = (w . (a,b1)) + (w . (b1,c)) by A1;

hence ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 ) by A3, RLVECT_1:8; :: thesis: verum

for w being Function of [: the carrier of M, the carrier of M:], the carrier of G

for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let M be non empty MidStr ; :: thesis: for w being Function of [: the carrier of M, the carrier of M:], the carrier of G

for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: for a, b1, b2, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

let a, b1, b2, c be Point of M; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) )

assume that

A1: w is_atlas_of the carrier of M,G and

A2: w is associating ; :: thesis: ( a @ c = b1 @ b2 iff w . (a,c) = (w . (a,b1)) + (w . (a,b2)) )

A3: ( a @ c = b1 @ b2 iff w . (a,b2) = w . (b1,c) ) by A1, A2, Th13;

hence ( a @ c = b1 @ b2 implies w . (a,c) = (w . (a,b1)) + (w . (a,b2)) ) by A1; :: thesis: ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 )

w . (a,c) = (w . (a,b1)) + (w . (b1,c)) by A1;

hence ( w . (a,c) = (w . (a,b1)) + (w . (a,b2)) implies a @ c = b1 @ b2 ) by A3, RLVECT_1:8; :: thesis: verum