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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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 & M,G are_associated_wrp w 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: M,G are_associated_wrp w ; :: 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, Def2;
w . a,(a @ b) = w . (a @ b),b by A2, Def2;
hence w . a,d = (w . c,(a @ b)) + (w . (a @ b),b) by A1, A3, Def3
.= w . c,b by A1, Def3 ;
:: 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, Def2
.= w . a,d by A1, Def3
.= (w . (a @ b),b) + (w . c,(a @ b)) by A1, A4, Def3 ;
then w . (a @ b),d = w . c,(a @ b) by RLVECT_1:21;
hence a @ b = c @ d by A2, Def2; :: thesis: verum

end;