let x1, x2 be FinSequence of COMPLEX ; :: 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 Th5;
then |((- x1),(- x2))| = - |(x1,(- x2))| by Th56
.= - (- |(x1,x2)|) by A1, Th57 ;
hence |((- x1),(- x2))| = |(x1,x2)| ; :: thesis: verum