let D be non empty set ; :: thesis: for df being FinSequence of D st not df is empty holds
ex d being Element of D ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 )
let df be FinSequence of D; :: thesis: ( not df is empty implies ex d being Element of D ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 ) )
deffunc H₁( Nat) -> set = df . ($1 + 1);
assume A1: not df is empty ; :: thesis: ex d being Element of D ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 )
then reconsider lend1 = (len df) - 1 as Element of NAT by INT_1:5, NAT_1:14;
1 <= len df by A1, NAT_1:14;
then 1 in dom df by Th25;
then reconsider d = df . 1 as Element of D by FINSEQ_2:11;
take d ; :: thesis: ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 )
consider dta being FinSequence such that
A2: len dta = lend1 and
A3: for j being Nat st j in dom dta holds
dta . j = H₁(j) from FINSEQ_1:sch 2();

now :: thesis: for j being Nat st j in dom dta holds
dta . j in D

let j be Nat; :: thesis: ( j in dom dta implies dta . j in D )
assume A4: j in dom dta ; :: thesis: dta . j in D
then j in Seg (len dta) by FINSEQ_1:def 3;
then j + 1 in Seg ((len dta) + 1) by FINSEQ_1:60;
then j + 1 in dom df by A2, FINSEQ_1:def 3;
then df . (j + 1) in D by FINSEQ_2:11;
hence dta . j in D by A3, A4; :: thesis: verum

end;

then reconsider dta = dta as FinSequence of D by FINSEQ_2:12;
take dta ; :: thesis: ( d = df . 1 & df = <*d*> ^ dta )
thus d = df . 1 ; :: thesis: df = <*d*> ^ dta

now :: thesis: ( len (<*d*> ^ dta) = len df & ( for i being Nat st i in dom df holds
df . i = (<*d*> ^ dta) . i ) )

thus A5: len (<*d*> ^ dta) = (len <*d*>) + (len dta) by FINSEQ_1:22
.= 1 + ((len df) - 1) by A2, FINSEQ_1:40
.= len df ; :: thesis: for i being Nat st i in dom df holds
df . b₂ = (<*d*> ^ dta) . b₂
let i be Nat; :: thesis: ( i in dom df implies df . b₁ = (<*d*> ^ dta) . b₁ )
A6: dom df = Seg (len df) by FINSEQ_1:def 3;
assume A7: i in dom df ; :: thesis: df . b₁ = (<*d*> ^ dta) . b₁
then A8: 1 <= i by A6, FINSEQ_1:1;
A9: i <= len df by A6, A7, FINSEQ_1:1;

per cases ( i = 1 or i > 1 ) by A8, XXREAL_0:1;

suppose i = 1 ; :: thesis: df . b₁ = (<*d*> ^ dta) . b₁

hence df . i = (<*d*> ^ dta) . i by FINSEQ_1:41; :: thesis: verum

end;

suppose A10: i > 1 ; :: thesis: df . b₁ = (<*d*> ^ dta) . b₁

then consider j being Element of NAT such that
A11: j = i - 1 and
A12: 1 <= j by INT_1:51;
i - 1 <= lend1 by A9, XREAL_1:9;
then A13: j in dom dta by A2, A11, A12, Th25;
len <*d*> = 1 by FINSEQ_1:40;
then (<*d*> ^ dta) . i = dta . j by A5, A9, A10, A11, FINSEQ_1:24
.= df . (j + 1) by A3, A13
.= df . i by A11 ;
hence df . i = (<*d*> ^ dta) . i ; :: thesis: verum

end;

end;

end;

hence df = <*d*> ^ dta by FINSEQ_2:9; :: thesis: verum