let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |(x,(<i> * y))| = - (<i> * |(x,y)|) )
assume A1: len x = len y ; :: thesis: |(x,(<i> * y))| = - (<i> * |(x,y)|)
A2: len (Im x) = len x by Th40;
A3: len (Re x) = len x by Th40;
A4: len (Im y) = len y by Th40;
|(x,(<i> * y))| = ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Im (<i> * y)))|)) + (<i> * |((Im x),(Re (<i> * y)))|)) + |((Im x),(Im (<i> * y)))| by Th48
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(Re (<i> * y)))|)) + |((Im x),(Im (<i> * y)))| by Th48
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Im (<i> * y)))| by Th48
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Re y))| by Th48
.= (((- |((Re x),(Im y))|) - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Re y))| by A1, A3, A4, RVSUM_1:122
.= (((- |((Re x),(Im y))|) - (<i> * |((Re x),(Re y))|)) + (<i> * (- |((Im x),(Im y))|))) + |((Im x),(Re y))| by A1, A2, A4, RVSUM_1:122
.= - (<i> * |(x,y)|) ;
hence |(x,(<i> * y))| = - (<i> * |(x,y)|) ; :: thesis: verum