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 dom f by FINSEQ_3:25;
hence f . i = f /. i by PARTFUN1:def 6; :: thesis: verum