let AFV be WeakAffVect; :: thesis: for o being Element of AFV
for a being Element of (GroupVect AFV,o)
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let o be Element of AFV; :: thesis: for a being Element of (GroupVect AFV,o)
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a be Element of (GroupVect AFV,o); :: thesis: for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
let a9 be Element of AFV; :: thesis: ( a = a9 implies - a = (Pcom o) . a9 )
assume A1: a = a9 ; :: thesis: - a = (Pcom o) . a9
reconsider aa = (Pcom o) . a9 as Element of (GroupVect AFV,o) ;
( Pcom o,o = o & o,a9 // Pcom o,a9, Pcom o,o ) by Th35, Th39;
then A2: Padd o,a9,(Pcom o,a9) = o by Def5;
a + aa = (Padd o) . a,(Pcom o,a9) by Def8
.= 0. (GroupVect AFV,o) by A1, A2, Def7 ;
hence - a = (Pcom o) . a9 by RLVECT_1:def 13; :: thesis: verum