let p, q be FinSequence; :: thesis: ( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )
thus ( p is_a_prefix_of q implies ex r being FinSequence st q = p ^ r ) by FINSEQ_1:80; :: thesis: ( ex r being FinSequence st q = p ^ r implies p is_a_prefix_of q )
given r being FinSequence such that A1: q = p ^ r ; :: thesis: p is_a_prefix_of q
( dom p = Seg (len p) & p = q | (dom p) ) by A1, FINSEQ_1:21, FINSEQ_1:def 3;
hence p is_a_prefix_of q ; :: thesis: verum