theorem :: PRVECT_3:10

for G, F being non empty right_complementable add-associative right_zeroed RLSStruct
for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]