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 A2, FINSEQ_2:18;
A6: (len fs1) + 1 = d + 1 by A2, A5, FINSEQ_2:16;
fs3 <> {} by A1, A2, FINSEQ_3:25;
then a in dom fs3 by A2, FINSEQ_5:6;
then fs3 . a = fs . a by A4, FINSEQ_1:def 7;
then fs . a = v by A5, A6, FINSEQ_1:42;
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