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 (Re y) = len y by Th48;
A3: len (Im x) = len x by Th48;
A4: len (Im y) = len y by Th48;
|((<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 Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Im (<i> * x)),(Re y))|)) + |((Im (<i> * x)),(Im y))| by Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Im (<i> * x)),(Im y))| by Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by Th58
.= (((- |((Im x),(Re y))|) - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by A1, A2, A3, EUCLID_2:22
.= (((- |((Im x),(Re y))|) - (<i> * (- |((Im x),(Im y))|))) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by A1, A3, A4, EUCLID_2:22
.= <i> * |(x,y)| ;
hence |((<i> * x),y)| = <i> * |(x,y)| ; :: thesis: verum