let R be Ring; :: thesis: for F being LModMorphism of R holds
( the Fun of F is additive & the Fun of F is homogeneous )
let F be LModMorphism of R; :: thesis: ( the Fun of F is additive & the Fun of F is homogeneous )
the Fun of F = fun F ;
hence ( the Fun of F is additive & the Fun of F is homogeneous ) by Def7; :: thesis: verum