for p, q being FinSequence holds
( p is_a_prefix_of q iff maxPrefix (p,q) = p ) by Def1;