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