theorem Th2: :: AOFA_L00:2

for I, J being set
for f being ManySortedSet of I
for g being ManySortedSet of J holds
( g is f -tolerating iff for x being object st x in I & x in J holds
f . x = g . x )