let S be non empty set ; :: thesis: for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:],the carrier of G st w is_atlas_of S,G holds
for a, b, c being Element of S holds
( (@ w) . a,b = c iff w . a,c = w . c,b )
let G be non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr ; :: thesis: for w being Function of [:S,S:],the carrier of G st w is_atlas_of S,G holds
for a, b, c being Element of S holds
( (@ w) . a,b = c iff w . a,c = w . c,b )
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G implies for a, b, c being Element of S holds
( (@ w) . a,b = c iff w . a,c = w . c,b ) )
assume A1: w is_atlas_of S,G ; :: thesis: for a, b, c being Element of S holds
( (@ w) . a,b = c iff w . a,c = w . c,b )
let a, b, c be Element of S; :: thesis: ( (@ w) . a,b = c iff w . a,c = w . c,b )
thus ( (@ w) . a,b = c implies w . a,c = w . c,b ) by A1, Def9; :: thesis: ( w . a,c = w . c,b implies (@ w) . a,b = c )
thus ( w . a,c = w . c,b implies (@ w) . a,b = c ) :: thesis: verum

proof

assume A2: w . a,c = w . c,b ; :: thesis: (@ w) . a,b = c
defpred S₁[ Element of S, Element of S, Element of S] means w . $1,$3 = w . $3,$2;
A3: for a, b, c, c' being Element of S st S₁[a,b,c] & S₁[a,b,c'] holds
c = c'

proof

let a, b, c, c' be Element of S; :: thesis: ( S₁[a,b,c] & S₁[a,b,c'] implies c = c' )
assume that
A4: S₁[a,b,c] and
A5: S₁[a,b,c'] ; :: thesis: c = c'
w . c,c' = (w . c,a) + (w . a,c') by A1, Def3
.= (w . c',b) + (w . b,c) by A1, A4, A5, Th7
.= w . c',c by A1, Def3
.= - (w . c,c') by A1, Th6 ;
then w . c,c' = 0. G by Th19;
hence c = c' by A1, Th5; :: thesis: verum

end;

set c' = (@ w) . a,b;
S₁[a,b,(@ w) . a,b] by A1, Def9;
hence (@ w) . a,b = c by A2, A3; :: thesis: verum

end;