let a, b, d be Real; ( 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) implies ( a = 0 & b = 0 ) )
assume that
A1:
0 <= d
and
A2:
d <= 1
and
A3:
a >= 0
and
A4:
b >= 0
and
A5:
(d * a) + ((1 - d) * b) = 0
; ( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) )
d - d <= 1 - d
by A2, Lm7;
then
( 1 - d = 0 or b = 0 )
by A1, A3, A4, A5;
hence
( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) )
by A5; verum