let G, H be AddGroup; :: thesis: for F being Morphism of G,H ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
let F be Morphism of G,H; :: thesis: ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
A1: the Target of F = cod F
.= H by Def12 ;
A2: the Source of F = dom F
.= G by Def12 ;
then reconsider f = the Fun of F as Function of G,H by A1;
take f ; :: thesis: ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
thus ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) by A2, A1, Th9; :: thesis: verum