let p be Element of REAL 3; :: thesis: len (- p) = len p
A2: len p = 3 by Th35;
- p = |[((- p) . 1),((- p) . 2),((- p) . 3)]| by Lm1;
hence len (- p) = len p by A2, FINSEQ_1:62; :: thesis: verum