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 (vectgroup M) 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 (vectgroup M) 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 (vectgroup M) 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 A2, Th20; :: thesis: verum