let I be set ; :: thesis: for A being ManySortedSet of I holds union (bool A) = A
let A be ManySortedSet of I; :: thesis: union (bool A) = A

now :: thesis: for i being object st i in I holds
(union (bool A)) . i = A . i

let i be object ; :: thesis: ( i in I implies (union (bool A)) . i = A . i )
assume A1: i in I ; :: thesis: (union (bool A)) . i = A . i
hence (union (bool A)) . i = union ((bool A) . i) by Def2
.= union (bool (A . i)) by A1, Def1
.= A . i by ZFMISC_1:81 ;
:: thesis: verum

end;

hence union (bool A) = A ; :: thesis: verum