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