let a, b, k be Nat; :: thesis: ( a + b = (k * a) + (k * b) & a * b > 0 implies k = 1 )
assume A0: ( a + b = (k * a) + (k * b) & a * b > 0 ) ; :: thesis: k = 1
then (k - 1) * (a + b) = 0 ;
then ( a + b = 0 or k - 1 = 0 ) ;
then ( a = 0 or k = 1 ) ;
hence k = 1 by A0; :: thesis: verum