let R be Ring; :: thesis: for F being LModMorphism of R holds the Fun of F is linear
let F be LModMorphism of R; :: thesis: the Fun of F is linear
the Fun of F = fun F ;
hence the Fun of F is linear by Def10; :: thesis: verum