let X be set ; :: thesis: for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
let f be FinSequence of X; :: thesis: for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = f /. i )
assume ( 1 <= i & i <= len f ) ; :: thesis: f . i = f /. i
then i in Seg (len f) by FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
hence f . i = f /. i by PARTFUN1:def 6; :: thesis: verum