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