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 x) = len x by Th48;
A3: len (Re y) = len y by Th48;
A4: len (Im x) = len x by Th48;
A5: len (Im y) = len y by Th48;
A6: len ((Re a) * (Re x)) = len (Re x) by EUCLID_2:8;
A7: len ((Im a) * (Im x)) = len (Im x) by EUCLID_2:8;
A8: len ((Re a) * (Im x)) = len (Im x) by EUCLID_2:8;
A9: len ((Im a) * (Re x)) = len (Re x) by EUCLID_2:8;
|((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 Th65
.= ((|((((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 Th65
.= ((|((((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 Th65
.= ((|((((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 Th65
.= (((|(((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 A1, A2, A3, A4, A6, A7, EUCLID_2:25
.= (((|(((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 A1, A2, A4, A5, A6, A7, EUCLID_2:25
.= (((|(((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 A1, A2, A3, A4, A8, A9, EUCLID_2:19
.= (((|(((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 A1, A2, A4, A5, A8, A9, EUCLID_2:19
.= (((|(((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 A1, A2, A5, EUCLID_2:20
.= (((|(((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 A1, A4, A5, EUCLID_2:20
.= (((((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 A1, A2, A3, EUCLID_2:20
.= (((((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 A1, A3, A4, EUCLID_2:20
.= (((((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 A1, A2, A3, EUCLID_2:20
.= (((((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 A1, A3, A4, EUCLID_2:20
.= (((((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 A1, A2, A5, EUCLID_2:20
.= (((((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 A1, A4, A5, EUCLID_2:20
.= ((((((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:29
.= (((((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:29
.= (((((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:29
.= (((a * |((Re x),(Re y))|) - (a * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:29
.= a * |(x,y)| ;
hence |((a * x),y)| = a * |(x,y)| ; :: thesis: verum