let G, H be AddGroup; :: thesis: for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds
f is strict Morphism of G,H
let f be strict GroupMorphismStr ; :: thesis: ( dom f = G & cod f = H & fun f is additive implies f is strict Morphism of G,H )
assume A1: ( dom f = G & cod f = H & fun f is additive ) ; :: thesis: f is strict Morphism of G,H
then reconsider f' = f as strict GroupMorphism by Def18;
f' is strict Morphism of G,H by A1, Def19;
hence f is strict Morphism of G,H ; :: thesis: verum