let I, J be set ; :: thesis: 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 )

let f be ManySortedSet of I; :: thesis: 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 )

let g be ManySortedSet of J; :: thesis: ( g is f -tolerating iff for x being object st x in I & x in J holds

f . x = g . x )

( dom f = I & dom g = J ) by PARTFUN1:def 2;

hence ( g is f -tolerating iff for x being object st x in I & x in J holds

f . x = g . x ) by Th1; :: thesis: verum

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 )

let f be ManySortedSet of I; :: thesis: 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 )

let g be ManySortedSet of J; :: thesis: ( g is f -tolerating iff for x being object st x in I & x in J holds

f . x = g . x )

( dom f = I & dom g = J ) by PARTFUN1:def 2;

hence ( g is f -tolerating iff for x being object st x in I & x in J holds

f . x = g . x ) by Th1; :: thesis: verum