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, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating 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, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating 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, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b iff w . (a,c) = Double (w . (a,b)) )

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

assume A1: ( w is_atlas_of the carrier of M,G & w is associating ) ; :: thesis: ( a @ c = b iff w . (a,c) = Double (w . (a,b)) )

then reconsider MM = M as MidSp by Th20;

reconsider bb = b as Point of MM ;

bb @ bb = bb by MIDSP_1:def 3;

hence ( a @ c = b iff w . (a,c) = Double (w . (a,b)) ) by A1, Th27; :: thesis: verum

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

for a, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating 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, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating 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, b, c being Point of M st w is_atlas_of the carrier of M,G & w is associating holds

( a @ c = b iff w . (a,c) = Double (w . (a,b)) )

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

assume A1: ( w is_atlas_of the carrier of M,G & w is associating ) ; :: thesis: ( a @ c = b iff w . (a,c) = Double (w . (a,b)) )

then reconsider MM = M as MidSp by Th20;

reconsider bb = b as Point of MM ;

bb @ bb = bb by MIDSP_1:def 3;

hence ( a @ c = b iff w . (a,c) = Double (w . (a,b)) ) by A1, Th27; :: thesis: verum