let fs be FinSequence; :: thesis: ( 1 <= len fs implies ( fs = <*(fs . 1)*> ^ (Del fs,1) & fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*> ) )
set fs1 = <*(fs . 1)*> ^ (Del fs,1);
set fs2 = (Del fs,(len fs)) ^ <*(fs . (len fs))*>;
A1: len <*(fs . 1)*> = 1 by FINSEQ_1:56;
assume A2: 1 <= len fs ; :: thesis: ( fs = <*(fs . 1)*> ^ (Del fs,1) & fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*> )
then A3: len fs in dom fs by FINSEQ_3:27;
A4: 1 in dom fs by A2, FINSEQ_3:27;
then A5: len fs = (len <*(fs . 1)*>) + (len (Del fs,1)) by A1, Def1
.= len (<*(fs . 1)*> ^ (Del fs,1)) by FINSEQ_1:35 ;
for b being Nat st 1 <= b & b <= len fs holds
fs . b = (<*(fs . 1)*> ^ (Del fs,1)) . b

proof

let b be Nat; :: thesis: ( 1 <= b & b <= len fs implies fs . b = (<*(fs . 1)*> ^ (Del fs,1)) . b )
assume that
A6: 1 <= b and
A7: b <= len fs ; :: thesis: fs . b = (<*(fs . 1)*> ^ (Del fs,1)) . b

now

per cases ( b = 1 or b > 1 ) by A6, XXREAL_0:1;

suppose A8: b = 1 ; :: thesis: (<*(fs . 1)*> ^ (Del fs,1)) . b = fs . b

1 in dom <*(fs . 1)*> by A1, FINSEQ_3:27;
hence (<*(fs . 1)*> ^ (Del fs,1)) . b = <*(fs . 1)*> . 1 by A8, FINSEQ_1:def 7
.= fs . b by A8, FINSEQ_1:57 ;
:: thesis: verum

end;

suppose A9: b > 1 ; :: thesis: (<*(fs . 1)*> ^ (Del fs,1)) . b = fs . b

then A10: b - 1 > 0 by XREAL_1:52;
then reconsider e = b - 1 as Element of NAT by INT_1:16;
A11: e >= 1 by A10, NAT_1:14;
thus (<*(fs . 1)*> ^ (Del fs,1)) . b = (Del fs,1) . e by A1, A5, A7, A9, FINSEQ_1:37
.= fs . (e + 1) by A4, A11, Def1
.= fs . b ; :: thesis: verum

end;

end;

end;

hence fs . b = (<*(fs . 1)*> ^ (Del fs,1)) . b ; :: thesis: verum

end;

hence <*(fs . 1)*> ^ (Del fs,1) = fs by A5, FINSEQ_1:18; :: thesis: fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*>
len <*(fs . (len fs))*> = 1 by FINSEQ_1:56;
then A12: len fs = (len <*(fs . (len fs))*>) + (len (Del fs,(len fs))) by A3, Def1
.= len ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) by FINSEQ_1:35 ;
A13: (len (Del fs,(len fs))) + 1 = len fs by A3, Def1;
then A14: len (Del fs,(len fs)) = (len fs) - 1 ;
for b being Nat st 1 <= b & b <= len fs holds
fs . b = ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b

proof

let b be Nat; :: thesis: ( 1 <= b & b <= len fs implies fs . b = ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b )
assume that
A15: 1 <= b and
A16: b <= len fs ; :: thesis: fs . b = ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b

now

per cases ( b = len fs or b < len fs ) by A16, XXREAL_0:1;

suppose A17: b = len fs ; :: thesis: ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b = fs . b

reconsider e = b - (b - 1) as Element of NAT ;
thus ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b = <*(fs . (len fs))*> . e by A13, A12, A17, FINSEQ_1:37, XREAL_1:148
.= fs . b by A17, FINSEQ_1:57 ; :: thesis: verum

end;

suppose A18: b < len fs ; :: thesis: ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b = fs . b

then b + 1 <= len fs by NAT_1:13;
then b <= len (Del fs,(len fs)) by A14, XREAL_1:21;
then b in dom (Del fs,(len fs)) by A15, FINSEQ_3:27;
hence ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b = (Del fs,(len fs)) . b by FINSEQ_1:def 7
.= fs . b by A3, A18, Def1 ;
:: thesis: verum

end;

end;

end;

hence fs . b = ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) . b ; :: thesis: verum

end;

hence fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*> by A12, FINSEQ_1:18; :: thesis: verum