theorem :: FINSEQ_1:73

for f, g being FinSequence holds f | (Seg 0) = g | (Seg 0) ;