let G1, G2, G3 be AddGroup; :: thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds
G * F = GroupMorphismStr(# G1,G3,(g * f) #)
let G be Morphism of G2,G3; :: thesis: for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds
G * F = GroupMorphismStr(# G1,G3,(g * f) #)
let F be Morphism of G1,G2; :: thesis: for g being Function of G2,G3
for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds
G * F = GroupMorphismStr(# G1,G3,(g * f) #)
let g be Function of G2,G3; :: thesis: for f being Function of G1,G2 st G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) holds
G * F = GroupMorphismStr(# G1,G3,(g * f) #)
let f be Function of G1,G2; :: thesis: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) implies G * F = GroupMorphismStr(# G1,G3,(g * f) #) )
assume A1: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) ) ; :: thesis: G * F = GroupMorphismStr(# G1,G3,(g * f) #)
dom G = G2 by Def12
.= cod F by Def12 ;
hence G * F = GroupMorphismStr(# G1,G3,(g * f) #) by A1, Def14; :: thesis: verum