let k be Element of 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:19;
A2: v2 is_a_prefix_of v1 by TREES_1:def 1;
consider v being FinSequence such that
A3: v1 = v2 ^ v by A2, TREES_1:8;
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 )
A4: k <= k + 1 by NAT_1:11;
A5: len v2 = k by A1, A4, FINSEQ_1:21;
A6: k + (len v) = k + 1 by A1, A3, A5, FINSEQ_1:35;
thus ( v1 = v2 ^ <*(v . 1)*> & len v2 = k ) by A1, A3, A4, A6, FINSEQ_1:21, FINSEQ_1:57; :: thesis: verum