theorem :: CLASSES5:74

Trivial-addLoopStr = Trivial-addLoopStr 0 by ALGSTR_0:def 9, FUNCT_5:def 6;