let F be strict GroupMorphism; ex G, H being AddGroup ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
consider G, H being AddGroup such that
A1:
F is Morphism of G,H
by Th14;
reconsider F9 = F as Morphism of G,H by A1;
consider f being Function of G,H such that
A2:
( F9 = GroupMorphismStr(# G,H,f #) & f is additive )
by Th12;
take
G
; ex H being AddGroup ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
take
H
; ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
take
f
; ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
thus
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
by A2; verum