theorem :: ALGSEQ_1:7

canceled;