let K be Field; :: thesis: for i being Element of NAT holds 1. K,<*i*> = <*(1. K,i)*>
let i be Element of NAT ; :: thesis: 1. K,<*i*> = <*(1. K,i)*>
A1: dom (1. K,<*i*>) = dom <*i*> by Def8
.= Seg 1 by FINSEQ_1:55 ;
then 1 in dom (1. K,<*i*>) ;
then A2: (1. K,<*i*>) . 1 = 1. K,(<*i*> . 1) by Def8
.= 1. K,i by FINSEQ_1:57 ;
len (1. K,<*i*>) = 1 by A1, FINSEQ_1:def 3;
hence 1. K,<*i*> = <*(1. K,i)*> by A2, FINSEQ_1:57; :: thesis: verum