let x, y be real-valued FinSequence; :: thesis: for a being Real st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let a be Real; :: thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
reconsider a2 = a as Element of REAL by XREAL_0:def 1;
A1: ( x is FinSequence of REAL & y is FinSequence of REAL ) by Lm2;
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 A1, FINSEQ_2:92;
|((a * x),y)| = Sum (a2 * (mlt (x2,y2))) by FINSEQOP:26
.= a * |(x,y)| by Th87 ;
hence |((a * x),y)| = a * |(x,y)| ; :: thesis: verum