for I being set
for f being V2() ManySortedSet of I
for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f