let p be Element of REAL 3; :: thesis: len (- p) = len p
A1: len p = 3 by Th42;
- p = |[((- p) . 1),((- p) . 2),((- p) . 3)]| by Th1;
hence len (- p) = len p by A1, FINSEQ_1:45; :: thesis: verum