{{}} = dom op1
by FUNCT_2:def 1;

then {} in dom op1 by TARSKI:def 1;

then [{},(op1 . {})] in op1 by FUNCT_1:def 2;

then A1: {[{},(op1 . {})]} c= op1 by ZFMISC_1:31;

rng op1 = {(op1 . {})} by FUNCT_2:48;

then A2: op1 . {} = {} by ZFMISC_1:18;

op1 c= [:{{}},{{}}:] ;

then op1 c= {[{},{}]} by ZFMISC_1:29;

hence op1 = {[{},{}]} by A2, A1; :: thesis: verum

then {} in dom op1 by TARSKI:def 1;

then [{},(op1 . {})] in op1 by FUNCT_1:def 2;

then A1: {[{},(op1 . {})]} c= op1 by ZFMISC_1:31;

rng op1 = {(op1 . {})} by FUNCT_2:48;

then A2: op1 . {} = {} by ZFMISC_1:18;

op1 c= [:{{}},{{}}:] ;

then op1 c= {[{},{}]} by ZFMISC_1:29;

hence op1 = {[{},{}]} by A2, A1; :: thesis: verum