:: deftheorem defines is_Iso_of AFVECT0:def 9 :
for X, Y being non empty addLoopStr
for f being Function of the carrier of X, the carrier of Y holds
( f is_Iso_of X,Y iff ( f is one-to-one & rng f = the carrier of Y & ( for a, b being Element of X holds
( f . (a + b) = (f . a) + (f . b) & f . (0. X) = 0. Y & f . (- a) = - (f . a) ) ) ) );