let K be Field; :: thesis: for x being FinSequence of K holds |((0* K,(len x)),x)| = 0. K
let x be FinSequence of K; :: thesis: |((0* K,(len x)),x)| = 0. K
thus |((0* K,(len x)),x)| = |(x,(0* K,(len x)))| by FVSUM_1:115
.= 0. K by Th17 ; :: thesis: verum