theorem :: ALGSEQ_1:15

canceled;