let k be Nat; :: thesis: for v1 being FinSequence st len v1 = k + 1 holds
ex v2 being FinSequence ex x being set st
( v1 = v2 ^ <*x*> & len v2 = k )
let v1 be FinSequence; :: thesis: ( len v1 = k + 1 implies ex v2 being FinSequence ex x being set st
( v1 = v2 ^ <*x*> & len v2 = k ) )
assume A1: len v1 = k + 1 ; :: thesis: ex v2 being FinSequence ex x being set st
( v1 = v2 ^ <*x*> & len v2 = k )
reconsider v2 = v1 | (Seg k) as FinSequence by FINSEQ_1:15;
v2 is_a_prefix_of v1 ;
then consider v being FinSequence such that
A2: v1 = v2 ^ v by TREES_1:1;
take v2 ; :: thesis: ex x being set st
( v1 = v2 ^ <*x*> & len v2 = k )
take v . 1 ; :: thesis: ( v1 = v2 ^ <*(v . 1)*> & len v2 = k )
A3: k <= k + 1 by NAT_1:11;
then len v2 = k by A1, FINSEQ_1:17;
then k + (len v) = k + 1 by A1, A2, FINSEQ_1:22;
hence ( v1 = v2 ^ <*(v . 1)*> & len v2 = k ) by A1, A2, A3, FINSEQ_1:17, FINSEQ_1:40; :: thesis: verum