let AFV be WeakAffVect; :: thesis: for o being Element of AFV holds
( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
let o be Element of AFV; :: thesis: ( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
thus for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a by Lm2; :: according to RLVECT_1:def 2 :: thesis: ( GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
thus for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c) by Lm3; :: according to RLVECT_1:def 3 :: thesis: GroupVect (AFV,o) is right_zeroed
thus for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a by Lm4; :: according to RLVECT_1:def 4 :: thesis: verum