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 Def18; :: thesis: verum