for f being non-empty Function
for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A