let I be set ; :: thesis: union ([0] I) = [0] I

now

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

end;

hence union ([0] I) = [0] I by PBOOLE:3; :: thesis: verum