theorem :: CLASSES5:74

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