let D be non empty set ; :: thesis: for r being FinSequence of D
for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
let r be FinSequence of D; :: thesis: for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
let r1 be FinSequence; :: thesis: ( 1 <= len r & r1 = r | (Seg 1) implies ex x being Element of D st r1 = <*x*> )
assume that
A1: 1 <= len r and
A2: r1 = r | (Seg 1) ; :: thesis: ex x being Element of D st r1 = <*x*>
consider x being set such that
A3: x = r1 . 1 ;
1 in {1} by TARSKI:def 1;
then 1 in dom r1 by A1, A2, FINSEQ_1:2, FINSEQ_1:17;
then A4: x in rng r1 by A3, FUNCT_1:def 3;
len r1 = 1 by A1, A2, FINSEQ_1:17;
then A5: r1 = <*x*> by A3, FINSEQ_1:40;
r1 is_a_prefix_of r by A2, TREES_1:def 1;
then ex q1 being FinSequence st r = r1 ^ q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
rng r9 c= D ;
hence ex x being Element of D st r1 = <*x*> by A5, A4; :: thesis: verum