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

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