let AFV be WeakAffVect; :: thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
let o be Element of AFV; :: thesis: for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
let a be Element of (GroupVect (AFV,o)); :: thesis: ex b being Element of (GroupVect (AFV,o)) st b + b = a
reconsider a99 = a as Element of AFV ;
consider b9 being Element of AFV such that
A1: o,b9 // b9,a99 by Def1;
reconsider b = b9 as Element of (GroupVect (AFV,o)) ;
a99 = Padd (o,b9,b9) by A1, Def5
.= b + b by Def6 ;
hence ex b being Element of (GroupVect (AFV,o)) st b + b = a ; :: thesis: verum