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 ) :: thesis: ( ex r being FinSequence st q = p ^ r implies p is_a_prefix_of q )

proof

given n being Element of NAT such that A1: p = q | (Seg n) ; :: according to TREES_1:def 1 :: thesis: ex r being FinSequence st q = p ^ r
thus ex r being FinSequence st q = p ^ r by A1, FINSEQ_1:80; :: thesis: verum

end;

given r being FinSequence such that A2: q = p ^ r ; :: thesis: p is_a_prefix_of q
( dom p = Seg (len p) & p = q | (dom p) ) by A2, FINSEQ_1:21, FINSEQ_1:def 3;
hence p is_a_prefix_of q by Def1; :: thesis: verum