let M be non empty MidStr ; :: thesis: for p, q being Point of M

for G being non empty right_complementable add-associative right_zeroed addLoopStr

for 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 holds

ex r being Point of M st r @ p = q

let p, q be Point of M; :: thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr

for 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 holds

ex r being Point of M st r @ p = q

let G be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for 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 holds

ex r being Point of M st r @ p = q

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ex r being Point of M st r @ p = q )

assume that

A1: w is_atlas_of the carrier of M,G and

A2: w is associating ; :: thesis: ex r being Point of M st r @ p = q

consider r being Point of M such that

A3: w . (r,q) = w . (q,p) by A1, Th6;

take r ; :: thesis: r @ p = q

thus r @ p = q by A2, A3; :: thesis: verum

for G being non empty right_complementable add-associative right_zeroed addLoopStr

for 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 holds

ex r being Point of M st r @ p = q

let p, q be Point of M; :: thesis: for G being non empty right_complementable add-associative right_zeroed addLoopStr

for 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 holds

ex r being Point of M st r @ p = q

let G be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for 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 holds

ex r being Point of M st r @ p = q

let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: ( w is_atlas_of the carrier of M,G & w is associating implies ex r being Point of M st r @ p = q )

assume that

A1: w is_atlas_of the carrier of M,G and

A2: w is associating ; :: thesis: ex r being Point of M st r @ p = q

consider r being Point of M such that

A3: w . (r,q) = w . (q,p) by A1, Th6;

take r ; :: thesis: r @ p = q

thus r @ p = q by A2, A3; :: thesis: verum