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, Th4

.= w . (d,c) by A1, Th4 ; :: thesis: verum

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, Th4

.= w . (d,c) by A1, Th4 ; :: thesis: verum