let K be non empty doubleLoopStr ; :: thesis: for J being Function of K,K holds

( J is isomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )

let J be Function of K,K; :: thesis: ( J is isomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )

thus ( J is isomorphism implies ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) ) by GROUP_1:def 13, GROUP_6:def 6; :: thesis: ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto implies J is isomorphism )

assume ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K ) ; :: thesis: ( not J is one-to-one or not J is onto or J is isomorphism )

then ( J is additive & J is multiplicative & J is unity-preserving ) ;

hence ( not J is one-to-one or not J is onto or J is isomorphism ) ; :: thesis: verum

( J is isomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )

let J be Function of K,K; :: thesis: ( J is isomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )

thus ( J is isomorphism implies ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) ) by GROUP_1:def 13, GROUP_6:def 6; :: thesis: ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto implies J is isomorphism )

assume ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K ) ; :: thesis: ( not J is one-to-one or not J is onto or J is isomorphism )

then ( J is additive & J is multiplicative & J is unity-preserving ) ;

hence ( not J is one-to-one or not J is onto or J is isomorphism ) ; :: thesis: verum