let M be non empty MidStr ; 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; 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 ; 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; ( 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
; 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
; r @ p = q
thus
r @ p = q
by A2, A3; verum