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

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

defpred S_{1}[ Element of S, Element of S, Element of S] means w . ($1,$3) = w . ($3,$2);

assume A2: w . (a,c) = w . (c,b) ; :: thesis: (@ w) . (a,b) = c

A3: for a, b, c, c9 being Element of S st S_{1}[a,b,c] & S_{1}[a,b,c9] holds

c = c9

S_{1}[a,b,(@ w) . (a,b)]
by A1, Def9;

hence (@ w) . (a,b) = c by A2, A3; :: thesis: verum

end;assume A2: w . (a,c) = w . (c,b) ; :: thesis: (@ w) . (a,b) = c

A3: for a, b, c, c9 being Element of S st S

c = c9

proof

set c9 = (@ w) . (a,b);
let a, b, c, c9 be Element of S; :: thesis: ( S_{1}[a,b,c] & S_{1}[a,b,c9] implies c = c9 )

assume A4: ( S_{1}[a,b,c] & S_{1}[a,b,c9] )
; :: thesis: c = c9

w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1

.= (w . (c9,b)) + (w . (b,c)) by A1, A4, Th5

.= w . (c9,c) by A1

.= - (w . (c,c9)) by A1, Th4 ;

then w . (c,c9) = 0. G by Th16;

hence c = c9 by A1, Th3; :: thesis: verum

end;assume A4: ( S

w . (c,c9) = (w . (c,a)) + (w . (a,c9)) by A1

.= (w . (c9,b)) + (w . (b,c)) by A1, A4, Th5

.= w . (c9,c) by A1

.= - (w . (c,c9)) by A1, Th4 ;

then w . (c,c9) = 0. G by Th16;

hence c = c9 by A1, Th3; :: thesis: verum

S

hence (@ w) . (a,b) = c by A2, A3; :: thesis: verum