theorem Lem12: :: BAGORD_2:9

for p, q being FinSequence holds
( p c< q iff ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) ) )