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:38 ;
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:40 ;
len (1. (K,<*i*>)) = 1 by A1, FINSEQ_1:def 3;
hence 1. (K,<*i*>) = <*(1. (K,i))*> by A2, FINSEQ_1:40; :: thesis: verum