[{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
hence op2 . ({},{}) = {} by FUNCT_2:50; :: thesis: ( op1 . {} = {} & op0 = {} )
{} in {{}} by TARSKI:def 1;
hence op1 . {} = {} by FUNCT_2:50; :: thesis: op0 = {}
thus op0 = {} ; :: thesis: verum