theorem :: CLASSES5:73

( op0 0 = op0 & op1 0 = op1 & op2 0 = op2 ) by FUNCT_5:def 5, FUNCT_5:def 6;