let F be strict GroupMorphism; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
take f ; :: thesis: ( 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; :: thesis: verum