let M be non empty MidStr ; :: thesis: ( M is MidSp iff ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) )

hereby :: thesis: ( ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) implies M is MidSp )
assume A1: M is MidSp ; :: thesis: ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating )

thus ex G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ex w being Function of [: the carrier of M, the carrier of M:], the carrier of G st
( w is_atlas_of the carrier of M,G & w is associating ) :: thesis: verum
proof
reconsider M = M as MidSp by A1;
set G = vectgroup M;
take vectgroup M ; :: thesis: ex w being Function of [: the carrier of M, the carrier of M:], the carrier of () st
( w is_atlas_of the carrier of M, vectgroup M & w is associating )

ex w being Function of [: the carrier of M, the carrier of M:], the carrier of () st
( w is_atlas_of the carrier of M, vectgroup M & w is associating )
proof
take vect M ; :: thesis: ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating )
thus ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating ) by Th21; :: thesis: verum
end;
hence ex w being Function of [: the carrier of M, the carrier of M:], the carrier of () st
( w is_atlas_of the carrier of M, vectgroup M & w is associating ) ; :: thesis: verum
end;
end;
given G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr , w being Function of [: the carrier of M, the carrier of M:], the carrier of G such that A2: ( w is_atlas_of the carrier of M,G & w is associating ) ; :: thesis: M is MidSp
thus M is MidSp by ; :: thesis: verum