thus ( p c= q implies ex n being Nat st p = q | (Seg n) ) :: thesis: ( ex n being Nat st p = q | (Seg n) implies p is_a_prefix_of q )

proof

assume A1: p c= q ; :: thesis: ex n being Nat st p = q | (Seg n)
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def 2;
reconsider n = n as Nat ;
take n ; :: thesis: p = q | (Seg n)
thus p = q | (Seg n) by A1, A2, GRFUNC_1:23; :: thesis: verum

end;

thus ( ex n being Nat st p = q | (Seg n) implies p is_a_prefix_of q ) by RELAT_1:59; :: thesis: verum