let a be Element of COMPLEX ; :: thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
|((a * x),y)| = a * |(x,y)|

let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
assume A1: len x = len y ; :: thesis: |((a * x),y)| = a * |(x,y)|
A2: ( len ((Re a) * (Im x)) = len (Im x) & len ((Im a) * (Re x)) = len (Re x) ) by RVSUM_1:117;
A3: ( len ((Re a) * (Re x)) = len (Re x) & len ((Im a) * (Im x)) = len (Im x) ) by RVSUM_1:117;
A4: len (Re x) = len x by Th40;
A5: len (Im y) = len y by Th40;
A6: len (Re y) = len y by Th40;
A7: len (Im x) = len x by Th40;
|((a * x),y)| = ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((Re (a * x)),(Im y))|)) + (<i> * |((Im (a * x)),(Re y))|)) + |((Im (a * x)),(Im y))| by Th54
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((Im (a * x)),(Re y))|)) + |((Im (a * x)),(Im y))| by Th54
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((Im (a * x)),(Im y))| by Th54
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by Th54
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (((Im a) * |((Re x),(Im y))|) + |(((Re a) * (Im x)),(Im y))|) by
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (((Im a) * |((Re x),(Im y))|) + ((Re a) * |((Im x),(Im y))|)) by
.= ((((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) * <i>) * |((Re x),(Im y))|)) + ((Im a) * |((Re x),(Im y))|)) + (((Re a) * (<i> * |((Im x),(Re y))|)) - ((Im a) * |((Im x),(Re y))|))) + (((Re a) + (<i> * (Im a))) * |((Im x),(Im y))|)
.= ((((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) * <i>) * |((Re x),(Im y))|)) + ((Im a) * |((Re x),(Im y))|)) + (((Re a) + (<i> * (Im a))) * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) + (<i> * (Im a))) * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((((Re a) + (<i> * (Im a))) * |((Re x),(Re y))|) - (a * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((a * |((Re x),(Re y))|) - (a * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= a * |(x,y)| ;
hence |((a * x),y)| = a * |(x,y)| ; :: thesis: verum