:: deftheorem Def1 defines multint INT_3:def 1 :
for b₁ being Element of K16(K17(K17(INT,INT),INT)) holds
( b₁ = multint iff for a, b being Element of INT holds b₁ . (a,b) = multreal . (a,b) );