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, b being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
( a @ c = b iff w . a,c = Double (w . a,b) )
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, b being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
( a @ c = b iff w . a,c = Double (w . a,b) )
let w be Function of [:the carrier of M,the carrier of M:],the carrier of G; :: thesis: for a, c, b being Point of M st w is_atlas_of the carrier of M,G & M,G are_associated_wrp w holds
( a @ c = b iff w . a,c = Double (w . a,b) )
let a, c, b be Point of M; :: thesis: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w implies ( a @ c = b iff w . a,c = Double (w . a,b) ) )
assume A1: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w ) ; :: thesis: ( a @ c = b iff w . a,c = Double (w . a,b) )
then reconsider MM = M as MidSp by Th23;
reconsider bb = b as Point of MM ;
bb @ bb = bb by MIDSP_1:def 4;
hence ( a @ c = b iff w . a,c = Double (w . a,b) ) by A1, Th34; :: thesis: verum