let a be Element of NAT ; :: thesis: for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )

let fs be FinSequence; :: thesis: ( a in dom fs implies ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) )

assume A1: a in dom fs ; :: thesis: ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )

then ( a >= 1 & a <= len fs ) by FINSEQ_3:25;
then reconsider b = (len fs) - a, d = a - 1 as Element of NAT by INT_1:5;
len fs = a + b ;
then consider fs3, fs2 being FinSequence such that
A2: len fs3 = a and
A3: len fs2 = b and
A4: fs = fs3 ^ fs2 by FINSEQ_2:22;
a = d + 1 ;
then consider fs1 being FinSequence, v being object such that
A5: fs3 = fs1 ^ <*v*> by ;
A6: (len fs1) + 1 = d + 1 by ;
fs3 <> {} by ;
then a in dom fs3 by ;
then fs3 . a = fs . a by ;
then fs . a = v by ;
hence ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) by A3, A4, A5, A6; :: thesis: verum