theorem :: ALGSEQ_1:6

canceled;