for p, q being non empty FinSequence st p . 1 = q . 1 holds
1 <= len (maxPrefix (p,q))