reconsider f0 = ZeroMap (G,H) as Element of Maps (G,H) by FUNCT_2:8;
set D = { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } ;
GroupMorphismStr(# G,H,f0 #) in { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } ;
then reconsider D = { GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive } as non empty set ;
A1: for x being object st x in D holds
x is strict Morphism of G,H
proof
let x be object ; :: thesis: ( x in D implies x is strict Morphism of G,H )
assume x in D ; :: thesis: x is strict Morphism of G,H
then ex f being Element of Maps (G,H) st
( x = GroupMorphismStr(# G,H,f #) & f is additive ) ;
hence x is strict Morphism of G,H by Th11; :: thesis: verum
end;
then A2: for x being Element of D holds x is strict Morphism of G,H ;
A3: for x being object st x is strict Morphism of G,H holds
x in D
proof
let x be object ; :: thesis: ( x is strict Morphism of G,H implies x in D )
assume x is strict Morphism of G,H ; :: thesis: x in D
then reconsider x = x as strict Morphism of G,H ;
A4: ( dom x = G & cod x = H ) by Def12;
then reconsider f = the Fun of x as Function of G,H ;
reconsider g = f as Element of Maps (G,H) by FUNCT_2:8;
A5: x = GroupMorphismStr(# G,H,g #) by A4;
the Fun of x is additive by Th9;
hence x in D by A5; :: thesis: verum
end;
reconsider D = D as GroupMorphism_DOMAIN of G,H by A2, Th25;
take D ; :: thesis: for x being object holds
( x in D iff x is strict Morphism of G,H )
thus for x being object holds
( x in D iff x is strict Morphism of G,H ) by A1, A3; :: thesis: verum