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:39;
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:25;
A4: 1 in dom fs by A2, FINSEQ_3:25;
then A5: len fs = (len <*(fs . 1)*>) + (len (Del (fs,1))) by A1, Def1
.= len (<*(fs . 1)*> ^ (Del (fs,1))) by FINSEQ_1:22 ;
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 :: thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b

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:25;
hence (<*(fs . 1)*> ^ (Del (fs,1))) . b = <*(fs . 1)*> . 1 by A8, FINSEQ_1:def 7
.= fs . b by A8 ;
:: thesis: verum

end;

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

then A10: b - 1 > 0 by XREAL_1:50;
then reconsider e = b - 1 as Element of NAT by INT_1:3;
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:24
.= 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; :: thesis: fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*>
len <*(fs . (len fs))*> = 1 by FINSEQ_1:39;
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:22 ;
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 :: thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b

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:24, XREAL_1:146
.= fs . b by A17 ; :: 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:19;
then b in dom (Del (fs,(len fs))) by A15, FINSEQ_3:25;
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; :: thesis: verum