let mu, lambda, nu be Real; :: thesis: ( 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
A: mu <> 1 and
B: 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) and
C: (1 - mu) + (mu * lambda) = 0 ; :: thesis: (1 - lambda) + (lambda * nu) = 0
D: 1 - mu <> 0 by A;
0 = ((- (1 - mu)) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) by B, C;
then 0 = (1 - mu) * (nu + ((1 - lambda) * (1 - nu))) ;
hence (1 - lambda) + (lambda * nu) = 0 by D; :: thesis: verum