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