let p, q be non empty FinSequence; :: thesis: ( p . 1 = q . 1 implies 1 <= len (maxPrefix (p,q)) )
assume that
A1: p . 1 = q . 1 and
A2: 1 > len (maxPrefix (p,q)) ; :: thesis: contradiction
A3: <*(p . 1)*> c= p by Th4;
<*(p . 1)*> c= q by A1, Th4;
then <*(p . 1)*> c= maxPrefix (p,q) by A3, Def1;
then len <*(p . 1)*> <= len (maxPrefix (p,q)) by FINSEQ_1:63;
hence contradiction by A2, FINSEQ_1:39; :: thesis: verum