let S be non empty set ; :: thesis: for a, b, c, d 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 & w . a,b = w . c,d holds
w . b,a = w . d,c
let a, b, c, d 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 & w . a,b = w . c,d holds
w . b,a = w . d,c
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 & w . a,b = w . c,d holds
w . b,a = w . d,c
let w be Function of [:S,S:],the carrier of G; :: thesis: ( w is_atlas_of S,G & w . a,b = w . c,d implies w . b,a = w . d,c )
assume that
A1: w is_atlas_of S,G and
A2: w . a,b = w . c,d ; :: thesis: w . b,a = w . d,c
thus w . b,a = - (w . c,d) by A1, A2, Th6
.= w . d,c by A1, Th6 ; :: thesis: verum