let K be Field; :: thesis: for x, y being FinSequence of K
for a being Element of K st len x = len y holds
( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) )
let x, y be FinSequence of K; :: thesis: for a being Element of K st len x = len y holds
( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) )
let a be Element of K; :: thesis: ( len x = len y implies ( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) ) )
assume len x = len y ; :: thesis: ( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) )
then reconsider y0 = y as Element of (len x) -tuples_on the carrier of K by Th1;
reconsider x0 = x as Element of (len x) -tuples_on the carrier of K by Th1;
thus mlt ((a * x),y) = a * (mlt (x0,y0)) by FVSUM_1:69
.= a * (mlt (x,y)) ; :: thesis: mlt (x,(a * y)) = a * (mlt (x,y))
thus mlt (x,(a * y)) = a * (mlt (x0,y0)) by FVSUM_1:69
.= a * (mlt (x,y)) ; :: thesis: verum