let S be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( w is_atlas_of S,G implies w . a,b = - (w . b,a) )
assume A1: w is_atlas_of S,G ; :: thesis: w . a,b = - (w . b,a)
then (w . b,a) + (w . a,b) = w . b,b by Def3
.= 0. G by A1, Th4 ;
then - (w . b,a) = - (- (w . a,b)) by RLVECT_1:19;
hence w . a,b = - (w . b,a) by RLVECT_1:30; :: thesis: verum