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 A1: p c= q ; :: thesis: maxPrefix p,q = p
A2: maxPrefix p,q c= p by Def1;
p c= maxPrefix p,q by A1, Def1;
hence maxPrefix p,q = p by A2, 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