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 that
A1: ( dom f = G & cod f = H ) and
A2: fun f is additive ; :: thesis: f is strict Morphism of G,H
reconsider f9 = f as strict GroupMorphism by A2, Def11;
f9 is strict Morphism of G,H by A1, Def12;
hence f is strict Morphism of G,H ; :: thesis: verum