theorem Th4: :: MSAFREE1:4

for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being non-empty ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2