let I be set ; :: thesis: union (EmptyMS I) = EmptyMS I

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

let i be object ; :: thesis: ( i in I implies (union (EmptyMS I)) . i = (EmptyMS I) . i )
assume i in I ; :: thesis: (union (EmptyMS I)) . i = (EmptyMS I) . i
hence (union (EmptyMS I)) . i = union ((EmptyMS I) . i) by Def2
.= {} by PBOOLE:5, ZFMISC_1:2
.= (EmptyMS I) . i by PBOOLE:5 ;
:: thesis: verum

end;

hence union (EmptyMS I) = EmptyMS I ; :: thesis: verum