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 ) )

thus M is MidSp by A2, Th20; :: thesis: verum

( 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 )

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( 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

end;( 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 )

( w is_atlas_of the carrier of M, vectgroup M & w is associating ) ; :: thesis: verum

end;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

hence
ex w being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) st
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;thus ( vect M is_atlas_of the carrier of M, vectgroup M & vect M is associating ) by Th21; :: thesis: verum

( w is_atlas_of the carrier of M, vectgroup M & w is associating ) ; :: thesis: verum

thus M is MidSp by A2, Th20; :: thesis: verum