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