let x, y be FinSequence of REAL ; :: 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)| )
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 FINSEQ_2:110;
reconsider a2 = a as Element of REAL by XREAL_0:def 1;
|((a * x),y)| = Sum (a2 * (mlt x2,y2)) by FINSEQOP:27
.= a * |(x,y)| by RVSUM_1:117 ;
hence |((a * x),y)| = a * |(x,y)| ; :: thesis: verum