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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w implies ex r being Point of M st r @ p = q )
assume A1: ( w is_atlas_of the carrier of M,G & M,G are_associated_wrp w ) ; :: thesis: ex r being Point of M st r @ p = q
then consider r being Point of M such that
A2: w . r,q = w . q,p by Th8;
take r ; :: thesis: r @ p = q
thus r @ p = q by A1, A2, Def2; :: thesis: verum