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