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 ) )
assume 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 A1: len df <> 0 ;
then 1 <= len df by NAT_1:14;
then 1 in dom df by Th27;
then reconsider d = df . 1 as Element of D by FINSEQ_2:13;
take d ; :: thesis: ex df1 being FinSequence of D st
( d = df . 1 & df = <*d*> ^ df1 )
reconsider lend1 = (len df) - 1 as Element of NAT by A1, INT_1:18, NAT_1:14;
deffunc H₁( Nat) -> set = df . ($1 + 1);
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

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:81;
then j + 1 in dom df by A2, FINSEQ_1:def 3;
then df . (j + 1) in D by FINSEQ_2:13;
hence dta . j in D by A3, A4; :: thesis: verum

end;

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

now

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

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

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

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

end;

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

then consider j being Element of NAT such that
A9: ( j = i - 1 & 1 <= j ) by INT_1:78;
i - 1 <= lend1 by A7, XREAL_1:11;
then A10: j in dom dta by A9, A2, Th27;
len <*d*> = 1 by FINSEQ_1:57;
then (<*d*> ^ dta) . i = dta . j by A6, A7, A8, A9, FINSEQ_1:37
.= df . (j + 1) by A3, A10
.= df . i by A9 ;
hence df . i = (<*d*> ^ dta) . i ; :: thesis: verum

end;

end;

end;

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