let fs be FinSequence; :: thesis: ( 1 <= len fs implies ( fs = <*(fs . 1)*> ^ (Del fs,1) & fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*> ) )
assume A1: 1 <= len fs ; :: thesis: ( 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))*>;
A2: ( len <*(fs . 1)*> = 1 & len <*(fs . (len fs))*> = 1 ) by FINSEQ_1:56;
A3: 1 in dom fs by A1, FINSEQ_3:27;
A4: len fs in dom fs by A1, FINSEQ_3:27;
then A5: (len (Del fs,(len fs))) + 1 = len fs by Def1;
then A6: len (Del fs,(len fs)) = (len fs) - 1 ;
A7: len fs = (len <*(fs . 1)*>) + (len (Del fs,1)) by A2, A3, Def1
.= len (<*(fs . 1)*> ^ (Del fs,1)) by FINSEQ_1:35 ;
A8: len fs = (len <*(fs . (len fs))*>) + (len (Del fs,(len fs))) by A2, A4, Def1
.= len ((Del fs,(len fs)) ^ <*(fs . (len fs))*>) 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 A9: ( 1 <= b & b <= len fs ) ; :: thesis: fs . b = (<*(fs . 1)*> ^ (Del fs,1)) . b

now

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

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

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

end;

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

then A12: b - 1 > 0 by XREAL_1:52;
then reconsider e = b - 1 as Element of NAT by INT_1:16;
A13: e >= 1 by A12, NAT_1:14;
thus (<*(fs . 1)*> ^ (Del fs,1)) . b = (Del fs,1) . e by A2, A7, A9, A11, FINSEQ_1:37
.= fs . (e + 1) by A3, A13, 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 A7, FINSEQ_1:18; :: thesis: fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*>
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 A14: ( 1 <= b & 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 A14, XXREAL_0:1;

suppose A16: 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 A5, A8, A16, FINSEQ_1:37, XREAL_1:148
.= fs . b by A16, FINSEQ_1:57 ; :: thesis: verum

end;

suppose A17: 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 A6, XREAL_1:21;
then b in dom (Del fs,(len fs)) by A14, 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 A4, A17, 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 A8, FINSEQ_1:18; :: thesis: verum