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