:: deftheorem defines base_exp_of ABCMIZ_A:def 19 :
for c being Element of Constructors holds base_exp_of c = (@ c) -trm (args (loci_of c));