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