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