let x1, x2 be real-valued FinSequence; :: 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 Th121;
hence |((- x1),x2)| = - |(x1,x2)| ; :: thesis: verum