theorem :: ALGSEQ_1:5

canceled;