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 A1: ( 1 <= len r & r1 = r | (Seg 1) ) ; :: thesis: ex x being Element of D st r1 = <*x*>
then A2: len r1 = 1 by FINSEQ_1:21;
r1 is_a_prefix_of r by A1, TREES_1:def 1;
then consider q1 being FinSequence such that
A3: r = r1 ^ q1 by TREES_1:8;
reconsider r' = r1 as FinSequence of D by A3, FINSEQ_1:50;
consider x being set such that
A4: x = r1 . 1 ;
A5: r1 = <*x*> by A2, A4, FINSEQ_1:57;
1 in {1} by TARSKI:def 1;
then 1 in dom r1 by A1, FINSEQ_1:4, FINSEQ_1:21;
then A6: x in rng r1 by A4, FUNCT_1:def 5;
rng r' c= D by FINSEQ_1:def 4;
hence ex x being Element of D st r1 = <*x*> by A5, A6; :: thesis: verum