let S be non empty set ; :: thesis: for a 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,a) = 0. G

let a 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,a) = 0. G

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,a) = 0. G

let w be Function of [:S,S:], the carrier of G; :: thesis: ( w is_atlas_of S,G implies w . (a,a) = 0. G )

assume w is_atlas_of S,G ; :: thesis: w . (a,a) = 0. G

then (w . (a,a)) + (w . (a,a)) = w . (a,a) ;

hence w . (a,a) = 0. G by RLVECT_1:9; :: 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 holds

w . (a,a) = 0. G

let a 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,a) = 0. G

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,a) = 0. G

let w be Function of [:S,S:], the carrier of G; :: thesis: ( w is_atlas_of S,G implies w . (a,a) = 0. G )

assume w is_atlas_of S,G ; :: thesis: w . (a,a) = 0. G

then (w . (a,a)) + (w . (a,a)) = w . (a,a) ;

hence w . (a,a) = 0. G by RLVECT_1:9; :: thesis: verum