let K be Field; :: thesis: for x, y being FinSequence of
for a being Element of 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 ; :: thesis: for a being Element of 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 ; :: 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:83
.= 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:83
.= a * (mlt x,y) ; :: thesis: verum