:: deftheorem defines PP_composition PARTPR_2:def 5 :
for D being set
for f, g being BinominativeFunction of D holds PP_composition (f,g) = (PPcomposition D) . (f,g);