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