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

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