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 5 :: 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 6 :: 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 7 :: thesis: verum