let p be Tuple of 1, REAL ; :: thesis: - p is Tuple of 1, REAL
consider d being Element of REAL such that
A1: p = <*d*> by FINSEQ_2:97;
- p = <*(- d)*> by A1, RVSUM_1:20;
hence - p is Tuple of 1, REAL ; :: thesis: verum