let x, y be FinSequence of COMPLEX ; ( len x = len y implies |((<i> * x),y)| = <i> * |(x,y)| )
assume A1:
len x = len y
; |((<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 A1, A3, A4, RVSUM_1:122
.=
(((- |((Im x),(Re y))|) - (<i> * (- |((Im x),(Im y))|))) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))|
by A1, A4, A2, RVSUM_1:122
.=
<i> * |(x,y)|
;
hence
|((<i> * x),y)| = <i> * |(x,y)|
; verum