let i be Nat; :: thesis: ( 1 <= i & i <= len <*(a ")*> implies (<*a*> ") . i = <*(a ")*> . i )
assume A2: ( 1 <= i & i <= len <*(a ")*> ) ; :: thesis: (<*a*> ") . i = <*(a ")*> . i
A3: len <*(a ")*> = 1 by FINSEQ_1:39;
then A4: i = 1 by A2, XXREAL_0:1;
len <*a*> = 1 by FINSEQ_1:39;
then i in Seg (len <*a*>) by A2, A3;
then A5: i in dom <*a*> by FINSEQ_1:def 3;
i in Seg (len (<*a*> ")) by A1, A2;
then i in dom (<*a*> ") by FINSEQ_1:def 3;
then A6: (<*a*> ") . i = (<*a*> ") /. i by PARTFUN1:def 6
.= (<*a*> /. i) " by A5, Def3 ;
<*a*> /. i = <*a*> . i by A5, PARTFUN1:def 6
.= a by A4, FINSEQ_1:40 ;
hence (<*a*> ") . i = <*(a ")*> . i by A4, A6, FINSEQ_1:40; :: thesis: verum