let S be non empty set ; 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 ; 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; ( 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
; 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; ( (@ 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; ( w . (a,c) = w . (c,b) implies (@ w) . (a,b) = c )
thus
( w . (a,c) = w . (c,b) implies (@ w) . (a,b) = c )
verumproof
defpred S1[
Element of
S,
Element of
S,
Element of
S]
means w . ($1,$3)
= w . ($3,$2);
assume A2:
w . (
a,
c)
= w . (
c,
b)
;
(@ w) . (a,b) = c
A3:
for
a,
b,
c,
c9 being
Element of
S st
S1[
a,
b,
c] &
S1[
a,
b,
c9] holds
c = c9
proof
let a,
b,
c,
c9 be
Element of
S;
( S1[a,b,c] & S1[a,b,c9] implies c = c9 )
assume A4:
(
S1[
a,
b,
c] &
S1[
a,
b,
c9] )
;
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;
verum
end;
set c9 =
(@ w) . (
a,
b);
S1[
a,
b,
(@ w) . (
a,
b)]
by A1, Def9;
hence
(@ w) . (
a,
b)
= c
by A2, A3;
verum
end;