let i be Nat; :: thesis: for D being set
for P being FinSequence of D st 1 <= i & i <= len P holds
P /. i = P . i
let D be set ; :: thesis: for P being FinSequence of D st 1 <= i & i <= len P holds
P /. i = P . i
let P be FinSequence of D; :: thesis: ( 1 <= i & i <= len P implies P /. i = P . i )
assume ( 1 <= i & i <= len P ) ; :: thesis: P /. i = P . i
then i in dom P by FINSEQ_3:25;
hence P /. i = P . i by PARTFUN1:def 6; :: thesis: verum