let x, y be real-valued FinSequence; :: thesis: for a being real number st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let a be real number ; :: thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
reconsider a2 = a as Element of REAL by XREAL_0:def 1;
A0: ( x is FinSequence of REAL & y is FinSequence of REAL ) by Lm4;
assume len x = len y ; :: thesis: |((a * x),y)| = a * |(x,y)|
then reconsider x2 = x, y2 = y as Element of (len x) -tuples_on REAL by A0, FINSEQ_2:110;
|((a * x),y)| = Sum (a2 * (mlt (x2,y2))) by FINSEQOP:27
.= a * |(x,y)| by Th117 ;
hence |((a * x),y)| = a * |(x,y)| ; :: thesis: verum