let K be Field; :: thesis: for x, y being FinSequence of K
for a being Element of K st len x = len y holds
|(x,(a * y))| = a * |(x,y)|
let x, y be FinSequence of K; :: thesis: for a being Element of K st len x = len y holds
|(x,(a * y))| = a * |(x,y)|
let a be Element of K; :: 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 Sum (mlt (x,(a * y))) = Sum (a * (mlt (x,y))) by Th8;
then Sum (mlt (x,(a * y))) = a * (Sum (mlt (x,y))) by FVSUM_1:73;
then Sum (mlt (x,(a * y))) = a * |(x,y)| by FVSUM_1:def 9;
hence |(x,(a * y))| = a * |(x,y)| by FVSUM_1:def 9; :: thesis: verum