let X be set ; :: thesis: for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d)
let b, c, d be natural-valued ManySortedSet of X; :: thesis: (b -' c) -' d = b -' (c + d)

now :: thesis: for x being object st x in X holds
((b -' c) -' d) . x = (b . x) -' ((c + d) . x)

let x be object ; :: thesis: ( x in X implies ((b -' c) -' d) . x = (b . x) -' ((c + d) . x) )
assume x in X ; :: thesis: ((b -' c) -' d) . x = (b . x) -' ((c + d) . x)
thus ((b -' c) -' d) . x = ((b -' c) . x) -' (d . x) by Def6
.= ((b . x) -' (c . x)) -' (d . x) by Def6
.= (b . x) -' ((c . x) + (d . x)) by NAT_2:30
.= (b . x) -' ((c + d) . x) by Def5 ; :: thesis: verum

end;

hence (b -' c) -' d = b -' (c + d) by Th33; :: thesis: verum