let K be Field; 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; 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; ( 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
; ( 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))
; 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))
; verum