let S be non empty set ; for a, b being Element of S
for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let a, b be Element of S; for G being non empty right_complementable add-associative right_zeroed addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let G be non empty right_complementable add-associative right_zeroed addLoopStr ; for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
w . (a,b) = - (w . (b,a))
let w be Function of [:S,S:], the carrier of G; ( w is_atlas_of S,G implies w . (a,b) = - (w . (b,a)) )
assume A1:
w is_atlas_of S,G
; w . (a,b) = - (w . (b,a))
then (w . (b,a)) + (w . (a,b)) =
w . (b,b)
.=
0. G
by A1, Th2
;
then
- (w . (b,a)) = - (- (w . (a,b)))
by RLVECT_1:6;
hence
w . (a,b) = - (w . (b,a))
by RLVECT_1:17; verum