let r be non zero non unit Real; ( op2 (op1 r) = (r - 1) / r & op1 (op2 r) = 1 / (1 - r) & op1 (op2 (op1 r)) = r / (r - 1) & op2 (op1 (op2 r)) = r / (r - 1) )
A1: 1 - (1 / r) =
(r / r) - (1 / r)
by XCMPLX_1:60
.=
(r - 1) / r
;
1 - r <> 0
by Def01;
then 1 - (1 / (1 - r)) =
((1 - r) / (1 - r)) - (1 / (1 - r))
by XCMPLX_1:60
.=
- (r / (1 - r))
.=
r / (- (1 - r))
by XCMPLX_1:188
;
hence
( op2 (op1 r) = (r - 1) / r & op1 (op2 r) = 1 / (1 - r) & op1 (op2 (op1 r)) = r / (r - 1) & op2 (op1 (op2 r)) = r / (r - 1) )
by A1, XCMPLX_1:57; verum