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