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