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