:: deftheorem defines compint INT_3:def 2 :
for b₁ being Element of K16(K17(INT,INT)) holds
( b₁ = compint iff for a being Element of INT holds b₁ . a = compreal . a );