let x1, x2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 implies |((- x1),x2)| = - |(x1,x2)| )
assume len x1 = len x2 ; :: thesis: |((- x1),x2)| = - |(x1,x2)|
then |((- x1),x2)| = (- 1) * |(x1,x2)| by Th20;
hence |((- x1),x2)| = - |(x1,x2)| ; :: thesis: verum