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 Th28, Th32;
then A2: Padd (o,a9,(Pcom (o,a9))) = o by Def5;
a + aa = (Padd o) . (a,(Pcom (o,a9))) by Def7
.= 0. (GroupVect (AFV,o)) by A1, A2, Def6 ;
hence - a = (Pcom o) . a9 by RLVECT_1:def 10; :: thesis: verum