let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; 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 ; 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; 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; ( 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
; ( 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; ( 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; verum