let n be Nat; :: thesis: for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
let r be FinSequence; :: thesis: ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
r | (Seg n) is FinSequence by FINSEQ_1:15;
then consider q being FinSequence such that
A1: q = r | (Seg n) ;
q is_a_prefix_of r by A1, TREES_1:def 1;
hence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r ) by A1; :: thesis: verum