let x, y be FinSequence of REAL ; :: thesis: for a being real number st len x = len y holds
|(x,(a * y))| = a * |(x,y)|
let a be real number ; :: thesis: ( len x = len y implies |(x,(a * y))| = a * |(x,y)| )
assume len x = len y ; :: thesis: |(x,(a * 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;
set f = multreal ;
a * (mlt y2,x2) = multreal .: ((multreal [;] a2,(id REAL )) * y2),x2 by FINSEQOP:27
.= mlt (a * y2),x2 ;
hence |(x,(a * y))| = a * |(x,y)| by RVSUM_1:117; :: thesis: verum