let r be non zero non unit Real; :: thesis: ( op2 (op1 (op2 (op1 r))) = op1 (op2 r) & op1 (op2 (op1 (op2 r))) = op2 (op1 r) )
( op2 (op1 (op2 (op1 r))) = 1 - (r / (r - 1)) & op1 (op2 (op1 (op2 r))) = 1 / (r / (r - 1)) ) by Th01;
hence ( op2 (op1 (op2 (op1 r))) = op1 (op2 r) & op1 (op2 (op1 (op2 r))) = op2 (op1 r) ) ; :: thesis: verum