theorem :: FINSEQ_3:113

for p, q being FinSequence st p c= q holds
q | (len p) = p