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 & M,G are_associated_wrp w ) )

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 & M,G are_associated_wrp w ) 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 & M,G are_associated_wrp w )
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 & M,G are_associated_wrp w ) :: thesis: verum

proof

reconsider M = M as MidSp by A1;
set G = vectgroup M;
A2: 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 & M, vectgroup M are_associated_wrp w )

proof

take vect M ; :: thesis: ( vect M is_atlas_of the carrier of M, vectgroup M & M, vectgroup M are_associated_wrp vect M )
thus ( vect M is_atlas_of the carrier of M, vectgroup M & M, vectgroup M are_associated_wrp vect M ) by Th24, Th27; :: thesis: verum

end;

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 & M, vectgroup M are_associated_wrp w )
thus 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 & M, vectgroup M are_associated_wrp w ) by A2; :: 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 A3: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w ) ; :: thesis: M is MidSp
thus M is MidSp by A3, Th23; :: thesis: verum