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