theorem :: ANPROJ10:3

for r being non zero non unit Real holds
( op2 (op1 (op2 (op1 r))) = op1 (op2 r) & op1 (op2 (op1 (op2 r))) = op2 (op1 r) )