let M be non empty MidStr ; :: thesis: for G being non empty right_complementable Abelian 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
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
let G be non empty right_complementable Abelian 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
for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
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 for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) ) )
assume that
A1: w is_atlas_of the carrier of M,G and
A2: w is associating ; :: thesis: for a, b, c, d being Point of M holds
( a @ b = c @ d iff w . (a,d) = w . (c,b) )
let a, b, c, d be Point of M; :: thesis: ( a @ b = c @ d iff w . (a,d) = w . (c,b) )
thus ( a @ b = c @ d implies w . (a,d) = w . (c,b) ) :: thesis: ( w . (a,d) = w . (c,b) implies a @ b = c @ d )

proof

set p = a @ b;
assume a @ b = c @ d ; :: thesis: w . (a,d) = w . (c,b)
then A3: w . (c,(a @ b)) = w . ((a @ b),d) by A2;
w . (a,(a @ b)) = w . ((a @ b),b) by A2;
hence w . (a,d) = (w . (c,(a @ b))) + (w . ((a @ b),b)) by A1, A3
.= w . (c,b) by A1 ;
:: thesis: verum

end;

thus ( w . (a,d) = w . (c,b) implies a @ b = c @ d ) :: thesis: verum

proof

set p = a @ b;
assume A4: w . (a,d) = w . (c,b) ; :: thesis: a @ b = c @ d
(w . ((a @ b),b)) + (w . ((a @ b),d)) = (w . (a,(a @ b))) + (w . ((a @ b),d)) by A2
.= w . (a,d) by A1
.= (w . ((a @ b),b)) + (w . (c,(a @ b))) by A1, A4 ;
then w . ((a @ b),d) = w . (c,(a @ b)) by RLVECT_1:8;
hence a @ b = c @ d by A2; :: thesis: verum

end;