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:110;
|(x,(0* K,(len x)))| = Sum (mlt p1,(0* K,(len x))) by FVSUM_1:def 10
.= Sum (0* K,(len x)) by Th2
.= 0. K by MATRIX_3:13 ;
hence |(x,(0* K,(len x)))| = 0. K ; :: thesis: verum