for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st ( for i being object holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g