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:101; :: thesis: verum

end;

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