theorem :: ALGSEQ_1:4

canceled;