let k be Nat; :: thesis: for D being non empty set
for pf being FinSequence of D st k in dom pf holds
<*pf*> * (1,k) = pf . k
let D be non empty set ; :: thesis: for pf being FinSequence of D st k in dom pf holds
<*pf*> * (1,k) = pf . k
let pf be FinSequence of D; :: thesis: ( k in dom pf implies <*pf*> * (1,k) = pf . k )
assume A1: k in dom pf ; :: thesis: <*pf*> * (1,k) = pf . k
A2: Indices <*pf*> = [:(Seg 1),(Seg (len pf)):] by MATRIX_0:23
.= [:{1},(dom pf):] by FINSEQ_1:2, FINSEQ_1:def 3 ;
1 in {1} by TARSKI:def 1;
then [1,k] in Indices <*pf*> by A1, A2, ZFMISC_1:87;
then ex q being FinSequence of D st
( q = <*pf*> . 1 & <*pf*> * (1,k) = q . k ) by MATRIX_0:def 5;
hence <*pf*> * (1,k) = pf . k ; :: thesis: verum