let t, z be Integer; :: thesis: ( t * z = t + z implies t = z )
assume t * z = t + z ; :: thesis: t = z
then 0 = ((t - 1) * (z - 1)) - 1 ;
then ( ( t - 1 = 1 & z - 1 = 1 ) or ( t - 1 = - 1 & z - 1 = - 1 ) ) by INT_1:9;
hence t = z ; :: thesis: verum