let p, q be FinSequence; :: thesis: len (maxPrefix (p,q)) <= len p
maxPrefix (p,q) c= p by Def1;
hence len (maxPrefix (p,q)) <= len p by FINSEQ_1:63; :: thesis: verum