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:56;
thus |(<*(0. K)*>,<*a*>)| = |((0* K,1),<*a*>)| by FINSEQ_2:73
.= 0. K by A1, Th18 ; :: thesis: verum