theorem :: FUNCT_6:58

commute {} = {} by FUNCT_5:42, FUNCT_5:43;