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