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
p @ q = q @ p
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
p @ q = q @ p
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
p @ q = q @ p
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 p @ q = q @ p )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: M,G are_associated_wrp w ; :: thesis: p @ q = q @ p
set r = p @ q;
w . (p,(p @ q)) = w . ((p @ q),q) by A2, Def2;
then w . ((p @ q),p) = w . (q,(p @ q)) by A1, Th7;
hence p @ q = q @ p by A2, Def2; :: thesis: verum