let M be non empty MidStr ; :: thesis:

hereby :: thesis:

assume A1: M is MidSp ; :: thesis:
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:

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 )

take vect M ; :: thesis:
thus ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating ) by Th21; :: thesis:

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:

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:
thus M is MidSp by A2, Th20; :: thesis: