let K be Ring; :: thesis: for V, W being LeftMod of K

for f being Function of V,W holds

( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )

let V, W be LeftMod of K; :: thesis: for f being Function of V,W holds

( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V 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 V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )

set J = id K;

A1: ( ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) implies for a being Scalar of K

for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ) ;

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) ) by A1, Def17; :: thesis: verum

for f being Function of V,W holds

( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )

let V, W be LeftMod of K; :: thesis: for f being Function of V,W holds

( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V 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 V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )

set J = id K;

A1: ( ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) ) implies for a being Scalar of K

for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ) ;

now :: thesis: ( ( for a being Scalar of K

for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ) implies for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) )

hence
( f is Homomorphism of V,W iff ( ( for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y) ) & ( for a being Scalar of Kfor x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ) implies for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x) )

assume A2:
for a being Scalar of K

for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ; :: thesis: for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x)

let a be Scalar of K; :: thesis: for x being Vector of V holds f . (a * x) = a * (f . x)

let x be Vector of V; :: thesis: f . (a * x) = a * (f . x)

(id K) . a = a ;

hence f . (a * x) = a * (f . x) by A2; :: thesis: verum

end;for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ; :: thesis: for a being Scalar of K

for x being Vector of V holds f . (a * x) = a * (f . x)

let a be Scalar of K; :: thesis: for x being Vector of V holds f . (a * x) = a * (f . x)

let x be Vector of V; :: thesis: f . (a * x) = a * (f . x)

(id K) . a = a ;

hence f . (a * x) = a * (f . x) by A2; :: thesis: verum

for x being Vector of V holds f . (a * x) = a * (f . x) ) ) ) by A1, Def17; :: thesis: verum