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:84; :: thesis: verum