let lambda, mu, nu be Real; ( mu <> 1 & 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) & (1 - mu) + (mu * lambda) = 0 implies (1 - lambda) + (lambda * nu) = 0 )
assume that
A1:
mu <> 1
and
A2:
0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))
and
A3:
(1 - mu) + (mu * lambda) = 0
; (1 - lambda) + (lambda * nu) = 0
A4:
1 - mu <> 0
by A1;
0 = ((- (1 - mu)) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))
by A2, A3;
then
0 = (1 - mu) * (nu + ((1 - lambda) * (1 - nu)))
;
hence
(1 - lambda) + (lambda * nu) = 0
by A4; verum