let I be set ; :: thesis: for i being object holds (EmptyMS I) . i = {}
let i be object ; :: thesis: (EmptyMS I) . i = {}

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

suppose i in I ; :: thesis: (EmptyMS I) . i = {}

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

end;

suppose not i in I ; :: thesis: (EmptyMS I) . i = {}

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

end;

end;