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:90
.= 0. K by Th20 ; :: thesis: verum