[{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
hence op2 . ({},{}) = {} by FUNCT_2:50; :: thesis: verum