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)|
A2: len (<i> * x1) = len x1 by Th3;
|((- x1),x2)| = |(((<i> * <i>) * x1),x2)|
.= |((<i> * (<i> * x1)),x2)| by Th44
.= <i> * |((<i> * x1),x2)| by A1, A2, Th49
.= <i> * (<i> * |(x1,x2)|) by A1, Th49
.= (- 1) * |(x1,x2)| ;
hence |((- x1),x2)| = - |(x1,x2)| ; :: thesis: verum