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