let a be Element of NAT ; 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; ( 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
; 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; verum