let p, q be FinSequence; :: thesis: ( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p )
A1: maxPrefix (p,q) c= p by Def1;

hereby :: thesis: ( len (maxPrefix (p,q)) < len p implies not p is_a_prefix_of q )

assume A2: not p c= q ; :: thesis: len (maxPrefix (p,q)) < len p

A3: now :: thesis: not len (maxPrefix (p,q)) = len p

assume len (maxPrefix (p,q)) = len p ; :: thesis: contradiction
then A4: dom (maxPrefix (p,q)) = dom p by FINSEQ_3:29;
maxPrefix (p,q) c= p by Def1;
then maxPrefix (p,q) = p by A4, GRFUNC_1:3;
hence contradiction by A2, Def1; :: thesis: verum

end;

maxPrefix (p,q) c= p by Def1;
then len (maxPrefix (p,q)) <= len p by FINSEQ_1:63;
hence len (maxPrefix (p,q)) < len p by A3, XXREAL_0:1; :: thesis: verum

end;

assume that
A5: len (maxPrefix (p,q)) < len p and
A6: p c= q ; :: thesis: contradiction
p c= maxPrefix (p,q) by A6, Def1;
hence contradiction by A5, A1, XBOOLE_0:def 10; :: thesis: verum