let AFV be WeakAffVect; :: thesis: for o being Element of AFV holds GroupVect AFV,o is right_complementable
let o be Element of AFV; :: thesis: GroupVect AFV,o is right_complementable
let s be Element of (GroupVect AFV,o); :: according to ALGSTR_0:def 16 :: thesis: s is right_complementable
reconsider s9 = s as Element of AFV ;
reconsider t = (Pcom o) . s9 as Element of (GroupVect AFV,o) ;
take t ; :: according to ALGSTR_0:def 11 :: thesis: s + t = 0. (GroupVect AFV,o)
Pcom o,o = o by Th35;
then o,s9 // Pcom o,s9,o by Th39;
then A1: Padd o,s9,(Pcom o,s9) = o by Def5;
thus s + t = (Padd o) . s9,(Pcom o,s9) by Def8
.= 0. (GroupVect AFV,o) by A1, Def7 ; :: thesis: verum