:: deftheorem defines PP_composition NOMIN_6:def 1 :
for D being set
for f1, f2, f3, f4, f5 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5) = PP_composition ((PP_composition (f1,f2,f3,f4)),f5);