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