let p, q be FinSequence; :: thesis: ( p is_a_prefix_of q iff maxPrefix (p,q) = p )

hereby :: thesis: ( maxPrefix (p,q) = p implies p is_a_prefix_of q )

assume p c= q ; :: thesis: maxPrefix (p,q) = p
then A1: p c= maxPrefix (p,q) by Def1;
maxPrefix (p,q) c= p by Def1;
hence maxPrefix (p,q) = p by A1, XBOOLE_0:def 10; :: thesis: verum

end;

assume maxPrefix (p,q) = p ; :: thesis: p is_a_prefix_of q
hence p is_a_prefix_of q by Def1; :: thesis: verum