let i, I be set ; :: thesis: ([[0]] I) . i = {}

per cases ( i in I or not i in I ) ;

suppose i in I ; :: thesis: ([[0]] I) . i = {}

hence ([[0]] I) . i = {} by FUNCOP_1:7; :: thesis: verum

end;

suppose not i in I ; :: thesis: ([[0]] I) . i = {}

then not i in dom ([[0]] I) by FUNCOP_1:13;
hence ([[0]] I) . i = {} by FUNCT_1:def 2; :: thesis: verum

end;

end;