let f be FinSequence; :: thesis: for n, i being Element of NAT st i <= n holds
(f | (Seg n)) | (Seg i) = f | (Seg i)
let n, i be Element of NAT ; :: thesis: ( i <= n implies (f | (Seg n)) | (Seg i) = f | (Seg i) )
assume i <= n ; :: thesis: (f | (Seg n)) | (Seg i) = f | (Seg i)
then Seg i c= Seg n by FINSEQ_1:5;
hence (f | (Seg n)) | (Seg i) = f | (Seg i) by RELAT_1:74; :: thesis: verum