:: deftheorem defines PP_composition NOMIN_8:def 3 :
for D being non empty set
for f1, f2, f3, f4, f5, f6, f7, f8, f9 being BinominativeFunction of D holds PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9) = PP_composition ((PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),f9);