let x1, x2 be real-valued FinSequence; :: thesis: ( len x1 = len x2 implies |((- x1),(- x2))| = |(x1,x2)| )
assume A1: len x1 = len x2 ; :: thesis: |((- x1),(- x2))| = |(x1,x2)|
then len (- x2) = len x1 by Th144;
then |((- x1),(- x2))| = - |(x1,(- x2))| by Th152
.= - (- |(x1,x2)|) by A1, Th152 ;
hence |((- x1),(- x2))| = |(x1,x2)| ; :: thesis: verum