let K be Field; :: thesis: for x being FinSequence of K holds |(x,(0* (K,(len x))))| = 0. K
let x be FinSequence of K; :: thesis: |(x,(0* (K,(len x))))| = 0. K
set n = len x;
reconsider p1 = x as Element of (len x) -tuples_on the carrier of K by FINSEQ_2:92;
|(x,(0* (K,(len x))))| = Sum (mlt (p1,(0* (K,(len x))))) by FVSUM_1:def 9
.= Sum (0* (K,(len x))) by Th13
.= 0. K by MATRIX_3:11 ;
hence |(x,(0* (K,(len x))))| = 0. K ; :: thesis: verum