let G, H be AddGroup; :: thesis: for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)
let F be strict Morphism of G,H; :: thesis: ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)
consider f being Function of G,H such that
A1: F = GroupMorphismStr(# G,H,f #) and
f is additive by Th12;
take f ; :: thesis: F = GroupMorphismStr(# G,H,f #)
thus F = GroupMorphismStr(# G,H,f #) by A1; :: thesis: verum