let a be Element of COMPLEX ; 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 ; ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
assume A1:
len x = len y
; |((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:147;
A3:
( len ((Re a) * (Re x)) = len (Re x) & len ((Im a) * (Im x)) = len (Im x) )
by RVSUM_1:147;
A4:
len (Re x) = len x
by Th48;
A5:
len (Im y) = len y
by Th48;
A6:
len (Re y) = len y
by Th48;
A7:
len (Im x) = len x
by Th48;
|((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, A4, A6, A7, A3, RVSUM_1:154
.=
(((|(((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, A4, A7, A5, A3, RVSUM_1:154
.=
(((|(((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, A4, A6, A7, A2, RVSUM_1:150
.=
(((|(((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, A7, A5, A2, RVSUM_1:150
.=
(((|(((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, RVSUM_1:151
.=
(((|(((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, A7, A5, RVSUM_1:151
.=
(((((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, A6, RVSUM_1:151
.=
(((((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, A6, A7, RVSUM_1:151
.=
(((((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, A6, RVSUM_1:151
.=
(((((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, A6, A7, RVSUM_1:151
.=
(((((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, RVSUM_1:151
.=
(((((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, A7, A5, RVSUM_1:151
.=
((((((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)|
; verum