:: deftheorem Def6 defines /. PARTFUN1:def 6 :
for D being set
for p being b₁ -valued Function
for i being object st i in dom p holds
p /. i = p . i;