let K be Ring; :: thesis: for V, W being LeftMod of
for f being Function of V,W holds
( f is Homomorphism of V,W iff ( ( for x, y being Vector of holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x) ) ) )
let V, W be LeftMod of ; :: thesis: for f being Function of V,W holds
( f is Homomorphism of V,W iff ( ( for x, y being Vector of holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x) ) ) )
let f be Function of V,W; :: thesis: ( f is Homomorphism of V,W iff ( ( for x, y being Vector of holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x) ) ) )
set J = id K;

A1: now

assume A2: for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x) ; :: thesis: for a being Scalar of
for x being Vector of holds f . (a * x) = ((id K) . a) * (f . x)
let a be Scalar of ; :: thesis: for x being Vector of holds f . (a * x) = ((id K) . a) * (f . x)
let x be Vector of ; :: thesis: f . (a * x) = ((id K) . a) * (f . x)
(id K) . a = a by FUNCT_1:35;
hence f . (a * x) = ((id K) . a) * (f . x) by A2; :: thesis: verum

end;

now

assume A3: for a being Scalar of
for x being Vector of holds f . (a * x) = ((id K) . a) * (f . x) ; :: thesis: for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x)
let a be Scalar of ; :: thesis: for x being Vector of holds f . (a * x) = a * (f . x)
let x be Vector of ; :: thesis: f . (a * x) = a * (f . x)
(id K) . a = a by FUNCT_1:35;
hence f . (a * x) = a * (f . x) by A3; :: thesis: verum

end;

hence ( f is Homomorphism of V,W iff ( ( for x, y being Vector of holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of
for x being Vector of holds f . (a * x) = a * (f . x) ) ) ) by A1, Def24; :: thesis: verum