let p, q be FinSequence; :: thesis: ( not p is_a_prefix_of q iff len (maxPrefix p,q) < len p )

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

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

A2: now

assume len (maxPrefix p,q) = len p ; :: thesis: contradiction
then A3: dom (maxPrefix p,q) = dom p by FINSEQ_3:31;
maxPrefix p,q c= p by Def1;
then maxPrefix p,q = p by A3, GRFUNC_1:9;
hence contradiction by A1, 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 A2, XXREAL_0:1; :: thesis: verum

end;

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