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 Th28;
then o,s9 // Pcom (o,s9),o by Th32;
then A1: Padd (o,s9,(Pcom (o,s9))) = o by Def5;
thus s + t = (Padd o) . (s9,(Pcom (o,s9))) by Def7
.= 0. (GroupVect (AFV,o)) by A1, Def6 ; :: thesis: verum