let K be Field; :: thesis: for x, y being FinSequence of K
for a being Element of K st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let x, y be FinSequence of K; :: thesis: for a being Element of K st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let a be Element of K; :: thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
assume A1: len x = len y ; :: thesis: |((a * x),y)| = a * |(x,y)|
A3: Sum (mlt (a * x),y) = Sum (a * (mlt x,y)) by BB243, A1;
A4: Sum (mlt (a * x),y) = a * (Sum (mlt x,y)) by A3, FVSUM_1:92;
Sum (mlt (a * x),y) = a * |(x,y)| by A4, FVSUM_1:def 10;
hence |((a * x),y)| = a * |(x,y)| by FVSUM_1:def 10; :: thesis: verum