for S being non empty non void ManySortedSign
for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g