:: deftheorem D1 defines PFcompos PARTPR_2:def 1 :
for A, B, C being set
for b₄ being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) holds
( b₄ = PFcompos (A,B,C) iff for f being PartFunc of A,B
for g being PartFunc of B,C holds b₄ . (f,g) = g * f );