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, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w 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, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w 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, c, b1, b2 being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
( a @ c = b1 @ b2 iff w . a,c = (w . a,b1) + (w . a,b2) )
let a, c, b1, b2 be Point of M; :: thesis: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w 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: M,G are_associated_wrp w ; :: 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, Th16;
A4: w . a,c = (w . a,b1) + (w . b1,c) by A1, Def3;
thus ( a @ c = b1 @ b2 implies w . a,c = (w . a,b1) + (w . a,b2) ) by A1, A3, Def3; :: thesis: ( w . a,c = (w . a,b1) + (w . a,b2) implies a @ c = b1 @ b2 )
thus ( w . a,c = (w . a,b1) + (w . a,b2) implies a @ c = b1 @ b2 ) by A3, A4, RLVECT_1:21; :: thesis: verum