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:27;
then reconsider b = (len fs) - a, d = a - 1 as Element of NAT by INT_1:18;
len fs = a + b ;
then consider fs3, fs2 being FinSequence such that
A2: ( len fs3 = a & len fs2 = b & fs = fs3 ^ fs2 ) by FINSEQ_2:25;
a <> 0 by A1, FINSEQ_3:27;
then fs3 <> {} by A2;
then a in dom fs3 by A2, FINSEQ_5:6;
then A3: fs3 . a = fs . a by A2, FINSEQ_1:def 7;
a = d + 1 ;
then consider fs1 being FinSequence, v being set such that
A4: fs3 = fs1 ^ <*v*> by A2, FINSEQ_2:21;
A5: (len fs1) + 1 = d + 1 by A2, A4, FINSEQ_2:19;
then fs . a = v by A3, A4, FINSEQ_1:59;
hence ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) by A2, A4, A5; :: thesis: verum