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

assume len (maxPrefix p,q) = len p ; :: thesis: contradiction
then A4: dom (maxPrefix p,q) = dom p by FINSEQ_3:31;
maxPrefix p,q c= p by Def1;
then maxPrefix p,q = p by A4, GRFUNC_1:9;
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:84;
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