let G, H be AddGroup; :: thesis: 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; :: thesis: ( f is additive implies GroupMorphismStr(# G,H,f #) is strict Morphism of G,H )
assume A1: f is additive ; :: thesis: GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
set F = GroupMorphismStr(# G,H,f #);
( dom GroupMorphismStr(# G,H,f #) = G & cod GroupMorphismStr(# G,H,f #) = H & fun GroupMorphismStr(# G,H,f #) = f ) ;
hence GroupMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th19; :: thesis: verum