let AFV be WeakAffVect; :: thesis: for o being Element of
for a being Element of holds a + (0. (GroupVect AFV,o)) = a
let o be Element of ; :: thesis: for a being Element of holds a + (0. (GroupVect AFV,o)) = a
let a be Element of ; :: thesis: a + (0. (GroupVect AFV,o)) = a
reconsider a' = a as Element of ;
reconsider x' = a + (0. (GroupVect AFV,o)) as Element of ;
x' = Padd o,a',o by Def7;
then o,a' // o,x' by Def5;
hence a + (0. (GroupVect AFV,o)) = a by Th5; :: thesis: verum