let m be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st m in dom f holds
f /. m = (f | m) /. (len (f | m))
let D be non empty set ; :: thesis: for f being FinSequence of D st m in dom f holds
f /. m = (f | m) /. (len (f | m))
let f be FinSequence of D; :: thesis: ( m in dom f implies f /. m = (f | m) /. (len (f | m)) )
assume A1: m in dom f ; :: thesis: f /. m = (f | m) /. (len (f | m))
m <= len f by A1, FINSEQ_3:25;
then A2: len (f | m) = m by FINSEQ_1:59;
1 <= m by A1, FINSEQ_3:25;
then m in Seg m ;
hence f /. m = (f | m) /. (len (f | m)) by A1, A2, Th71; :: thesis: verum