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

( 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