let A, B, I be set ; :: thesis: for X, Y being ManySortedSet of I st I c= A \/ B & X | B = Y | B holds
X,Y equal_outside A
let X, Y be ManySortedSet of I; :: thesis: ( I c= A \/ B & X | B = Y | B implies X,Y equal_outside A )
( dom X = I & dom Y = I ) by PARTFUN1:def 2;
hence ( I c= A \/ B & X | B = Y | B implies X,Y equal_outside A ) by Th133; :: thesis: verum