let F be GroupMorphism; :: thesis: the Fun of F is additive
the Fun of F = fun F ;
hence the Fun of F is additive by Def11; :: thesis: verum