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