{{}} = dom op1 by CARD_1:49, 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 CARD_1:49, FUNCT_2:48;
then A2: op1 . {} = {} by CARD_1:49, ZFMISC_1:18;
op1 c= [:{{}},{{}}:] by CARD_1:49;
then op1 c= {[{},{}]} by ZFMISC_1:29;
hence op1 = {[{},{}]} by A2, A1, XBOOLE_0:def 10; :: thesis: verum