let K be Field; :: thesis: for a being Element of K holds |(<*(0. K)*>,<*a*>)| = 0. K
let a be Element of K; :: thesis: |(<*(0. K)*>,<*a*>)| = 0. K
A1: len <*a*> = 1 by FINSEQ_1:39;
thus |(<*(0. K)*>,<*a*>)| = |((0* (K,1)),<*a*>)| by FINSEQ_2:59
.= 0. K by A1, Th21 ; :: thesis: verum