for S being functional with_common_domain set
for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i