for I being set
for f being non-empty b₁ -defined Function
for p being b₁ -defined b₂ -compatible Function ex s being Element of product f st p c= s