let G, H be AddGroup; for f being Function of G,H st f is additive holds
GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
let f be Function of G,H; ( f is additive implies GroupMorphismStr(# G,H,f #) is strict Morphism of G,H )
assume A1:
f is additive
; GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
set F = GroupMorphismStr(# G,H,f #);
fun GroupMorphismStr(# G,H,f #) = f
;
hence
GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
by A1, Th10; verum