let R be Ring; :: thesis: for M, N being LeftMod of R
for a being Element of the carrier of R
for f, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )
let M, N be LeftMod of R; :: thesis: for a being Element of the carrier of R
for f, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )
let a be Element of the carrier of R; :: thesis: for f, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )
let f, h be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: ( h = (LMULT (M,N)) . [a,f] iff for x being Element of M holds h . x = a * (f . x) )
thus ( h = (LMULT (M,N)) . [a,f] implies for x being Element of the carrier of M holds h . x = a * (f . x) ) by Def16; :: thesis: ( ( for x being Element of M holds h . x = a * (f . x) ) implies h = (LMULT (M,N)) . [a,f] )

now :: thesis: ( ( for x being Element of the carrier of M holds h . x = a * (f . x) ) implies h = (LMULT (M,N)) . [a,f] )

assume A1: for x being Element of the carrier of M holds h . x = a * (f . x) ; :: thesis: h = (LMULT (M,N)) . [a,f]
for x being Element of the carrier of M holds h . x = ((LMULT (M,N)) . [a,f]) . x

proof

let x be Element of the carrier of M; :: thesis: h . x = ((LMULT (M,N)) . [a,f]) . x
thus h . x = a * (f . x) by A1
.= ((LMULT (M,N)) . [a,f]) . x by Def16 ; :: thesis: verum

end;

hence h = (LMULT (M,N)) . [a,f] ; :: thesis: verum

end;

hence ( ( for x being Element of M holds h . x = a * (f . x) ) implies h = (LMULT (M,N)) . [a,f] ) ; :: thesis: verum