let F be RingMorphism; :: thesis: the Fun of F is linear
the Fun of F = fun F ;
hence the Fun of F is linear by Def5; :: thesis: verum