[0,0] in [:{0},{0}:] by ZFMISC_1:28;
hence op2 . (0,0) = 0 by FUNCT_2:50; :: thesis: verum