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 #) & f is additive ) by Th22;
take f ; :: thesis: F = GroupMorphismStr(# G,H,f #)
thus F = GroupMorphismStr(# G,H,f #) by A1; :: thesis: verum